What is the best way to evaluate theorems and proofs generated by a LLM in LeanDojo?

[brando90]

In general I want to know how to verify if a theorem generated from a LLM is true in Lean Dojo using a prover.

More details:
I want to build a static eval benchmark for my autoformalization projects using LeanDojo and a Prover (e.g., linarith,LeanHammer, ReProver).
For this the AF LLM model will output formal string that will be made into proofs of the form formal_stmt_mdl_af ===_prover formal_stmt_ground_truth and I want to be able to check if the two are equivalent using some prover (essentially using a Prover to prove equivalences). Initially anything that makes the code run and is simple is likely good. Basically using a prover to prove equivalences).

Given all the engineering efforts in LeanDojo I wasn't 100% sure how to start this. Is the right level of abstraction to think of LeanDojo as an Lean env I can give two formal strings to check if they are equivelent using some powerful prover e.g., equiv(f_stmt1, f_stmt2, prover, env=LeanDojo)? Or does LeanDojo work better by processing things in bulk? Or maybe due to the complexity of LeanDojo and the engineering efforts, there might be another detail/unknown I'm not even aware of.

Note, I have seen https://github.com/lean-dojo/LeanDojo/blob/main/scripts/generate-benchmark-lean4.ipynb and read around the docs and repo and realized the project is complex, so wanted to ask before spending to much time on any approach.

Thanks in advance!

[yangky11]

Hi Brando,

If I'm understanding it correctly, by "proving two theorems equivalent", you have two theorems, A and B and want to prove A => B /\ B => A?

You can certainly enter this theorem into LeanDojo and apply various tactics to it. However, how do you plan to prove the theorem? In general, it is quite hard to prove if two theorems are equivalent, and I don't think any existing proof automation in Lean (linarith or ReProver) comes even close to that. Also, there is no hammer in Lean as of now.

[brando90]

Hi Kaiyu,

Yes, I want to do that experiment and see how for current provers take us. It's ok if it fails, I can figure out what to do if it fails. What I really need is to know as a first step what is your recommended way to give LeanDojo this type of statement (i.e., formal statements created by a LLM/model). I can imagine different options but given the complexity of Lean Dojo I wanted to ask before I dive into a (wrong) rabit hole. I'd try whatever Prover is easiest to run initiialy, any is fine e.g., linarith, ReProver, LeanHammer.

So my main question is: what is your recommended way to use Lean Dojo for verifying statements (knowing the string might be created by an LLM)?

One thing that would be nice is if it fits int he HF evaluate framework https://huggingface.co/docs/evaluate/index but idk if that's a good constraint to put on myself.

[yangky11]

I'd recommend using LeanDojo as a REPL. If you look at "Interact through Commands" at the end of https://github.com/lean-dojo/LeanDojo/blob/main/scripts/demo-lean4.ipynb, it allows you to navigate to any position in a Lean source file and run commands. For example, if your ground truth theorem is A, and the autoformalization model outputs B, you can run the command theorem equiv : A <-> B in LeanDojo, which provides feedback if the theorem statement is not valid.

If the theorem is valid, then you would want to enter tactic mode and try to prove the theorem. For this part, I'm not sure if LeanDojo can readily do that, but I'm happy to help implement this feature if needed.

[yangky11]

Have you ever used LeanHammer? I'm not sure if it's a working system. As far as I know, the Lean FRO is eagerly trying to hire someone to implement the hammer for Lean.