PaperlayerView exact revision on arXiv

Source-linked AI summary

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar

arXiv:2306.15626v2cs.LGcs.AIcs.LOstat.ML

TL;DR

Learning-based theorem proving has been hindered by private resources, difficult reproduction, and the challenge of selecting premises from large math libraries. LeanDojo provides open tools and data for Lean, while ReProver retrieves premises to guide tactic generation. On a 98,734-theorem benchmark, ReProver proved 51.2% of theorems, exceeding direct tactic generation and zero-shot GPT-4.

  • Problem

    Existing theorem-proving methods are difficult to reproduce because of private code and data, high compute requirements, and limited premise-selection support for novel lemmas.

  • Method

    LeanDojo extracts proof and premise data from Lean and enables programmatic interaction, while ReProver retrieves accessible mathlib premises to condition tactic generation.

  • Results

    51.2% of LeanDojo Benchmark theorems were proved by ReProver, versus 47.6% for direct tactic generation and 29.0% for zero-shot GPT-4.

  • Takeaways & Limitations

    LeanDojo provides open-source, reproducible baselines for retrieval-augmented theorem proving, trained in five days on a single GPU and released without private datasets.

  • Takeaways & Limitations

    Direct comparison with existing Lean LLM provers was infeasible because they were not open-source or reproducible with reasonable effort.

Abstract

from arXiv · show

Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: an open-source Lean playground consisting of toolkits, data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection: a key bottleneck in theorem proving. Using this data, we develop ReProver (Retrieval-Augmented Prover): an LLM-based prover augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. Furthermore, we construct a new benchmark consisting of 98,734 theorems and proofs extracted from Lean's math library. It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research.

1 Introduction

LeanDojo addresses reproducibility barriers in learning-based theorem proving by providing open-source tools, data, models, and benchmarks for Lean. Its ReProver system combines premise retrieval with tactic generation and outperforms specified non-retrieval and GPT-4 baselines.

  • Automated theorem proving supports formal mathematics and formal verification, while interactive theorem proving lets models learn proof-assistant interactions from human-written proofs.
  • Existing LLM-based theorem provers face barriers from private code and data, high compute requirements, and infrastructure that is difficult to reproduce.
  • LeanDojo extracts proof trees and premise annotations from Lean while enabling models to observe states, execute tactics, and interact with the proof environment programmatically.
  • Premise selection is difficult because mathlib contains hundreds of thousands of definitions and theorems, while all possible premises exceed LLM context windows and unseen lemmas challenge memorization.
  • ReProver retrieves a small set of mathlib premises for each proof state and conditions an encoder-decoder Transformer on them to generate the next tactic.
  • LeanDojo Benchmark contains 98,734 mathlib theorems and proofs, with splits requiring generalization to premises never used during training.
  • 51.2% of LeanDojo Benchmark theorems were proved by ReProver, versus 47.6% for direct tactic generation and 29.0% for zero-shot GPT-4.
  • ReProver training took five days on one GPU and proved 26.5% of MiniF2F theorems, 13.8% of ProofNet theorems, and 65 previously unproved Lean theorems.

2 Related Work

Related work spans classical, graph-based, and Transformer theorem provers, premise-selection systems, proof-assistant tools, and natural-language mathematical reasoning. LeanDojo is distinguished by public premise extraction and robust Lean interaction for retrieval-augmented proving.

  • Theorem Proving: Learning-based theorem proving has progressed from KNN and graph neural networks to Transformer-based LLMs, alongside advances in proof search, reinforcement learning, auxiliary data, and classical-prover integration.
  • Premise Selection: Premise-selection research has used classical models, recurrent networks, graph networks, and Transformers, but often separates retrieval from theorem proving or feeds premises to symbolic provers.
  • Data and Tools for Theorem Proving: Existing proof-assistant tools and datasets cover Coq, Isabelle, HOL Light, and Lean, while MiniF2F provides a cross-system evaluation set with 488 theorems.
  • Data and Tools for Theorem Proving: LeanDojo is the only listed tool that extracts premises for retrieval-augmented theorem proving, interacts robustly with Lean, and extracts data from Lean 4.
  • Mathematical Reasoning in Natural Language: Natural-language mathematical reasoning includes autoformalization, which translates natural-language texts into formal theorems and proofs, whereas this paper focuses on formal logic.
  • Retrieval-Augmented Language Models: ReProver adapts retrieval-augmented architectures to formal theorem proving by retrieving premises accessible to the current Lean file rather than generic code corpora.

