PaperlayerView exact revision on arXiv

Source-linked AI summary

TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang

arXiv:2407.03203v2cs.FLcs.AI

TL;DR

Scarce NL-FL aligned data and limited methods constrain training general-purpose LLMs to write Lean4 proofs from natural-language guidance. TheoremLlama builds bootstrapped aligned data and trains a prover with complementary techniques; it reports higher MiniF2F accuracy than GPT-4.

  • Problem

    There is no large-scale NL-FL aligned dataset for Lean4 and no universally recognized method for training LLMs to generate whole proofs directly.

    Source: §4.1 · p. 9

  • Method

    TheoremLlama creates the OBT NL-FL aligned, bootstrapped dataset and trains a general-purpose LLM using block training, curriculum sorting, and iterative proof writing.

    Source: §2.2.3 · p. 5, §5 · p. 9

  • Results

    36.48% on MiniF2F-Valid and 33.61% on MiniF2F-Test; TheoremLlama surpasses GPT-4 and Gemini-1.5 baselines.

    Source: §5 · p. 9

  • Takeaways & Limitations

    OBT provides an NL-FL aligned, bootstrapped dataset for training an LLM Lean4 prover.

    Source: §5 · p. 9

    TheoremLlama and other formal provers struggle with difficult IMO-level problems, and the paper does not explore RL or Lean feedback for refining incorrect proofs.

    Source: Limitations · p. 9

Abstract

from arXiv · show

Proving mathematical theorems using computer-verifiable formal languages like Lean significantly impacts mathematical reasoning. One approach to formal theorem proving involves generating complete proofs using Large Language Models (LLMs) based on Natural Language (NL) proofs. However, due to the scarcity of aligned NL and Formal Language (FL) theorem-proving data most modern LLMs exhibit suboptimal performance.This scarcity results in a paucity of methodologies for training LLMs and techniques to fully utilize their capabilities in composing formal proofs. To address these challenges, this paper proposes TheoremLlama, an end-to-end framework that trains a general-purpose LLM to be a Lean4 expert. TheoremLlama includes NL-FL dataset generation and bootstrapping method to obtain aligned dataset, curriculum learning and block training techniques to train the model, and iterative proof writing method to write Lean4 proofs that work together synergistically. Using the dataset generation method in TheoremLlama, we provide Open Bootstrapped Theorems (OBT), an NL-FL aligned and bootstrapped dataset. Our novel NL-FL bootstrapping method, where NL proofs are integrated into Lean4 code for training datasets, leverages the NL reasoning ability of LLMs for formal reasoning. The TheoremLlama framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets respectively, surpassing the GPT-4 baseline of 22.95% and 25.41%. Our code, model checkpoints, and the generated dataset is published in GitHub

1 Introduction

The paper targets the difficulty of generating Lean4 proofs from natural-language guidance amid scarce aligned data and limited Lean4 familiarity. It proposes TheoremLlama, combining aligned-data generation, training techniques, and iterative proof writing.

1 Introduction

  • Lean4 few-shot performance remains unsatisfactory, with concise formal code, confusing Lean3 pretraining data, and scarce NL-FL alignment identified as challenges.The paper focuses on generating Lean4 proofs guided by natural-language proofs.Source: §1 · p. 2
  • TheoremLlama combines NL-FL dataset generation, Lean4 prover training, and iterative proof writing in an end-to-end framework.The framework is designed to transform a general-purpose LLM into a Lean4 expert.Source: §1 · pp. 2–3
  • The data pipeline informalizes Mathlib4 theorems using retrieved examples, then embeds natural-language reasoning into Lean4 code to create OBT.The examples are retrieved with a fine-tuned T5 encoder, and Gemini-1.5 produces informalizations.Source: §1 · p. 2, Figure 1 · p. 2
  • Block training supports in-context learning, while curriculum sorting orders training data from easier to harder examples.The framework also iteratively reuses correct proofs as in-context examples.Source: §1 · p. 2
  • 36.48% on MiniF2F-Valid and 33.61% on MiniF2F-Test; TheoremLlama surpasses the reported GPT-4 baselines.The framework also includes ablation studies of major dataset-generation and training components.Source: §1 · p. 3
  • The paper releases the OBT dataset, model checkpoints, and code; fine-tuning takes about 32 hours on an 8-GPU A6000 machine.The authors present this GPU footprint as supporting lower barriers for academic researchers.Source: §1 · p. 3

