LLMLean, anyone using it?

Stream: Machine Learning for Theorem Proving

[Jason Rute]

Has anyone tried out LLMLean, either locally or via an API? I'm curious if it is any good? In particular, I'm curious about the following:

• Does it fill in the kinds of proofs you would like an AI to fill in for you? (Especially in comparison to similar tools like Lean Copilot, or the general purpose coding copilots?)
• Is it easy to install?
• Does the answer to the first two questions matter if you are using the local or API version?
• If using the API version, is it quickly going through your API credits? (I assume llmqed is doing an expensive search, but I'm not sure. Maybe the parameters suggest llmqed has a fairly low limit on the number of model calls.)

[Bolton Bailey]

I would try updating my lean toolchain for my project and installing it now, but it seems it's on the leanprover/lean4:v4.11.0-rc1 toolchain and mathlib is now on leanprover/lean4:v4.11.0, so will it even be possible to use?

[Kim Morrison]

Those toolchains are fairly compatible. Most of the changes are bugfixes around the variable command, so if that is not used much you may be lucky.

[Bolton Bailey]

Ok yes, got it working with no changes, thanks!

Frankly I'm unimpressed with it though. llmqed is failing to find a proof for a a subgoal with hk_pos : 0 < k ⊢ k ≠ 0 in the context

[Jason Rute]

@Bolton Bailey Is that running it locally via ollama or through an OpenAI API? Also, is that the full goal, or is the 0 < k buried in there among other elements?

[Bolton Bailey]

That is running locally through Ollama, entirely possible that a more powerful LLM would be more consistent.
@Sean Welleck is there any way using a Local LLM to let the LLM crank through more trials to potentially get more consistent results?

[Bolton Bailey]

is that the full goal,

It is also buried among other elements, so understandable that the LLM would get confused, but still not exactly encouraging, since I feel most contexts I am in the final steps of closing do have a bunch of now-irrelevant hypotheses.

I am also noticing that llmqed is not really working even with this as the full goal, ie

import Mathlib
import LLMlean

example (x : ℕ) (h: ¬ x = 0) : 1 ≤ x := by
  llmqed -- sometimes gives no suggestions, sometimes one or two step candidates, but doesn't ever close the goal

[Bolton Bailey]

I am also seeing that it never suggests more than one step at a time, I wonder if I am using it wrong?

[Sean Welleck]

Thanks for trying it out! If you're using the default ollama model, it's fine-tuned for tactic prediction (the llmstep tactic). For llmqed you may see more success with Open AI.

Here's what llmqed with the Open AI API gives for your example:

llmqed.png

[Sean Welleck]

To control the number of trials, you can use the LLMLEAN_NUMSAMPLES environment variable (ref).

[Jason Rute]

Sean Welleck said:

If you're using the default ollama model, it's fine-tuned for tactic prediction (the llmstep tactic). For llmqed you may see more success with Open AI.

This may be good to add to the documentation.

[Jason Rute]

Sean Welleck said:

To control the number of trials, you can use the LLMLEAN_NUMSAMPLES environment variable (ref).

Is there a reason this couldn't just be added as an optional parameter to the llmqed tactic? Of course, you could still change the default with a command line parameter (or an option configurable with set_option).

[Jason Rute]

Also, does your code generalize to other public API models like those of Mistral, Anthropic, etc? (Or is there something special about OpenAI, such as using a fine-tuned OpenAI model or a prompt specific to OpenAI?) Also, would it be easy to incorporate the new DeepSeek-Prover models?

[Jason Rute]

And a very silly question (for anyone here), how do you set env variables when running Lean in VS Code?

[Adam Topaz]

if you spawn a process then IO.Process.SpawnArgs has a field for environment variables.

[Jason Rute]

@Adam Topaz I think I’m talking about the other direction. LLMlean is using IO.getEnv to read the environmental variables (not to set them for a subprocess). But since Lean runs in VSCode it is not exactly clear to me (or other people probably) how to set these so that the LLMLean tactics can read them. (Also, I don’t necessarily think this is the ideal way to change settings for a tactic. It might be fine for private data like an API key, that you don’t want to leak into your repo, but not for the number of samples to generate.)

[Adam Topaz]

The usual way to set env variables is by modifying your profile file (at least on Linux, I have no idea what windows does). Is that what you’re asking?

[Adam Topaz]

I don’t know how to do this within vscode or if it’s even possible

[Julian Berman]

@Jason Rute the 'easiest' way I think is "start VSCode from your shell rather than a graphical menu". (I say this not being a VSCode user but having helped someone do this previously)

[Julian Berman]

But undoubtedly VSCode has some way of configuring what environment it spawns processes in -- the thing is yeah, it will require figuring out whether that happens before or after it spawns the language server, and which kind of shell it spawns (if any -- which hopefully is 'none' by default), and ...

[Julian Berman]

That being said, something like this stackoverflow thread and answer seem to have some details if you want to get it working in other ways

[Adam Topaz]

It looks like this can be accomplished by modifying the launch configuration of vscode: https://code.visualstudio.com/docs/editor/debugging#_launch-configurations

[Adam Topaz]

but it also seems that this is primarily for debugging purposes.

[Sean Welleck]

We used to be able to easily set environment variables in the VS Code settings, but this functionality disappeared from VS Code at some point

Here's a screenshot from the old LLMLean docs before this feature was removed from VS Code:
env_example1.png

[Sean Welleck]

Now I add the environment variables to .bashrc (or .zshrc) and restart VS Code

[Phoebe Bai]

image.png
I got a stupid question, after i import"LLMlean" and write the tactic"llmstep", it stay still for such a long time , and i can't get any output. Can someone tell me why?