PaperlayerView exact revision on arXiv

Source-linked AI summary

Lean-STaR: Learning to Interleave Thinking and Proving

Haohan Lin, Zhiqing Sun, Sean Welleck, Yiming Yang

arXiv:2407.10040v5cs.AI

TL;DR

Formal proof code omits the informal reasoning before each tactic, which proof-data training leaves unused. Lean-STaR trains models to generate stepwise thoughts and tactics, then applies expert iteration; with InternLM2-7b-plus it reaches 45.4% (pass@32) versus the previous 43.4% (pass@32) on miniF2F-test.

  • Problem

    Proof-data training typically uses formal code alone, leaving out informal reasoning before proof steps that may help models learn theorem proving.

    Source: §1 · pp. 1–2

  • Method

    Lean-STaR generates retrospective thoughts from ground-truth tactics, trains a model to produce a thought before each tactic, and further fine-tunes sampled proofs verified by Lean using expert iteration.

    Source: §1 · p. 2, §5 · p. 9

  • Results

    45.4% (pass@32) with InternLM2-7b-plus surpasses the previous 43.4% (pass@32) result on miniF2F-test.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Lean-STaR links informal and formal mathematics by generating natural-language thoughts for individual proof steps while improving formal proving capabilities.

    Source: §1 · p. 2

    Performance may be constrained by scalability: the fine-tuning dataset is small, GPT-4 data generation may be costly and introduce biases, and expert iteration can be bottlenecked by CPU and IO limits.

    Source: §5 · pp. 9–10

Abstract

from arXiv · show

Traditional language model-based theorem proving assumes that by training on a sufficient amount of formal proof data, a model will learn to prove theorems. Our key observation is that a wealth of informal information that is not present in formal proofs can be useful for learning to prove theorems. For instance, humans think through steps of a proof, but this thought process is not visible in the resulting code. We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof, thereby boosting the model's theorem-proving capabilities. Lean-STaR uses retrospective ground-truth tactics to generate synthetic thoughts for training the language model. At inference time, the trained model directly generates the thoughts prior to the prediction of the tactics in each proof step. Building on the self-taught reasoner framework, we then apply expert iteration to further fine-tune the model on the correct proofs it samples and verifies using the Lean solver. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment, significantly outperforming base models ($\boldsymbol{43.4\% \rightarrow 46.3\%,}$ Pass@64). We also analyze the impact of the augmented thoughts on various aspects of the theorem proving process, providing insights into their effectiveness.

1 INTRODUCTION

Lean-STaR uses informal thoughts before each formal proof tactic, addressing reasoning information absent from formal proof code. It combines retrospective thought generation, stepwise thought-and-tactic prediction, and expert iteration; its reported miniF2F-test results exceed prior results at the stated Pass@32 setting.

1 INTRODUCTION

  • Formal-proof training commonly uses Lean, Isabelle, or Coq code, but leaves out informal reasoning that may help models learn to prove theorems.The motivating example is the thought process before each proof step, which is not visible in formal source code.Source: §1 · pp. 1–2
  • Lean-STaR generates retrospective thoughts from human-written Lean proofs, trains a model to produce a thought before each tactic, then applies expert iteration using multi-step success as reward.The paper describes the training thoughts as synthetic and based on ground-truth tactics.Source: §1 · p. 2
  • Lean-STaR introduces natural-language thoughts for individual proof steps, complementing prior work translating standalone statements or informal proofs into formal proofs.The paper frames this as a new link between informal and formal mathematics.Source: §1 · p. 2
  • 45.4% (pass@32) with InternLM2-7b-plus surpasses the previous 43.4% (pass@32) result on miniF2F-test.With InternLM2-7b, Lean-STaR solves 34.8% (pass@32) or 36.1% (pass@64) of miniF2F-test problems.Source: §1 · p. 2
  • The implementation starts with roughly 50,000 thought-augmented Mathlib examples and synthesizes another 50,000 through two expert-iteration rounds.The authors describe this as the first thought-augmented theorem-proving dataset to their knowledge.Source: §1 · p. 2