2 Methodology

The methodology trains a general-purpose LLM to generate whole Lean4 proofs guided by natural-language proofs. It constructs bootstrapped aligned data, trains with block and curriculum techniques, and iteratively reuses verified proofs as examples.

2.1.1 Lean4 Proof Extration

  • Mathlib4 supplies the Lean4 theorem proofs for OBT, a dataset containing 106,852 NL-FL aligned and bootstrapped theorems.Mathlib4 is described as a repository of high-quality, human-crafted proofs.Source: §2.1 · p. 3, §2.1.1 · p. 3

2.1.2 Informalization with Example Retrival

  • A ByT5 encoder aligns NL and Lean4 theorem statements and retrieves similar examples for Gemini-1.5 informalization; filtering yields 106,852 theorems.The authors remove repeated, overlength, and other erroneous generations.Source: §2.1.2 · p. 4

2.1.3 NL-FL Bootstrapping

  • NL-FL bootstrapping embeds natural-language proofs as comments in Lean4 code, then checks that removing comments restores the original code.The approach is intended to help LLMs use NL reasoning while writing formal proofs.Source: §2.1.3 · p. 4

2.2 LLM Prover Training

  • The training section proposes block training and curriculum data sorting as instruction fine-tuning techniques for formal reasoning.The paper frames these techniques as responses to limited training methods for NL-guided whole-proof generation.Source: §2.2 · p. 4

2.2.1 Block Training

  • Block training treats tokenized records as a text ring and fills context with previous examples to train in-context learning for Lean4 proofs.Each record pairs natural-language input with its corresponding bootstrapped Lean4 code.Source: §2.2.1 · pp. 4–5

2.2.2 Curriculum Data Sorting

  • Curriculum Data Sorting orders proofs by the number of steps needed to solve their goals, from easier examples to harder ones.The authors report that this stabilizes the training loss curve and improves prover performance.Source: §2.2.2 · p. 5

2.2.3 Instruction Fine-tuning

  • Instruction fine-tuning takes a natural-language theorem statement and proof plus a Lean4 statement as input, targeting a bootstrapped Lean4 proof.Examples fill context windows, and the target includes natural-language explanations.Source: §2.2.3 · p. 5

2.3 Iterative Proof Writing

  • Iterative proof writing adds the prover’s Lean-verified proofs as examples in later iterations, stopping at a step limit or when no new theorems are proved.The authors say same-dataset examples can mitigate distribution shifts between generated and real-world natural-language statements and proofs.Source: §2.3 · p. 5

3 Experiments

The experiments evaluate TheoremLlama on MiniF2F and compare it with tree-search, few-shot, and math-specialist baselines. They report stronger benchmark results, component ablation effects, iterative-proof gains, retrieval behavior, and a generated-proof case study.

3.1.1 Dataset and Task

  • The 488 MiniF2F problems span MATH, high-school competitions, and manually crafted questions; TheoremLlama trains on 106,852 OBT theorems for about 32 hours on eight A6000 GPUs.The proof-generation task uses Lean4 and natural-language statements and proofs with up to 16 in-context examples.Source: §3.1.1 · pp. 5–6, §3.2 · pp. 6–7

3.1.2 Baseline

  • Baselines include tree-search provers, few-shot general LLMs, and math-specialist models; tree-search methods use pass@1 under comparable inference costs.The authors note that no universally approved baselines exist for this task and that direct comparison with Isabelle methods is infeasible.Source: §3.1.2 · p. 6

