The team used LeanDojo Benchmark to train and evaluate a model called ReProver. During testing, the tactic generator is combined with best-first search to search for complete proofs. The results showed that ReProver outperforms Lean's built-in proof automation tactic and other baselines. They also built a LeanDojo ChatGPT plugin that enables ChatGPT to prove theorems by interacting with Lean. However, it struggles to find correct proofs in most cases, due to weakness in search and planning.
Key takeaways:
- LeanDojo is a tool that uses language learning models (LLMs) to automate theorem proving in Lean, a mathematical proof assistant. It can suggest tactics and search for proofs, and users can use their own models either locally or on the cloud.
- The LeanDojo system extracts proofs in Lean into datasets for training machine learning models. It also enables the trained model to prove theorems by interacting with Lean's proof environment.
- LeanDojo provides a gym-like environment for the prover to observe the proof state, run tactics to change the state, and receive feedback on errors or proof completion. This environment is crucial for evaluating, deploying, or training the prover.
- LeanDojo has been used to train and evaluate a model called ReProver, which outperforms Lean's built-in proof automation tactic and other baselines. It has also been used to discover new proofs and uncover bugs in the formalization of theorem statements.