LeanInfer: Neural Network Inference in Lean 4

Stream: Machine Learning for Theorem Proving

[Kaiyu Yang]

Hi all,

We're excited to release LeanInfer (https://github.com/lean-dojo/LeanInfer): a tool for running the inference of neural networks in Lean. It is under development and currently provides a tactic for suggesting proof steps.

LeanInfer.png

The frontend of our tactic suggestion tool is based on llmstep (thanks!). However, instead of having Lean make requests to a model running in Python, we turn the model into a shared library and run it directly through Lean's FFI. We use the tactic generator (w/o retrieval) in LeanDojo. The model is relatively small (299M parameters) and has no problem running on my old MacBook 2020 with 16GB memory and no GPU.

Here is an example of how you can use LeanInfer in your project. You're welcome to check it out! Feel free to let us know if you encounter any glitches in installation (likely due to FFI), and we are happy to help.

This is a joint effort with Anima and @Peiyang Song, with the majority of technical work attributed to Peiyang.

[Scott Morrison]

Is there any prospect of simplifying the installation process? Step 3 is pretty dire.

[Scott Morrison]

e.g. could you provide ONNX automatically, using the same cloud build mechanism that ProofWidgets uses?

[Scott Morrison]

Even step 2 I'd hope could be done from inside Lean (e.g. the first time you run suggest_tactics, if it can't find the model it recommends running some command which will do it for you).

[Scott Morrison]

Maybe a more concrete suggestion: could you create a branch of Mathlib, so that running LeanInfer is a matter of:

• checking out the branch
• run some script (e.g. that downloads requirements)
• open VSCode?

If this is not possible, what is missing that we could provide in Lean / Lake / the VSCode extension that would make it possible?

[Scott Morrison]

(I appreciate that your instructions differ for different operating systems, but e.g. ProofWidgets copes with this: when I run lake build in a fresh clone of Mathlib you see Downloading proofwidgets/v0.0.13/macOS-64.tar.gz.)

[Kaiyu Yang]

Hi @Scott Morrison ,

Thank you for the suggestions! I totally agree this is the way to go. I wasn't aware of the cloud build mechanism and just took a look. From my understanding, we can compile LeanInfer's C++ code into static libraries for different platforms and release them on GitHub. When the user runs lake build in a project depending on LeanInfer, all libraries will be downloaded instead of built locally. The user does not need to compile anything locally (no need to set environment variables). Also, the user doesn't have to install ONNX Runtime since it is included in LeanInfer's static libraries. Is that correct?

Following this idea, I created an improve-installation branch in LeanInfer and released it as v0.0.3. I also created an improve-installation branch in lean4-example, which depends on v0.0.3 of LeanInfer. However, when running lake build, I see the following error. Looks like it still tries to compile ffi.o even if it's available in the release.

(base) kaiyuy@Kaiyus-MacBook-Pro lean4-example % lake build
Downloading LeanInfer/v0.0.3/macOS-64.tar.gz
[0/93] Building Std.Lean.Position
[0/99] Building Std.Tactic.OpenPrivate
[0/99] Building Std.Lean.Command
[0/99] Building Std.Tactic.Unreachable
[0/102] Building Std.Lean.TagAttribute
[0/105] Building Std.Tactic.RCases
[0/112] Building Std.Util.TermUnsafe
[1/197] Compiling ffi.cpp
[2/197] Compiling Std.Lean.TagAttribute
Unpacking LeanInfer/v0.0.3/macOS-64.tar.gz
[3/197] Compiling Std.Lean.Position
[4/197] Compiling Std.Tactic.Unreachable
[5/197] Compiling Std.Lean.Command
[6/197] Building Std.Tactic.ByCases
[7/197] Building Std.Tactic.SeqFocus
[8/197] Building Std.Lean.Name
[9/197] Building Std.Lean.Parser
[10/197] Building Std.Lean.Meta.Basic
[11/197] Building Std.Lean.Tactic
error: > clang++ -c -o ./lake-packages/LeanInfer/build/ffi.o ./lake-packages/LeanInfer/ffi.cpp -fPIC -std=c++11 -stdlib=libc++ -O3 -I /Users/kaiyuy/.elan/toolchains/leanprover--lean4---v4.0.0/include
error: stderr:
./lake-packages/LeanInfer/ffi.cpp:2:10: fatal error: 'onnxruntime_cxx_api.h' file not found
#include <onnxruntime_cxx_api.h>
         ^~~~~~~~~~~~~~~~~~~~~~~
1 error generated.

Note that the error is not deterministic. If I run lake clean && lake build multiple times in lean4-example, sometimes the error becomes:

