Lean-STaR
Bootstraps interleaved informal thoughts and formal Lean tactics via expert iteration and best-first proof search verified by the Lean kernel.
The loop
- Proposes
A language model generates a rationale thought followed by a formal Lean tactic at each node of the proof tree.
- Judged by
The Lean proof assistant checks whether the tactic advances or closes the goal.
- Steers
Best-first tree search explores multiple thought-tactic branches, and verified trajectories are used to fine-tune the model in STaR expert-iteration rounds.
Headline result
Improved miniF2F-test pass@64 in Lean from 30.8% to 46.3%, outperforming tactic-only search baselines.
What this does not prove
Generating natural-language thoughts before every tactic increases token count per node during tree search.
How it generalizes the harness
- The algorithm is the solver
- Inverted control
- A domain authority judges
- Feedback retrains the generator
- Search over a population
- An infallible formal kernel
- Intra-algorithmic surgery (inside the while-loop)
Best-first proof search and Lean kernel verification filter thought-augmented tactic trajectories to retrain the generator.
Classification
| What it proposes | Proof tactic |
|---|---|
| Generative model | InternLM2-Math-Base 7B with thought-tactic policy |
| Algorithmic authority | Lean theorem prover and best-first search tree |
| Feedback | Proof state |
| What gets updated | Search tree and model weights |
| When it runs | During training |
| Validity | Formal (machine-checked) |
| Evidence | Code released |
| Lineage | Original system |