3.3 Results

  • 36.48% on MiniF2F-Valid and 33.61% on MiniF2F-Test are TheoremLlama’s cumulative accuracies, surpassing all baselines.Table 1 reports 128 generation rounds for other LLMs and cumulative results across multiple proof iterations for TheoremLlama.Source: Table 1 · p. 6, §3.3 · p. 7
  • Tree-search methods average 27.2% accuracy, while TheoremLlama also outperforms math-expert models; Gemini performs best among the baselines.The authors report similar Test and Valid accuracy for un-finetuned Llama3-8B-Instruct and GPT-4, and interpret this as evidence that modern LLMs are under-trained on Lean4 reasoning.Source: §3.3 · p. 7

3.4 Ablation Studies

  • Removing any of four components—NL guidance, NL-FL bootstrapping, block training, or curriculum sorting—reduces performance; the ablations attribute drops to lost guidance, proof tracking, or training-test mismatch.Without NL guidance, the fine-tuned model does not outperform the untrained model; without block training, training lacks the in-context information present at test time.Source: §3.4 · p. 7

3.5 Iterative Proof Writing study

  • Using examples from the same dataset for iterative proof writing increases pass rate by 2%, which the authors say reduces the test-example distribution gap to some extent.The study compares different rounds of iterative proof writing.Source: §3.5 · p. 8, Table 3 · p. 8

3.6 Effectiveness of Example Retrieval

  • The retriever largely distinguishes similar from different NL and Mathlib4 statements; a generated case proof uses sq_nonneg and linarith with in-code NL guidance.The case study is presented as qualitative validation of NL guidance and NL-FL bootstrapping.Source: §3.6 · p. 8, §3.7 · p. 8

4 Related work

Prior formal-reasoning work includes theorem search, few-shot whole-proof generation, and attempts to build aligned data, but large-scale NL-FL alignment remains unavailable. The paper also situates OBT within broader dataset-generation approaches that use existing data and LLM knowledge.

4.1 Formal Reasoning

  • Formal-reasoning methods include KNN, GNN, tree-search provers, and few-shot whole-proof generation, but no large-scale NL-FL aligned dataset exists and no universally recognized whole-proof training method has emerged.The cited aligned-dataset attempts include Azerbayev et al. (2023a) and Ying et al. (2024).Source: §4.1 · pp. 8–9

4.2 Dataset Generation

5 Conclusion

TheoremLlama combines the OBT dataset with training and proof-writing methods to turn general-purpose LLMs into Lean4 experts. It reports results above the GPT-4 and Gemini-1.5 baselines on MiniF2F.

5 Conclusion

  • TheoremLlama combines NL-FL dataset generation, block training, curriculum data sorting, and iterative proof writing with the OBT training dataset.The framework is presented as a way to transform a general-purpose LLM into a Lean4 expert.Source: §5 · p. 9
  • NL-FL bootstrapping integrates natural-language proofs into generated data to help transfer LLMs’ natural-language reasoning to Lean4 proof writing.Source: §5 · p. 9
  • 36.48% and 33.61% of the theorems were proved on MiniF2F-Valid and Test, respectively, surpassing the GPT-4 and Gemini-1.5 baselines.The passage does not give baseline values.Source: §5 · p. 9

6 Discussion

TheoremLlama presents a framework for applying modern LLMs to corner cases where data is lacking, including formal reasoning.

6 Discussion

  • TheoremLlama combines ways to leverage incomplete data, train LLMs for unfamiliar tasks, and improve their performance in applications.The discussion presents this framework as potentially relevant beyond formal reasoning, for LLM corner cases with data scarcity.Source: §6 · p. 9

Limitations

The authors identify limits in solving technically difficult problems and in integrating Lean feedback into proof generation. They also note a risk that formalization may mask errors in natural-language proofs.