2 RELATED WORK

Prior theorem-proving work has explored formal-proof training, search, data augmentation, and informal-to-formal translation. Lean-STaR places stepwise thoughts inside Lean tactic prediction, drawing on rationale-augmented reasoning and self-generated training data.

2 RELATED WORK

  • Learning-based theorem proving typically follows the GPT-f framework (Polu & Sutskever, 2020), training language models on (proof state, next-tactic) pairs and using them in best-first tree search; subsequent work explored data augmentation.Source: §2 · p. 2
  • Draft-Sketch-Prove uses informal drafts and formal proof sketches, but cited related systems depend on Isabelle tools such as Sledgehammer, whereas Lean lacks those tools.Lean-STaR instead generates a thought and predicts the next tactic at each proof step.Source: §2 · p. 3
  • Rationale-augmented methods can improve reasoning, but typically require extensive annotated examples or many similar pretraining examples, scarce resources for formal theorem proving.The paper proposes synthesizing examples using the formal system's correctness signal.Source: §2 · p. 3
  • Prior bootstrapping work uses expert iteration or self-generated correct reasoning-answer pairs; Lean-STaR builds on these ideas for thought-augmented proving.The cited work includes Polu et al. (2022), Zelikman et al. (2022), and Singh et al. (2023).Source: §2 · p. 3

3 OUR METHOD: LEAN-STAR

Lean-STaR extends formal tactic prediction with informal thoughts at each proof step, then bootstraps the model with expert iteration. The method moves from Lean proof states and tactics to thought-augmented training and sampling-based evaluation.

3.1 PRELIMINARIES

  • Lean represents theorem proving as successive goal states simplified by tactics; proving every resulting subgoal completes the proof.The interactive theorem prover supplies the new state after each tactic.Source: §3.1 · p. 3

3.2 DATA GENERATION & TRAINING

  • Training covers direct tactic prediction, thought-augmented tactic prediction, and a final model trained through expert iteration.The pipeline diagram shows GPT-4 producing a CoT dataset, followed by fine-tuning and iterative dataset updates.Source: §3.2 · p. 3, Figure 3 · p. 5

3.2.1 DIRECT TACTIC PREDICTION

  • The direct tactic-prediction baseline fine-tunes on successful-trajectory pairs of proof states and next tactics.The SFT model predicts a tactic from the current proof state.Source: §3.2.1 · p. 4

3.2.2 THOUGHT-AUGMENTED TACTIC PREDICTION

  • Thought-augmented prediction inserts a latent thought before each tactic, with the tactic conditioned on both thought and state.An oracle generates thoughts retrospectively from ground-truth tactics and proof states; the resulting examples fine-tune Lean-CoT from SFT. In the illustrated example, Lean's nlinarith completes the calculation despite an error in the thought.Source: §3.2.2 · pp. 4–5, Figure 2 · p. 4

3.2.3 BOOTSTRAPPING THOUGHT-AUGMENTED THEOREM PROVING

  • Expert iteration samples proof trajectories, filters for successful proofs, deduplicates them, and fine-tunes on the resulting data alongside the initial thought-augmented dataset.The updated model supplies trajectories for the next iteration.Source: §3.2.3 · p. 5

3.3 EVALUATION

  • For evaluation, best-first search expands prioritized states, while sampling generates parallel trajectories and ignores illegal tactics.The authors report that best-first search performed poorly with Lean-CoT and Lean-STaR, attributing this to average log probabilities being an unreliable quality indicator when thoughts are generated; sampling accommodates thoughts and uses approximately the same GPU time at equal S × K.Source: §3.3 · pp. 5–6

4 EXPERIMENTS

Across MiniF2F experiments, Lean-STaR improved theorem-proving pass rates over baselines, with gains from thought augmentation and further gains from expert iteration.