3 Background: Theorem Proving in Lean

Lean combines programming, mathematical definitions, theorem statements, and machine-checkable tactic proofs. Proving in Lean requires navigating an unbounded tactic space and selecting valid premises from a large, import-constrained library.

  • Lean is a functional programming language with dependent types that supports conventional programs, mathematical objects, theorems, and proofs.
  • Lean’s tactic system constructs machine-checkable proofs semi-automatically, and tactics can be extended as programs in a domain-specific language.
  • The gcd_self proof uses mod_self from another imported file, illustrating why selecting among hundreds of thousands of library premises is a central bottleneck.
  • In the gcd example, Lean defines gcd recursively, proves gcd_zero_left, and states gcd_self: ∀n ∈N, gcd n n = n, using five tactics.
  • The tactic action space is discrete, combinatorial, and unbounded, making theorem proving challenging for machine learning.
  • Premises are existing lemmas or definitions used as tactic arguments, but proofs may use only premises defined and imported in the current file.

4 LeanDojo: Toolkit and Benchmark

LeanDojo extracts structured training data from Lean and provides programmatic interaction with the proof assistant. It also supplies a large benchmark designed to test generalization beyond memorized similar proofs.

  • Toolkit: LeanDojo extracts file dependencies, ASTs, proof states, tactics, and premise definitions or uses from Lean repositories.These annotations expose information unavailable in raw Lean code, including intermediate proof states and fully qualified premise names.
  • Toolkit: LeanDojo modifies Lean to resolve premises’ full names and locate their definitions during data extraction without changing evaluation Lean.The modified system is used only for extraction, preserving the logical soundness of the evaluation environment.
  • Benchmark: LeanDojo Benchmark contains 98,734 theorems from 3,384 mathlib files and includes definitions of 130,262 premises.The benchmark supports both premise selection and theorem proving across topics including analysis, algebra, and geometry.
  • Benchmark: The novel_premises split requires each testing proof to use at least one premise never used in training, preventing easy transfer from paired similar proofs.Random splits can overestimate performance because similar theorems may have identical proofs; the benchmark uses 94,734/2,000/2,000 training/validation/testing theorems.
  • Toolkit: LeanDojo turns Lean into a gym-like environment where models observe proof states, execute tactics, and receive error or completion feedback.Its interface includes theorem initialization and tactic execution, while failed states remain failed under subsequent execution.

5 ReProver: Retrieval-Augmented Theorem Prover

ReProver combines premise retrieval with tactic generation: it retrieves potentially useful accessible premises for each proof state and conditions tactic generation on them. Its retriever adapts DPR through accessibility analysis and in-file hard negatives.

  • Model: ReProver retrieves potentially useful premises for the current proof state and conditions tactic generation on the state-premise concatenation.At each step, multiple tactic candidates are generated and searched with a standard best-first algorithm.
  • Premise Retrieval: The DPR-based retriever embeds proof states and premises, ranking candidates by cosine similarity in a shared vector space.Premise embeddings can be precomputed, while each query requires one forward pass and no separate reranking pass.
  • Premise Retrieval: Restricting retrieval to premises accessible to the theorem narrows the candidate library from an average of 128K premises to 33K.Accessible premises include earlier definitions in the same file and premises imported from other files.
  • Retriever Training: ReProver trains its retriever with positive premises and in-batch negatives, including a deliberate mixture of in-file and random negative examples.The in-file negatives address early errors in which randomly sampled training negatives caused retrieval of other premises from the positive premise’s file.
  • Tactic Generation: An encoder-decoder ByT5 model generates human-written tactics from retrieved premises and the proof state using cross-entropy training.The implementation builds on google/byt5-small, avoiding domain-specific pretraining and using substantially less compute than prior methods.

6 Experiments