(base) kaiyuy@Kaiyus-MacBook-Pro lean4-example % lake clean && lake build
Downloading LeanInfer/v0.0.3/macOS-64.tar.gz
[0/9] Building Std.Lean.Position
[0/36] Building Std.Tactic.OpenPrivate
[0/45] Building Std.Lean.Command
[0/63] Building Std.Tactic.RCases
[0/84] Building Std.Tactic.Unreachable
[0/87] Building Std.Util.TermUnsafe
[0/87] Building Std.Lean.TagAttribute
[1/197] Building Std.Tactic.ByCases
[2/197] Building Std.Tactic.SeqFocus
Unpacking LeanInfer/v0.0.3/macOS-64.tar.gz
[3/197] Building Std.Lean.Name
[4/197] Building Std.Lean.Parser
[5/197] Building Std.Lean.Meta.Basic
[6/197] Building Std.Lean.Tactic
[7/197] Building Std.Lean.NameMapAttribute
[8/197] Building Std.Data.List.Init.Lemmas
[9/197] Compiling Std.Lean.TagAttribute
[10/197] Compiling Std.Lean.Position
[11/197] Compiling Std.Tactic.Unreachable
[12/197] Compiling Std.Lean.Name
[13/197] Compiling Std.Lean.Parser
[14/197] Compiling Std.Lean.Command
[15/197] Compiling Std.Lean.Tactic
[16/197] Compiling Std.Util.TermUnsafe
[17/197] Compiling Std.Tactic.SeqFocus
[18/197] Compiling Std.Lean.NameMapAttribute
[19/197] Compiling Std.Tactic.ByCases
[20/197] Compiling Std.Tactic.OpenPrivate
[21/197] Linking libleanffi.dylib
[22/197] Linking Std.Lean.TagAttribute
error: > /Users/kaiyuy/.elan/toolchains/leanprover--lean4---v4.0.0/bin/leanc -shared -o ./lake-packages/LeanInfer/build/lib/libleanffi.dylib -Wl,-force_load,./lake-packages/LeanInfer/build/lib/libleanffi.a -lonnxruntime -lstdc++
error: stderr:
ld64.lld: error: library not found for -lonnxruntime
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/Users/kaiyuy/.elan/toolchains/leanprover--lean4---v4.0.0/bin/leanc` exited with code 1

Regarding how lake selects the file to download based on the platform, it doesn't distinguish between x64 and arm64? The macOS release was built on my Intel x64 Mac. I'm not sure if it will work for a newer Mac.

[Utensil Song]

Hi @Kaiyu Yang Thanks for creating LeanInfer and the work on installation improvements!

I've tried out lean4-example in Github Codespace, I got the following issues:

1. lake build fails to compile C++ with Clang++, resolved by removing all -stdlib=libc++from the lakefile of LeanInfer

lean4-example (improve-installation) $ lake build
[23/197] Compiling ffi.cpp
error: > clang++ -c -o ./lake-packages/LeanInfer/build/ffi.o ./lake-packages/LeanInfer/ffi.cpp -fPIC -std=c++11 -stdlib=libc++ -O3 -I /home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include
error: stderr:
In file included from ./lake-packages/LeanInfer/ffi.cpp:1:
/home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include/lean/lean.h:14:10: fatal error: 'atomic' file not found
#include <atomic>
         ^~~~~~~~
1 error generated.
error: external command `clang++` exited with code 1

I ran bash -c "$(wget -O - https://apt.llvm.org/llvm.sh)" from https://apt.llvm.org/ to fix it, no change.
Then I test the clang++ command with extra options -E -x c++ -v at the end, it showed the following search path:

ignoring nonexistent directory "/include"
#include "..." search starts here:
#include <...> search starts here:
 /home/codespace/.elan/toolchains/leanprover--lean4---v4.0.0/include
 /usr/local/include
 /usr/lib/llvm-10/lib/clang/10.0.0/include
 /usr/include/x86_64-linux-gnu
 /usr/include
End of search list.

which is shorter than a raw clang++ -E -x c++ - -v < /dev/null 2>&1 which shows

ignoring nonexistent directory "/include"
ignoring duplicate directory "/usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9"
#include "..." search starts here:
#include <...> search starts here:
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/x86_64-linux-gnu/c++/9
 /usr/bin/../lib/gcc/x86_64-linux-gnu/9/../../../../include/c++/9/backward
 /usr/local/include
 /usr/lib/llvm-10/lib/clang/10.0.0/include
 /usr/include/x86_64-linux-gnu
 /usr/include
End of search list.

Clearly Clang++ stop looking for the GNU C++ headers if -stdlib=libc++ is present. If Github Codespace misses it I guess it would be missed in the environments of many end-users.

2. After resolved issue 1, I end up having the same issue fatal error: 'onnxruntime_cxx_api.h' file not found, resolved by

( cd /workspace/ && wget https://github.com/microsoft/onnxruntime/releases/download/v1.15.1/onnxruntime-linux-x64-1.15.1.tgz && tar xzvf  onnxruntime-linux-x64-1.15.1.tgz)

Then add "-I", "/workspaces/onnxruntime-linux-x64-1.15.1/include" to flags in LeanInfer lakefile

3. Run lake build after step 2, I have the same linker error libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, libonnxruntime.so.1.15.1: cannot open shared object file: No such file or directory, I tried to fix it by adding "-L", "/workspace/onnxruntime-linux-x64-1.15.1/lib/" to moreLinkArgs then

LD_LIBRARY_PATH=/workspaces/onnxruntime-linux-x64-1.15.1/lib/ lake build

But the build hangs indefinitely, and it's not using much CPU. So far I'm stuck here.

So the answer to the question

The user does not need to compile anything locally (no need to set environment variables). Also, the user doesn't have to install ONNX Runtime since it is included in LeanInfer's static libraries. Is that correct?

is currently no. In my test, "When the user runs lake build in a project depending on LeanInfer, all libraries will be downloaded instead of built locally. " is not happening, the end user would still have to recompile like you did.

[Kaiyu Yang]

Hi @Utensil Song , the improve-installation branch is not ready yet. Could you please try out the main branch? Do you see the same error messages?

[Kaiyu Yang]

is currently no. In my test, "When the user runs lake build in a project depending on LeanInfer, all libraries will be downloaded instead of built locally. " is not happening, the end user would still have to recompile like you did.

With the cloud build mechanism, the user shouldn't need to compile anything? I'm wondering why it still tries to compile the library when the library can simply be downloaded.

[Scott Morrison]

I suspect for questions about the interaction of cloud build and FFI --- which presumably have never been asked before! --- we may need to see if @Mac Malone can answer.

(They don't usually read this stream, but I'll spam them now. :-)

[Utensil Song]

Kaiyu Yang said:

Hi Utensil Song , the improve-installation branch is not ready yet. Could you please try out the main branch? Do you see the same error messages?

I tried main (it deletes the old LeanInfer and rebuilds), and the same 3 issues happens.

[Utensil Song]

Kaiyu Yang said:

With the cloud build mechanism, the user shouldn't need to compile anything? I'm wondering why it still tries to compile the library when the library can simply be downloaded.

From the source of both lakefiles in LeanInfer and lean4-example, I see no code handling uploading the built binary, or downloading the built binary for the end user. How did you implement it?

[Kaiyu Yang]

@Utensil Song Could you please open an issue in LeanInfer? Thanks!

I uploaded the built binaries manually when creating the release. As for the cloud build, it is handled by lake. With preferReleaseBuild in lakefile.lean, lake will download from the package's GitHub releases when running lake build.

[Utensil Song]

Kaiyu Yang said:

I uploaded the built binaries manually when creating the release. As for the cloud build, it is handled by lake. With preferReleaseBuild in lakefile.lean, lake will download from the package's GitHub releases when running lake build.

In that case, I read the code in lake, it turns out to only fetch the cloud release when running lake build :release in LeanInfer.

When I run it, it successfully skips building from scratch, printed:

$ lake build :release
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
Downloading LeanInfer/v0.0.3/linux-64.tar.gz
Unpacking LeanInfer/v0.0.3/linux-64.tar.gz

But if I run lake build for lean4-example, it still compiles ffi.cpp, ignoring everything upacked (ffi.o, libLeanInfer-Basic-1.so, libLeanInfer-Frontend-1.so, libleanffi.so etc.)

I've opened an issue about Codespace build only: lean-dojo/LeanInfer#3

[Mac Malone]

Utensil Song said:

it turns out to only fetch the cloud release when running lake build :release in LeanInfer.

With preferReleaseBuild set, it should download it by default as part of a normally lake build (without needing to specify lake build :release)

[Mac Malone]

Utensil Song said:

But if I run lake build for lean4-example, it still compiles ffi.cpp, ignoring everything upacked (ffi.o, libLeanInfer-Basic-1.so, libLeanInfer-Frontend-1.so, libleanffi.so etc.)

The problem here is likely that lean4-example does not depend on the improve-installation branch of LeanInfer where preferReleaseBuild is set to true.

[Kaiyu Yang]

@Utensil Song Thanks for opening the issue. It has been resolved in https://github.com/lean-dojo/LeanInfer/issues/3. The problem was related to the conflicts between LLVM+Clang vs. GCC.

[Utensil Song]

Yes, I understand the expected behavior, but for LeanInfer and lean4-example of it, lake build :release indeed triggered a different behavior, without :release it just builds from scratch.

I see nothing done different from the lake doc or the Proof Widget project in LeanInfer @ v0.0.3 where the improve-installation of LeanInfer is released there.

[Mac Malone]

@Utensil Song The LeanInfer version of lean4-example is 5c75218 which does not use preferReleaseBuild and that is why it does not work there (or at least part of the reason). For LeanInfer itself, you are correct, you do need to use lake build :release to download the cloud build.

[Kaiyu Yang]

@Mac Malone

The problem here is likely that lean4-example does not depend on the improve-installation branch of LeanInfer where preferReleaseBuild is set to true.

I was using the improve-installation branch of lean4-example. It depends on LeanInfer@v0.0.3 (lakefile here). And v0.0.3 is the latest commit (5782a422a8d11650640324eb4e68fa2c298e9736) of LeanInfer's improve-installation branch.

[Mac Malone]

@Kaiyu Yang Ah, sorry, I did not notice there was another branch of lean4-example.

[Kaiyu Yang]

Sorry for the confusion. Basically we're trying to improve the installation, and this WIP is named improve-installation branch in both repos.

[Kaiyu Yang]

default as part of a normally lake build (with needing to specify lake build :release)

@Mac Malone Did you actually mean "without needing to"?

[Mac Malone]

@Kaiyu Yang Ah, I figured out the problem here. LeanInfer's extern_lib does not depend on the release facet, so it begins building without waiting for the download to complete.

[Utensil Song]

Mac Malone said:

Utensil Song The LeanInfer version of lean4-example is 5c75218 which does not use preferReleaseBuild and that is why it does not work there (or at least part of the reason). For LeanInfer itself, you are correct, you do need to use lake build :release to download the cloud build.

I tried adding preferReleaseBuild to the lakefile of the example, but it still rebuild from scratch. Then I checked Mathlib4 which is using ProofWidget, and it has set no such flag, so I thought this flag is not needed for the end user lean project that's using LeanInfer.

[Mac Malone]

@Utensil Song You are correct .lean4-example does not need preferReleaseBuild (since we do not need cloud releases of lean4-example itself).

[Kaiyu Yang]

@Mac Malone Oh, I see, that makes sense. Would it be possible for you to open a PR to (the improve-installation branch of) LeanInfer to fix this? Thanks!

[Utensil Song]

It's strange that even when I manually made the binaries downloaded via lake build :release, lake still doesn't recognize them.

[Utensil Song]

How to depend on the release facet? Found no doc about it, and the extern_lib source has no arguments for that too. :joy:

[Mac Malone]

Utensil Song said:

It's strange that even when I manually made the binaries downloaded via lake build :release, lake still doesn't recognize them.

:sweat_smile: That is because there is a second problem: the dependency trace of ffi.o includes the hash of the -Ilean/include directory which is system-dependent. That also needs to be fixed. Working on a PR now.

[Mac Malone]

lean-dojo/LeanInfer#4

[Mac Malone]

@Kaiyu Yang

[Kaiyu Yang]

I'll take a look asap. Thanks!

[Kaiyu Yang]

@Mac Malone This PR works great! Now it no longer tries to re-compile the C++ library. But we got another error during linking. I put the details in the PR.

[Kaiyu Yang]

We have made the installation process substantially simpler and more robust. Here are steps to see a working example in GitHub Codespace:

1. Launch a GitHub Codespace on the LeanInfer-demo branch of lean4-example.
2. Install elan: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
3. Download the model and build the project: git lfs install && git clone https://huggingface.co/kaiyuy/onnx-leandojo-lean4-tacgen-byt5-small && lake build
4. Install the lean4 VSCode extension and open Lean4Example.lean

We handle most dependencies in LeanInfer's lakefile, so the user doesn't have to install anything other than elan. And they do not have to compile the FFI part locally (fewer nasty compilation errors). This wouldn't be possible without the help of @Mac Malone !

We also plan to get rid of the model downloading when building the project. I'll work on that when I get a chance.

[Kaiyu Yang]

Here is a more technical note of what we did. It might be useful for other projects involving FFI + external dependencies + cloud release + cross-platform:

Challenge 1: Dependency Hell

LeanInfer's C++ code depends on an external library called ONNX Runtime, whose platform-specific binaries can be downloaded here. Furthermore, somehow LeanInfer can only be compiled by LLVM (with Clang, libc++, libc++abi, and libunwind) but not GCC. This has caused a lot of hassles during compilation. The LLVM installation on many Linux systems is incomplete. For example, if you use LLVM's official installation script, by default, it does not install libunwind. You may get a compilation error that libunwind cannot be found. Or worse, the compiler may link to a non-LLVM version of libunwind, leading to mysterious errors down the road.

Our solution is to locate the correct libonnxruntime.so, libc++.so, libc++abi.so, and libunwind.so, pack them into build/lib/, and release them using lake's cloud release mechanism. We only do this for Linux, since the compilation toolchain on macOS is based on LLVM.

Challenge 2: Supporting Different Platforms

We want to support 4 platforms:
linux-x86_64
macOS-x86_64
macOS-arm64
linux-arm64 (relatively rare but possible, e.g., Linux Docker container running on macOS-arm64)
lake's cloud release mechanism does not directly support distinguishing x86_64 and arm64. The binary libraries in the cloud release are platform-dependent and wouldn't work on a different platform. However, we managed to set preferReleaseBuild and buildArchive ? in a platform-dependent way to make sure the correct version of the binary is downloaded.

[Utensil Song]

This went well for mathlib-free projects, thanks for the exploration of such a solution that also applies to other FFI projects!

Does this work with Mathlib4? My attempt:

1. start with the LeanInfer example that already works.
2. added require mathlib from git "https://github.com/leanprover-community/mathlib4" to lakefile
3. run lake update & lake exe cache get -> cache complains a million times of: Warning: lake-packages/std/Std/Data/Sum/Basic.lean not found. Skipping all files that depend on it
4. import any Mathlib stuff that already works in a non-LeanInfer project
5. run lake build

error: no such file or directory (error code: 2)
  file: ./lake-packages/std/././Std/Data/Sum/Basic.lean

I think this is because Mathlib also depends on Std and I recall a warning about don't require Std ourselves, but I don't know if this would cause troubles if I depend on Std via LeanInfer.

[Utensil Song]

Ah, it works, as long as I require Mathlib first, then LeanInfer ( I also removed explicitly requiring aesop).

The cache is downloaded and unpacked, but the whole Mathlib is compiled again: lake.log

Anyway, it works smoothly ever since.

Here's a great case to close the goal:

image.png

Unfortunately, the result is very volatile, if I delete the line and re-enter suggest_tactics, it mostly suggests other unhelpful tactics that makes no use of Filter-related info, one of them looks like this:

image.png

Also, if I only just move cursor elsewhere and back, the suggestion mostly stay the same (maybe this is by design), I'll have to do some retyping like remove and type the trailing "s" to trigger a refresh of suggestions. After the first time LeanInfer gives me the great result, I tried a few dozen times to get the same suggestion back.

Maybe it's an interesting case to investigate, here's the #mwe:

import LeanInfer
import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Finite
import Mathlib.Order.Filter.Basic

theorem Filter.ext_iff₁ (f g : Filter α) : f = g ↔ (∀ s, s ∈ f ↔ s ∈ g) := by
  suggest_tactics

[Kaiyu Yang]

@Utensil Song the problem you encountered might be related to the version of std4. I got a similar error when trying to add LeanInfer as a dependency of mathlib4 and run lake update && lake build. The problem was resolved after I switched to lake update LeanInfer && lake build. It looks like mathlib4 may break if you update some of its dependencies.

[Patrick Massot]

A very useful general tip is to never ever run lake update without argument.

[Kaiyu Yang]

Regarding the quality of the tactic suggestions, for now, we expect them to lag behind the version in LeanDojo (although they use the same model). In LeanDojo, we use beam search to generate 64 tactics, and the hyperparameters (e.g., length penalty in beam search) are well-tuned. Currently, LeanInfer uses multinomial sampling (since it's way easier to implement than beam search), and the hyperparameters are quite arbitrary. Here is a nice blog explaining different algorithms for generation. We plan to add beam search to LeanInfer by implementing the algorithm directly in Lean, though our first priority right now is to support premise selection similar to lean-premise-selection.

Yes, moving the cursor around wouldn't trigger a regeneration. suggest_tactics is just like other tactics. It is re-run only when you make changes to the file that have an effect on it.

[Utensil Song]

Thanks, I'm aware the issue of lake update and mathlib, but note that in my experimenting case (starting with a working LeanInfer & Mathlib-free project, then add Mathlib), lake update or lake update mathlib is required (or the manifest is missing mathlib). So the cause is actually the order of require: one can't require Mathlib after a Lean library that also uses std4, and this is also how I solved it.

The unresolved issue is, even after the reordering, mathlib cache seems to be ineffective and lake rebuilt it.

[Utensil Song]

Looking forward to the Lean implemented beam search (or at least top-k would already be better).

Now the suggestion varies from making no progress, some progress(blue) and closing the goal( :tada: ) so I need to trigger it repeatedly. And I found it's more convenient to apply a suggestion then undo to trigger a new round of suggestion.

[Utensil Song]

Presumably the premise-selection-guided suggestions would also be better, even with greedy search algorithm with multinomial sampling.

One observation of a series of different suggestions given is that they somehow guess the likely tactics first, then their parameters (e.g. premises). Algorithmically, It first give very random tactics (due to temperature 1.0), then greedily find premises that fit the tactics but match the goal less.

[Kaiyu Yang]

I'm wondering how the version of std4 is determined if lakefile.lean contains

require mathlib from git "https://github.com/leanprover-community/mathlib4"
require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.6"

And will it be any different if the order of mathlib4 and LeanInfer is switched? @Mac Malone

[Mac Malone]

@Kaiyu Yang In that order, the version of Std from mathlib will picked. In the reverse order, the version of Std from LeanInfer will be picked. Every dependency of a package is resolved in order, then each dependency's depedencies are resolved recursively in order. For example, given the tree:

A
  AA
     AAA
     AAB
  AB
     ABA
     ABB
B
  BA
     BAA
     BAB
  BB
     BBA
     BBB

The resolution, in order, is A,. B, AA, AB, AAA, AAB, ABA, ABB, BA, BB, BAA, BAB, BBA, BBB.

[Kaiyu Yang]

@Mac Malone I see. Thanks for the explanation! Since mathlib4 is less permissive in the versions of its dependencies, we should probably require mathlib4 first before requiring other packages?

[Mac Malone]

@Kaiyu Yang Yes, though, the problem appears to be that LeanInfer is using some newer features of Std not present in mathlbi's current version (namely, Std.Data.Sum.Basic).

[Scott Morrison]

I just made a sample project with LeanInfer and Mathlib as dependencies. For me it seems to work quite well:

You just need:

git clone https://github.com/leanprover-community/mathlib4_with_LeanInfer.git && cd mathlib4_with_LeanInfer && git submodule init && git submodule update && lake exe cache get && lake build

and then open Mathlib4WithLeanInfer.lean, in which:

example (f g : Filter α) : f = g ↔ (∀ s, s ∈ f ↔ s ∈ g) := by
  suggest_tactics

displays:

  Try this:
  • 🎉 simp only [Filter.ext_iff, Set.mem_setOf_eq]
  • constructor
  • rw [ext_iff, ext_iff]
  • simp only [Filter.Eventually, ext_iff, exists_imp]
  • simp_rw [← eq_comm, compl_compl, eq_iff_iff]
  • simp only [Filter.mem_iff, image_iff_bex, exists_prop]
  • simp only [eq_iff_iff, forall_congr', forall_exists_index]
  • simp only [← @filter_eq_iff, forall_exists_index, Iff.comm]

[Scott Morrison]

Unfortunately lake exe cache get seems to download an unusable cache (presumably the "two different projects both depend on Std" problem?), so the lake build step is still slow.

[Mario Carneiro]

I don't see any reason why the cache shouldn't work

[Kaiyu Yang]

I followed @Scott Morrison's steps, and lake exe cache getseemed to work well? It didn't recompile any file from mathlib.

(base) kaiyuy@Kaiyus-MacBook-Pro mathlib4_with_LeanInfer % lake exe cache get
info: cloning https://github.com/leanprover-community/mathlib4.git to ./lake-packages/mathlib
info: cloning https://github.com/lean-dojo/LeanInfer.git to ./lake-packages/LeanInfer
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
info: cloning https://github.com/gebner/quote4 to ./lake-packages/Qq
info: cloning https://github.com/JLimperg/aesop to ./lake-packages/aesop
info: cloning https://github.com/mhuisi/lean4-cli.git to ./lake-packages/Cli
info: cloning https://github.com/EdAyers/ProofWidgets4 to ./lake-packages/proofwidgets
info: Downloading proofwidgets/v0.0.15/macOS-64.tar.gz
info: Unpacking proofwidgets/v0.0.15/macOS-64.tar.gz
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
Attempting to download 85 file(s)
Downloaded: 85 file(s) [attempted 85/85 = 100%] (100% success)
Decompressing 3764 file(s)
unpacked in 13073 ms
(base) kaiyuy@Kaiyus-MacBook-Pro mathlib4_with_LeanInfer % lake build
Downloading LeanInfer/v0.0.6/x86_64-macOS-64.tar.gz
[8/187] Compiling Std.Lean.Position
[8/187] Compiling Std.Lean.TagAttribute
[8/187] Compiling Std.Lean.Command
[8/187] Compiling Std.Tactic.Unreachable
[8/187] Compiling Std.Tactic.OpenPrivate
[8/187] Compiling Std.Util.TermUnsafe
[8/245] Compiling Std.Tactic.RCases
[15/784] Compiling Std.Tactic.ByCases
[16/784] Compiling Std.Tactic.SeqFocus
[17/784] Compiling Std.Lean.Name
[21/784] Linking Std.Lean.TagAttribute
[22/784] Compiling Std.Lean.Parser
[28/784] Compiling Std.Lean.Tactic
[28/784] Compiling Std.Lean.Meta.Basic
[33/784] Compiling Std.Lean.NameMapAttribute
[34/784] Compiling Std.Data.List.Init.Lemmas
[35/784] Compiling Std.Data.Ord
[36/784] Compiling Std.Classes.Dvd
[37/784] Compiling Std.Control.ForInStep.Basic
[38/784] Compiling Std.Util.ExtendedBinder
[39/784] Compiling Std.Data.Option.Init.Lemmas
[40/784] Compiling Std.Tactic.HaveI
[106/784] Compiling Std.Lean.Meta.Expr
[107/784] Compiling Std.Lean.PersistentHashMap
[108/784] Compiling Std.Classes.BEq
[109/784] Compiling Std.Lean.Meta.LCtx
Unpacking LeanInfer/v0.0.6/x86_64-macOS-64.tar.gz
[112/784] Linking Std.Tactic.Unreachable
[112/784] Linking Std.Lean.Position
[112/784] Linking Std.Lean.Name
[115/784] Linking Std.Lean.Command
[116/784] Linking Std.Util.TermUnsafe
[117/784] Linking Std.Lean.Parser
[117/784] Compiling Std.Lean.AttributeExtra
[119/784] Linking Std.Lean.Tactic
[120/784] Linking Std.Tactic.SeqFocus
[120/784] Compiling Std.Tactic.GuardExpr
[121/784] Compiling Std.Tactic.NoMatch
[121/784] Compiling Std.Lean.Format
[122/784] Linking Std.Lean.NameMapAttribute
[133/784] Linking Std.Data.List.Init.Lemmas
[133/784] Linking Std.Tactic.ByCases
[133/784] Linking Std.Data.Ord
[133/784] Compiling Std.Data.Char
[133/784] Linking Std.Data.Option.Init.Lemmas
[134/784] Linking Std.Classes.Dvd
[136/784] Linking Std.Control.ForInStep.Basic
[136/784] Linking Std.Tactic.OpenPrivate
[137/784] Linking Std.Lean.Meta.Expr
[137/784] Linking Std.Classes.BEq
[142/784] Linking Std.Lean.Meta.LCtx
[149/784] Compiling Std.Linter.UnreachableTactic
[152/784] Linking Std.Lean.PersistentHashMap
[158/784] Linking Std.Tactic.HaveI
[162/784] Linking Std.Lean.AttributeExtra
[164/784] Compiling Std.Tactic.Lint.Basic
[164/784] Linking Std.Lean.Format
[164/784] Compiling Std.Data.Nat.Basic
[164/784] Compiling Std.Control.ForInStep.Lemmas
[165/784] Compiling Std.Classes.SetNotation
[185/784] Linking Std.Util.ExtendedBinder
[193/784] Linking Std.Tactic.NoMatch
[193/784] Linking Std.Control.ForInStep.Lemmas
[195/784] Linking Std.Data.Nat.Basic
[200/784] Compiling Std.Linter.UnnecessarySeqFocus
[200/784] Compiling Std.Tactic.Simpa
[202/784] Compiling Std.Data.Array.Init.Basic
[203/784] Compiling Std.Tactic.TryThis
[212/784] Linking Std.Lean.Meta.Basic
[213/784] Linking Std.Tactic.Lint.Basic
[215/784] Linking Std.Data.Array.Init.Basic
[217/784] Linking libleanffi.dylib
[220/784] Linking Std.Linter.UnreachableTactic
[226/784] Linking Std.Tactic.GuardExpr
[231/784] Compiling Std.Linter
[231/784] Linking Std.Classes.SetNotation
[233/784] Compiling Std.Tactic.SimpTrace
[233/784] Compiling Std.Tactic.ShowTerm
[238/784] Compiling Std.Data.Array.Basic
[249/784] Compiling Std.Tactic.Lint.Misc
[257/784] Compiling Std.Tactic.Basic
[258/784] Linking Std.Data.Array.Basic
[262/784] Linking Std.Linter.UnnecessarySeqFocus
[264/784] Compiling Std.Logic
[267/784] Linking Std.Tactic.TryThis
[274/784] Linking Std.Linter
[274/784] Compiling Std.Classes.LawfulMonad
[274/784] Compiling Std.Data.Nat.Init.Lemmas
[278/784] Linking Std.Tactic.ShowTerm
[284/784] Compiling Std.Data.Option.Basic
[284/784] Compiling Std.Data.Nat.Lemmas
[286/784] Compiling Std.Data.Array.Init.Lemmas
[294/784] Compiling Std.Data.List.Basic
[294/784] Compiling Std.Data.Array.Merge
[308/784] Compiling Std.Lean.Meta.DiscrTree
[315/784] Linking Std.Tactic.Simpa
[319/784] Compiling Std.Tactic.Ext.Attr
[326/784] Compiling Std.Tactic.Ext
[327/784] Compiling Std.Data.Option.Lemmas
[329/784] Linking Std.Tactic.SimpTrace
[340/784] Linking Std.Tactic.Basic
[342/784] Compiling Std.Data.List.Lemmas
[352/784] Compiling Std.Data.Array.Lemmas
[356/784] Compiling Std.Data.Array.Match
[364/784] Compiling Std.Data.String.Basic
[367/784] Linking Std.Tactic.Lint.Misc
[368/784] Building LeanInfer.Frontend
[374/784] Linking Std.Logic
[377/784] Linking Std.Data.Nat.Init.Lemmas
[377/784] Linking Std.Classes.LawfulMonad
[384/784] Linking Std.Data.Nat.Lemmas
[388/784] Linking Std.Data.Option.Basic
[388/784] Linking Std.Data.Array.Init.Lemmas
[392/784] Linking Std.Data.Array.Merge
[519/784] Linking Std.Lean.Meta.DiscrTree
[763/784] Linking Std.Tactic.RCases
[764/784] Linking Std.Data.Char
[764/784] Linking Std.Tactic.Ext.Attr
[766/784] Linking Std.Tactic.Ext
[766/784] Linking Std.Data.Option.Lemmas
[769/784] Linking Std.Data.List.Basic
[770/784] Linking Std.Data.List.Lemmas
[771/784] Linking Std.Data.Array.Lemmas
[774/784] Linking Std.Data.Array.Match
[775/784] Linking Std.Data.String.Basic
[776/784] Linking LeanInfer.Frontend
[777/784] Building LeanInfer.Basic
[779/784] Linking LeanInfer.Basic
[780/784] Building LeanInfer
[782/784] Linking LeanInfer
[783/784] Building Mathlib4WithLeanInfer

[Scott Morrison]

Can confirm, works for me too!

[Scott Morrison]

Now that it is a one-liner to install I hope many people will try it out.

[Scott Morrison]

@Kaiyu Yang, I think the obvious final step would be to remove the need to manually download.

Instead, the first time running suggest_tactics, fail with an error, and a suggestion to run the #download_lean_infer_model command

[Kaiyu Yang]

It's sort of already doing that. If it cannot find the model, it produces a warning and ask the user to download the model.
image.png

[Scott Morrison]

Oh, I missed that!

[Scott Morrison]

Can we just change it to: "Cannot find the generator model. If you would like to download it to this project, run suggest_tactics!"?

[Scott Morrison]

(I guess it would be better to download it somewhere central, e.g. ~/.models/?)

[Adam Topaz]

IIRC git lfs requires an additional install on some operating systems (e.g. it did for me on Nixos). Maybe it’s worthwhile to add something to those instruction along those lines, in case some users get confused by the suggested command failing?

[Kaiyu Yang]

I just released v0.0.7 incorporating these suggestions from @Scott Morrison and @Adam Topaz.

Since downloading the model may take a few minutes, it would be great to show something so that the user knows it's downloading. I tried to add a LogInfo before downloading, but the message appears only after the downloading finishes, presumably because the message is not flushed. I see this is an existing issue without a good solution: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Implementing.20find_theorems/near/378461661. For now, I just give the user heads-up in suggest_tactics's warning message:

Cannot find the generator model. If you would like to download it to this project, run `suggest_tactics!` and wait for a few minutes.

[Scott Morrison]

The solution here is widgets. It's slightly painful overhead to implement something if it is only needed for the downloading step.

(e.g. consider Sagredo, which gives progressive updates from GPT)

It would be nice to implement a widget that just executes an external shell command and streams the output back to the infoview.

[Min-Hsien Weng]

Kaiyu Yang said:

I just released v0.0.7 incorporating these suggestions from Scott Morrison and Adam Topaz.

The new release [v0.0.7] works. Here is my experiment with LeanInfer v.0.0.7 and the example code.
(1) Followed the instructions and the installation worked well.
(2) Opened the example code Lean4Example.lean with VS Code.
(2.1) Added the code import LeanInfer. This started the building process and showed a successful message.
(2.2) Added the code suggest_tactic. I saw the following warning message:

Cannot find the generator model. If you would like to download it to this project, run `suggest_tactics!` and wait for a few minutes.

After waiting some time, the LeanInfer model was downloaded successfully to the folder ~/.cache/lean_infer.
(3) VS Code asked me to restart the LEAN server. I tried to restart it, but the LeanInfo window didn't show up properly.
(4) So I restarted VS Code and opened the example code Lean4Example.lean again.
(5) VS Code displayed a list of suggested tactics. :tada:

I am using Ubuntu 20.04 on Windows for Linux, with an Intel i5 CPU and 16 GB of memory.
A minor technical glitch with Lean Infoview is that it sometimes asks to restart the LEAN server when I make changes to Lean example code. However, once the server is up, Lean Infoview works well.

[Scott Morrison]

I guess a minor quibble: the help text without a model says "to download it to this project", but suggest_tactic! downloads to ~/.cache/.

[Utensil Song]

The lakefile of LeanInfer has quite some code to handle Challenge 1: Dependency Hell and Challenge 2: Supporting Different Platforms.

Two questions naturally arise:

1. Could these code be moved into a separate lean file, e.g. lakefile_helper.lean so the lakefile remain concise? Is this practice supported by lake (both technically and idiomatically)?

2. Could some of them be added to vanilla lake and made declarative?

[Mac Malone]

Utensil Song

1. No, Lake does not currently support this (technically). It will be a while before this feature is possible.

2. Parts of it, yes, I do hope to add to Lake, but a lot is specific to LeanInfer. Components that have been or are hoped to be added:

   • Architecture distinguishing in cloud releases (lake#173)
   • afterReleaseSync/Async (already done in lean4#2521; will be in Lean v4.1.0)
   • Better shared external library & C++ standard library support

[Utensil Song]

Thanks, after struggling for my experimental C++ FFI project trying to figure out what can be simplified in the lakefile, I've realized every line is helpful :joy:

I will open a separate topic later about what I found (and still can't solve), really looking forward to better shared external library & C++ standard library support in lake as well as other handy utilities for cloud release etc., and LeanInfer is an excellent milestone in the journey.

[Mac Malone]

Utensil Song said:

Thanks, after struggling for my experimental C++ FFI project trying to figure out what can be simplified in the lakefile.

If you have the time, please make issues for any missing features or bugs you have found along the way (that do not already have issues for them)!

[Siddhartha Gadgil]

This looks very exciting but I have naive questions. For concreteness, suppose I have fine-tuned a CodeT5 model in pytorch using huggingface trainer. Can I export to ONNX and run this from within Lean using LeanInfer? If not yet then in the foreseeable future?

[Kaiyu Yang]

@Siddhartha Gadgil It shouldn't be difficult to convert the model from Hugging Face to ONNX. However, tokenization might be a problem. The current model used by LeanInfer is from LeanDojo. It is based on ByT5, which does not need tokenization. For CodeT5, however, you would need to run the tokenizer in C++. What tokenizer does CodeT5 use? Is there a way to call it in C++?

[Siddhartha Gadgil]

Thanks. The way I use tokenizers for codet5 and many other models is the transformers command
tokenizer = AutoTokenizer.from_pretrained("Salesforce/codet5-large")

I don't know what tokenizer is actually used. It would be ideal if the AutoTokenizer.from_pretrainedis available so a lot of models can be used.

[Utensil Song]

It seems that the tokenizer can be exported to ONNX together with the trick in Convert Transformers to ONNX with Hugging Face Optimum and maybe run via onnxruntime-extensions as ONNX doesn't define string related operators so it can't run tokenizers natively. But it also seems to be a long shot.

I wonder why didn't LeanInfer choose llama.cpp as its runtime, it actively supports many models out-of-box. And there's even a Lean binding llama.lean (last updated May, so it needs some polish).

[Utensil Song]

Previously I thought finetuning LeanDojo based on Code Llama (particularly Phind-CodeLlama which achieves 73.8% pass@1 on HumanEval) or Star Coder series (particularly StarChat-Beta ) then run its quantized model with llama.cpp via Lean binding is the most natural way to go. But don't know if anyone is working towards this direction, and if not, I'm interested in the rationale.

Lately I came across lean-training-data which seems to be a great addition to LeanDojo's data extraction tool. One could imagine more ways to curate the dataset from there.

[Scott Morrison]

(Aside, yes, sorry, I never wrote an announcement about the availability of lean-training-data, and I'm about to be offline for a few days. I can answer any questions about it next week.)

[Kaiyu Yang]

@Utensil Song I wasn't aware of the possibility of converting a Hugging Face tokenizer to ONNX. I'll take a look. Thanks! Also, many tokenizers are based on tokenization libraries in C++, e.g., sentencepiece. In principle, it's possible to use them in LeanInfer.

However, currently, we don't see empirical evidence that larger models, such as LLaMA or StarCoder, are significantly better than the existing model LeanDojo uses (based on google/byt5-small). We performed some preliminary experiments, but the results were inconclusive. I don't think we should integrate bigger and slower models into Lean (e.g., via LeanInfer) before validating their effectiveness in a more machine learning setting (e.g., LeanDojo).

[Siddhartha Gadgil]

@Kaiyu Yang It would be great if LeanInfer could be made a single interface for integrating a variety of models into Lean. I have no idea how much effort this is (and this is outside my competence) so I cannot tell if it is worth it in that sense. But in planning AI experiments it would be nice to know that if a model works well it can be practically used in Lean.

[Utensil Song]

Kaiyu Yang said:

Utensil Song I wasn't aware of the possibility of converting a Hugging Face tokenizer to ONNX. I'll take a look. Thanks! Also, many tokenizers are based on tokenization libraries in C++, e.g., sentencepiece. In principle, it's possible to use them in LeanInfer.

Yes, indeed, many tokenizers are based on tokenization libraries in C++, and I've checked the source in llama.cpp, particularly how it handles Falcon tokenizer by parsing vocab, and hyperparams of the tokenizer, then reuse a handful of common tokenize functions, it seems that all these can be extracted as a C++ library to handle the tokenization on a per-model basis. The porting time is equivalent or less than training on a new model anyway. So very feasible.

[Kaiyu Yang]

In the long term, we do want LeanInfer to support different models. I don't think there is any fundamental obstacle, though it will need some engineering effort. Currently, it's of relatively low priority on LeanInfer's TODO list, as we plan to have some major improvements and new features coming next month. Nevertheless, we welcome collaboration if anyone wants to work in this direction.

[Utensil Song]

Kaiyu Yang said:

However, currently, we don't see empirical evidence that larger models, such as LLaMA or StarCoder, are significantly better than the existing model LeanDojo uses (based on google/byt5-small). We performed some preliminary experiments, but the results were inconclusive. I don't think we should integrate bigger and slower models into Lean (e.g., via LeanInfer) before validating their effectiveness in a more machine learning setting (e.g., LeanDojo).

Observing no significant performance boost on larger models in simple setting like predicting premises and tactics solely based on local goals is somewhat expected, as this is effectively a simple recommendation algorithm, plus a little microscale organization about how to call the tactics with parameters, small models are sufficient in this case.

Large models might be more expected to perform better when it can make use of informal Math corpus and its corresponding formal forms, the extra context when choosing a premise or a tactic instead of only local goals, and when it's expected to generate a full working proof and its informal walkthrough, given it can interact with Lean multiple rounds to adjust. So in retrospect, I'm actually expecting quite different things for the use of larger models.

[Johan Commelin]

At the moment it doesn't seem trivial to incorporate LeanInfer in regular mathlib development. You need to work on a branch in which you add a new dependency to mathlib, and then remove that dependency when you PR. But if the PR needs more refactoring, you maybe want to add the dep again, etc...
Is there a way that we can make this work more smoothly?

[Mario Carneiro]

and I assume adding the dep also invalidates the cache...

[Adam Topaz]

@Johan Commelin that's one of the main reasons I wanted something like I described here:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Combining.20Envs/near/390758391

[Min-Hsien Weng]

Utensil Song said:

Large models might be more expected to perform better when it can make use of informal Math corpus and its corresponding formal forms, the extra context when choosing a premise or a tactic instead of only local goals, and when it's expected to generate a full working proof and its inform walkthrough, given it can interact with Lean multiple rounds to adjust. So in retrospect, I'm actually expecting quite different things for the use of larger models.

Large language models have become more capable and continue to improve rapidly. I think we could use LLM to do something different, e.g. to rewrite or simplify proofs to make them more concise and readable, or to translate proofs into natural languages for better understanding, or even to explain difficult proofs to people and answer their questions. Interactive LLM systems would open up new possibilities for humans and machines to work together.

[Scott Morrison]

Mario Carneiro said:

and I assume adding the dep also invalidates the cache...

In the long run there are some ideas for this (i.e. import for meta).

But in the meantime, I think we should strongly consider simply adding LeanInfer as a mathlib dependency. It would put an already useful tool into users hands, and give the LeanInfer authors much more feedback.

My understanding is that the LeanInfer authors are very open to working with generic frameworks, and understand that Mathlib would not want to commit to being tied to LeanInfer in particular. (Of course, as LeanInfer will only be used while writing proofs, there won't be any ongoing dependency.)

[Utensil Song]

It's worth noticing that LeanInfer is not building on reservoir. The build process has been quite streamlined as an FFI project, so it's very possible to build with minor tweaks.

Can't see the log details, but reservoir seems to be using this script to build it.

[Kaiyu Yang]

The error may be related to the C++ compiler toolchain used for building the project. Is there a way to access the error log or troubleshoot?

[Utensil Song]

I just realized the log is here

[Kaiyu Yang]

I see segfaults in the log, so maybe it's related to this issue. We can wait for this issue to be fixed and check later.