4.1 EXPERIMENTAL SETUP

  • The experiments use Mathlib-based LeanDojo training, GPT-4 retrospective thought generation, two expert-iteration rounds, and evaluation on miniF2F and LeanDojo.For thought annotation, 17,256 successful trajectories yielded 52,438 thoughts; steps whose tactic contained a newline were filtered out.Source: §4 · p. 7, §4.1 · p. 7

4.3 EXPERIMENTS WITH STRONGER BASE MODEL AND MORE DATA

  • 45.4% (Lean-STaR) versus 40.9% (InternLM-plus) was reported with a similar inference budget; InternLM-plus reached 43.4% using best-first search with more budget.The comparison is on miniF2F-test with Lean.Source: Table 2 · p. 8, §4.3 · p. 9

4.1 EXPERIMENTAL SETUP

  • The evaluation excludes methods for other formal languages and some methods with substantially different or computationally expensive inference budgets.The study uses sampling for Lean-STaR and compares against baselines under settings intended to resemble their inference budgets.Source: §4.1 · p. 8

4.2 MAIN RESULTS

  • 34.8% (Lean-STaR) versus 30.3% (InternLM2) and 30.7% (COPRA) was achieved at a similar inference budget; a larger budget raised Lean-STaR to 36.1%.The InternLM2 baseline used best-first search; COPRA used GPT-4.Source: §4.2 · p. 8
  • 32.8% (LEAN-COT) versus 29.5% (SFT) shows improved pass rate after training on thought-augmented examples.The SFT model was already specialized for generating Lean tactics.Source: §4.2 · p. 8
  • 32.8% to 34% to 34.8% pass rates followed two expert-iteration rounds, and doubling the sampling budget raised performance to 36.1%.Expert iteration trains on sampled thoughts and tactics that yield correct proofs.Source: §4.2 · p. 8

4.4 EXPERIMENTS ON EXPERT ITERATION WITHOUT COT

  • Expert iteration without CoT reached 43.0% versus 45.4% for Lean-STaR on InternLM-plus, and 30.7% versus 34.0% on InternLM-base.Table 3 compares Lean-CoT, Lean-STaR, and expert iteration without CoT.Source: Table 3 · p. 9, §4.4 · p. 9

4.3 EXPERIMENTS WITH STRONGER BASE MODEL AND MORE DATA

  • The stronger-base-model experiment used 140,000 GPT-4o-annotated thoughts for Lean-CoT, then about 60,000 sampled proof-state, thought, and next-tactic pairs for one expert-iteration round.The resulting STaR dataset was used to fine-tune Lean-CoT into Lean-STaR.Source: §4.3 · p. 9

5 CONCLUSION & LIMITATIONS

Lean-STaR combines retrospective thought generation with expert iteration and reports improved MiniF2F-test pass rates, while identifying computational scalability as its primary limitation.

5 CONCLUSION & LIMITATIONS

  • The paper reports increasing the miniF2F-test pass rate from 30.3% to 36.1% with Lean-STaR.The method generates synthetic rationales retrospectively using ground-truth tactics, then fine-tunes on correct proofs sampled and verified with Lean.Source: §5 · p. 9
  • Computational scalability is the primary limitation, with performance potentially constrained by the relatively small fine-tuning dataset and costs of GPT-4 synthetic-data generation.The authors also note possible bias in generated data and CPU/IO bottlenecks that may slow expert iteration.Source: §5 · pp. 9–10

A ADDITIONAL EXPERIMENT SETUP

The appendix describes how successful sampled proof trajectories are collected and used for two expert-iteration rounds.

A.1 LEAN-STAR EXPERT ITERATION

  • Each iteration samples LeanDojo problems, retains examples from successful proofs, and fine-tunes on the combination of initial GPT-4-annotated reasoning data and collected examples.The first iteration produced 32,231 distinct proof-state, thought, and next-tactic pairs; fine-tuning ran for one epoch.Source: §A.1 · p. 14
  • Sampling used K = 32 parallel attempts at temperature T = 1.0, at most five tactic generations per problem, and a one-minute limit per problem.Each problem required about 0.5 A100 minutes on average; up to three successful trajectories were collected per problem.Source: §A.1 · p. 14
  • The second iteration generated roughly 19,000 pairs, and the InternLM2-plus experiment used a slightly different setup detailed elsewhere.The second-round model was fine-tuned on the new dataset; the setup difference is described in Section 4.3 and Appendix F.Source: §A.1 · p. 14