Experiments evaluate ReProver on premise selection and theorem proving using the LeanDojo Benchmark and external datasets. ReProver outperforms the reported baselines, while challenging splits remain substantially harder.

  • Premise Selection: ReProver outperforms BM25 and both ablations on premise selection across random and novel_premises splits.The ablations retrieve from all premises or omit in-file negatives, isolating the two retrieval improvements.
  • Theorem Proving: ReProver uses a two-stage setup: retrieve 100 premises, train a tactic generator on state-premise inputs, then apply best-first search during evaluation.Theorem-proving performance is measured with Pass@1 on LeanDojo Benchmark testing data.
  • Limitations: Direct comparison with existing Lean LLM provers is infeasible because their code and pretraining data are private and their settings differ.The paper instead releases code and models as accessible baselines for future work.
  • Theorem Proving: ReProver outperforms tidy, GPT-4, and a direct tactic-generation baseline on both LeanDojo Benchmark data splits.The authors report that GPT-4 performs substantially worse despite possible exposure to ground-truth proofs through data contamination.
  • Generalization: All methods perform substantially worse on novel_premises than on the random split, making the challenging split more indicative of prover capability.The degradation reflects the requirement to generalize to testing proofs using premises absent from training.
  • External Evaluation: On MiniF2F, ReProver achieves 26.5% Pass@1, and on ProofNet it achieves 13.8% Pass@1.It also discovers 33 MiniF2F proofs and 39 ProofNet proofs without existing Lean ground-truth proofs.

7 Conclusion

LeanDojo is an open-source Lean playground that combines data extraction, programmatic interaction, and retrieval-augmented theorem proving. Its environment addresses reliability problems in prior Lean interaction tools while supporting premise-aware learning.

  • Conclusion: LeanDojo provides an open-source playground with toolkits, models, and benchmarks for learning-based theorem proving in Lean.It extracts data from Lean and enables models to interact with Lean programmatically.
  • Extracting Premise Information: LeanDojo traces premise names and definitions through Lean’s elaboration and namespace resolution, enabling accurate premise information for retrieval.Premises can be referred to by short names while Lean resolves them to unique fully qualified names.
  • Reliable Interaction: The benchmark study used Lean v3.42.1 and a specified mathlib revision, and documented examples from the remaining 1.4% of errors.The evaluation entered extracted tactic-style proofs into both lean-gym and LeanDojo.

A.3 Comparison with Existing Tools for Learning-Based Theorem Proving in Lean

LeanDojo unifies data extraction and programmatic Lean interaction, while earlier tools provide only one of these functions and lack support for current Lean ecosystems. Its extraction pipeline records premise-linked proof data and structured source metadata.

  • Functionality: LeanDojo supports both data extraction and programmatic Lean interaction, whereas LeanStep supports extraction and lean-gym supports interaction.The earlier tools were not actively maintained and did not support recent mathlib versions.
  • Implementation: LeanDojo uses Lean’s built-in mechanisms to export ASTs and proof trees, avoiding LeanStep’s ad-hoc Python parser and tactic-logging reconstruction.LeanStep’s implementation is described as brittle and incompatible with current Lean/mathlib versions.
  • Functionality: LeanDojo supports Lean 4, recent mathlib, and repositories beyond mathlib, unlike LeanStep and lean-gym in the comparison.The comparison table reports Lean 4 support and recent mathlib support only for LeanDojo.
  • Reliability: LeanDojo reports 1.4% estimated interaction errors versus 21.1% for lean-gym, while the table lists documentation and unit tests only for LeanDojo.The authors attribute lean-gym’s errors to mishandled namespace semantics during environment construction.
  • Benchmark Data: The benchmark records theorem tactics with proof states before and after each tactic, including premise annotations such as the resolved full name and definition path.The example records the premise pi_pos used by linarith.
  • Benchmark Data: Not all theorems have tactic-style proofs, so concatenated tactics may not reconstruct complete original proofs, although this does not affect evaluation or tactic-generator training.The limitation concerns proof reconstruction rather than the stated theorem-proving uses.

B.2 Datasheet

The LeanDojo Datasheet documents a self-contained benchmark of formal Lean definitions, theorems, and proofs, together with its provenance, licensing, and intended uses. The supplied implementation passages also describe the model components and evaluation search procedure.

  • Dataset Purpose: LeanDojo Benchmark was created as a benchmark for learning-based theorem proving in Lean and contains formal definitions, theorems, and proofs.The dataset was created by the paper’s authors.
  • Dataset Contents: 98,734 theorems and proofs and 130,262 premises are defined across 3,384 files.The dataset includes all extractable theorems and proofs from the specified mathlib commit.
  • Dataset Structure: Definitions are explicitly linked to the proofs that use them as premises, supporting premise-selection and theorem-proving tasks.The dataset has been used to train and evaluate machine-learning models on both tasks.
  • Data Collection: The dataset is self-contained, generated by building a Lean repository with modified Lean and postprocessing exported data.No manual effort was involved in collection, and the final version was generated in October 2023.
  • Distribution: LeanDojo Benchmark is released under CC BY 2.0, while the LeanDojo extraction and interaction tool is released under the MIT license.The dataset is hosted on Zenodo and the code, documentation, and model checkpoints are publicly distributed.
  • Model and Evaluation: ReProver uses a ByT5-based retriever and tactic generator, with retrieval restricted to premises accessible to the current file through LeanDojo’s program analysis.Evaluation combines the tactic generator with best-first search and 64 beam-search tactic candidates per step.