Limitations

  • Existing formal provers, including TheoremLlama, struggle with difficult IMO-level problems, and the authors say LLMs lack understanding of intricate technical aspects of human proofs.Source: Limitations · p. 9
  • The paper does not explore online-interaction RL or Lean feedback to refine incorrect proofs, citing Lean4 kernel complexity and the need for deeper Lean–Python integration.Source: Limitations · p. 9
  • A natural-language-guided Lean4 prover may automatically correct errors in natural language, risking that wrong natural-language proofs are treated as correct and propagated.Source: Limitations · p. 10

A Confusing Lean3 Data in LLM Pre-train

The authors report that LLMs can produce Lean3 syntax despite prompts to use Lean4, and attribute this behavior to Lean3-heavy pretraining. TheoremLlama uses Lean4 data during instruction fine-tuning to reduce the problem.

A Confusing Lean3 Data in LLM Pre-train

B Case Study

The case studies illustrate how NL guidance supports formal proof construction, from algebraic reductions and subgoal generation to step-by-step reasoning across languages.

B Case Study

  • Case 1 illustrates complex Lean4 reductions guided by natural language, including algebraic reductions based on conditions absent from the natural-language proof.Source: B Case Study · p. 12
  • Case 2 shows the framework producing Lean4 subgoals in the correct form, a behavior absent from correct proofs by the untrained model.Source: B Case Study · p. 12
  • The case studies show LLMs using natural-language proof guidance to perform step-by-step reasoning in both natural and formal language on relatively complex proofs.The authors present cases 3–5 as evidence of NL-FL bootstrapping's effectiveness.Source: B Case Study · p. 12

C Various dataset size training

These appendices discuss dataset-size behavior, Gemini-1.5 informalization, and the contents of an OBT record. The reported dataset-size gains do not follow the expected scaling law.

C Various dataset size training

D Different LLM’s behavior in Informalization

  • Gemini-1.5-generated proofs read more like mathematical proofs, while GPT-4-generated proofs read more like explanations of Lean4 code.The authors say this supports Gemini-1.5's stronger ability to understand Lean4 code for informalization.Source: D Different LLM’s behavior in… · p. 12

E OBT dataset record

2. Statement: Lean4 statement of the theorem

  • The record also stores the NL-FL bootstrapped Lean4 code, and the paper shows an example record in Table 14.Source: §2 · p. 13

F More bootstrapping method analysis

The paper compares in-code NL-FL bootstrapping with Head Bootstrapping, finding higher accuracy for its in-code approach in the reported experiment.

F More bootstrapping method analysis

G Applying TheoremLlama framework to other models

The paper reports that applying TheoremLlama to DeepSeek-Math improves Lean4 performance and presents an example of bootstrapping's effect. It also reports errors in a manual sample of OBT records and provides term and license information.

G Applying TheoremLlama framework to other models

  • Applying TheoremLlama to DeepSeek-Math substantially increased the model's Lean4 performance, supporting use beyond Llama.The authors use DeepSeek-Math-7B as the base model for this evaluation.Source: G Applying TheoremLlama framework to… · p. 13

H Analyze the impact of NL-FL Bootstrapping

  • In the example, the proof without bootstrapping does not use natural-language guidance and fails to solve the theorem.The authors contrast this with the bootstrapped proof example as evidence for the method's effectiveness.Source: H Analyze the impact of NL-FL… · p. 13

I OBT dataset quality analysis

  • Of 40 randomly sampled OBT records, 29 were correct, 4 partially correct, and 7 contained critical mistakes that made the proof mathematically incorrect.Reported errors included confusing general Lebesgue measure with probability measure and using normal rather than Cauchy sequence convergence in the informal reasoning.Source: I OBT dataset quality analysis · p. 13

J Term List

  • The term list explains paper terminology that the authors say may be unfamiliar to researchers in formal theorem proving.Source: J Term List · p. 14

K License

  • The dataset and code are assigned CC BY 2.0 and MIT licenses, respectively; the source Mathlib4 and Lean use Apache 2.0.Source: K License · p. 14
Loading 2407.03203v2…