B STATISTICS FOR OUR METHODS AS WELL AS THE BASELINES

Table 4 reports MiniF2F statistics for baselines, Lean-CoT, and Lean-STaR under a shared sampling configuration.

B STATISTICS FOR OUR METHODS AS WELL AS THE BASELINES

  • Table 4 covers baselines, Lean-CoT, and Lean-STaR on MiniF2F using sampling with N = 50, K = 32, and T = 0.7.Source: Table 4 · p. 14

C DATA LEAKAGE

The paper discusses data-leakage risk and argues it is unlikely, citing the evaluation setup and differences from manually written proofs. It also explains a Lean induction proof and reports performance patterns by problem type and difficulty.

C DATA LEAKAGE

  • The authors consider leakage possible because GPT-4 or InternLM may have encountered miniF2F during pretraining, but argue it is unlikely given the evaluation setup and generated-proof differences.They note that InternLM was evaluated on miniF2F in a widely used setup and that almost all generated proofs differ from manual ones.Source: C DATA LEAKAGE · p. 15, Table 5 · p. 15

D AN EXAMPLE AND EXPLANATION OF A FORMAL PROOF IN LEAN

D.1 PERFORMANCE ANALYSIS BY TYPES AND DIFFICULTIES USING INTERNLM2-PLUS-7B

The analysis partitions InternLM2-plus-7b miniF2F-test results by problem type and difficulty, distinguishing Lean-CoT and Lean-STaR performance patterns.

D.1 PERFORMANCE ANALYSIS BY TYPES AND DIFFICULTIES USING INTERNLM2-PLUS-7B

  • Lean-STaR improves performance on difficult problems across all categories, unlike the reported InternLM2-base pattern.Source: §D.1 · p. 17
  • Lean-CoT’s improvements are concentrated mainly in Number Theory.Source: §D.1 · p. 17
  • The reported counts are split by problem type and difficulty for InternLM2-plus-7b.Source: §D.1 · p. 17

E COMPARISON BETWEEN SEARCH METHOD AND SAMPLING METHOD

The section compares search and sampling setups and reports that the better training approach varies between InternLM2-base and InternLM2-plus.

E COMPARISON BETWEEN SEARCH METHOD AND SAMPLING METHOD

  • The comparison evaluates sampling with N = 50, S = 1, K = 32 against best-first search with N = 50, S = 32, K = 1.Sampling uses temperature 0.7; BFS denotes Best-First Search.Source: Table 8 · p. 18

F PERFORMANCE DIFFERENCE OF JOINT TRAINING AND CONTINUE TRAINING

F.1 SEARCH AND SAMPLING BUDGET

The section reports that Lean-STaR benefits from larger sampling budgets, then gives GPT-4 instructions for retrospective rationale generation and examples of thought-augmented Lean proofs.

F.1 SEARCH AND SAMPLING BUDGET

  • Lean-STaR benefits more as sampling budget K increases, while additional sampling without thoughts may saturate; the authors attribute the difference to output diversity and exploration.The analysis fixes N = 50 and examines pass rate against search size or sampling budget S × K.Source: §F.1 · p. 18, Table 10 · p. 19

G RETROSPECTIVE RATIONALE GENERATION PROMPT OF GPT-4

  • The retrospective-rationale prompt asks for goal-based, logically ordered reasoning that avoids mentioning the target tactic until the conclusion.It also instructs the model not to construct the reasoning retrospectively from the given tactic.Source: G RETROSPECTIVE RATIONALE GENERATION… · pp. 19–20

H EXAMPLES OF GENERATED LEAN PROOFS WITH THOUGHTS

Loading 2407.10040v5…