C.4 Evaluation on MiniF2F and ProofNet

ReProver was evaluated on MiniF2F and ProofNet to test theorem proving outside its training distribution. It achieved competitive MiniF2F performance and produced new Lean proofs on both benchmarks, but comparisons are constrained by differing setups.

  • MiniF2F: 26.5% Pass@1 on MiniF2F was competitive with the 25.9% non-reinforcement-learning baseline.ReProver was evaluated on the test set using the specified MiniF2F commit.
  • MiniF2F: ReProver proved 33 MiniF2F theorems that previously lacked Lean proofs.The authors provide the complete list of these new proofs in a pull request.
  • Comparison Caveats: MiniF2F comparisons are limited by different interaction tools, training regimes, evaluation metrics, and proof-assistant settings.ReProver uses supervised learning and Pass@1, while some prior work uses reinforcement learning or Pass@64.
  • ProofNet: ReProver proved 48 of 349 ProofNet theorems, achieving 13.8% Pass@1.This was reported as the first theorem-proving result on ProofNet.
  • ProofNet: 39 of ReProver’s 48 proved ProofNet theorems lacked existing Lean proofs, and three required premise retrieval.The contributed proofs helped reveal and fix formalization problems in seven theorems.

D LeanDojo for Lean 4

LeanDojo fills a Lean 4 tooling gap by extracting proof-related data and supporting programmatic interaction. Its LeanDojo Benchmark 4 provides a large evaluated corpus with random and novel-premises splits.

  • LeanDojo fully supports Lean 4, for which no existing data-extraction tool or learning-based theorem-proving work was known.
  • LeanDojo extracts file dependencies, ASTs, proof states, tactics, and premise information from Lean 4 repositories.
  • LeanDojo Benchmark 4 contains 102,514 theorems/proofs, 213,067 tactics, and 152,695 premises from mathlib4.
  • The benchmark allocates 2,000 theorems each for validation and testing, with the remainder used for training.
  • LeanDojo Benchmark 4 includes random and novel_premises data splits for training and evaluation.

E ChatGPT Plugin for Theorem Proving

LeanDojo exposes Lean through a ChatGPT plugin that lets users request theorem proofs and interact with proof states. The examples show useful mathematical explanations and error interpretation, alongside frequent failures and hallucinated success claims.

  • The plugin lets ChatGPT prove user-specified theorems by initializing proof searches and executing tactics through LeanDojo.
  • Users provide a theorem name and file path, after which ChatGPT receives proof states and state IDs through the plugin APIs.
  • ChatGPT can explain tactic choices in natural language, interpret Lean error messages, and backtrack to previous proof states.
  • The examples include ChatGPT-3.5 and GPT-4 interactions, with captions documenting step-by-step proof attempts.
  • ChatGPT failed on most tested theorems, commonly hallucinating success and struggling to search systematically or backtrack from unpromising paths.
  • The study is exploratory because theorem contamination is likely and plugin-based quantitative evaluation is difficult.

F Limitations and Future Work

The paper identifies limitations in its model scale, tokenizer, retrieval architecture, training data, and ChatGPT evaluation, while outlining several directions for improvement. These include stronger models, better retrieval fusion, auxiliary or interactive data, and improved search strategies.

  • The paper prioritizes simplicity and efficiency over maximizing performance across the many components of a learning-based prover.
  • ByT5 has 299M parameters, and stronger open-source code models are proposed as potential future backbones.
  • Byte-level sequences are unnecessarily long, harming efficiency because Transformer cost scales quadratically with sequence length.
  • GPT-4 and ChatGPT do not solve theorem proving out of the box and remain far behind finetuned models under the paper's preliminary prompting strategy.
  • With a 2,300-token limit, ReProver fits only 10–15 retrieved premises, motivating hidden-space fusion architectures such as Fusion-in-Decoder.
  • The paper suggests auxiliary data, online interaction, generative retrieval, and stronger search strategies as directions for overcoming current limitations.
  • LeanDojo's 98,734 human-written proofs are scarce for data-hungry LLMs and omit the intermediate trial-and-error history of interactive proving.
Loading 2306.15626v2…