Research map / Large language models / Agents, code and math
Lean-STaR: Learning to Interleave Thinking and Proving
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Lean-STaR trains LLMs to generate informal thoughts before each Lean tactic, using GPT-4 retrospective rationales and expert iteration verified by the Lean solver, reaching 36.1% pass@64 on miniF2F-test.
Problem
Language-model-based formal theorem proving in Lean relies only on formal (proof state, tactic) data, ignoring the informal thought process that precedes each proof step.
Approach
Generate synthetic natural-language thoughts retrospectively with GPT-4 conditioned on ground-truth tactics, fine-tune a tactic predictor to produce a thought before each tactic, then bootstrap with expert iteration filtered by Lean verification, and use a sampling-based proof search suited to thought-augmented outputs.
Key results
- Lean-STaR (Iter-2) on InternLM2-7b reaches 34.8% pass@32 and 36.1% pass@64 on miniF2F-test, versus 28.7% for few-shot InternLM2-7b and 29.5% for SFT.
- Lean-STaR built on InternLM2-plus-7b reaches 45.4% pass@32 and 46.3% pass@64 on miniF2F-test, versus 40.9% for the base model with sampling and 43.4% for the reported best-first search result.
- Expert iteration without thoughts reaches 30.7% on InternLM2-base and 43.0% on InternLM2-plus, below Lean-STaR, suggesting gains are not solely from expert iteration.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add retrospectively generated thoughts to tactic training | InternLM2-7b SFT · miniF2F-test | Pass@32: 29.5% -> 32.8% | Helped |
| Add retrospectively generated thoughts to tactic training | InternLM2-plus-7b SFT · miniF2F-test | Pass@32: 41.3% -> 43.4% | Helped |
| Add one round of expert iteration to Lean-CoT | InternLM2-7b Lean-CoT · miniF2F-test | Pass@32: 32.8% -> 34.0% | Helped |
| Add a second round of expert iteration | InternLM2-7b Lean-STaR (Iter-1) · miniF2F-test | Pass@32: 34.0% -> 34.8% | Helped |
| Increase sampling budget from K=32 to K=64 | InternLM2-7b Lean-STaR (Iter-2) · miniF2F-test | pass rate: 34.8% -> 36.1% | Helped |
| Apply expert iteration without CoT, using (state, tactic) pairs only (ablation) | InternLM2-plus-7b SFT · miniF2F-test | Pass@32: 41.3% -> 43.0% | Helped |
| Replace CoT expert iteration with expert iteration without CoT (ablation) | InternLM2-plus-7b · miniF2F-test | Pass@32: 43.0% -> 45.4% | Hurt |
| Use joint training instead of continuing training from Lean-CoT (ablation) | InternLM2-plus-7b Lean-STaR · miniF2F-test | Pass@32: 45.5% -> 43.9% | Hurt |
| Use joint training instead of continuing training from Lean-CoT (ablation) | InternLM2-base-7b Lean-STaR · miniF2F-test | Pass@32: 33.2% -> 34.0% | Helped |
| Use sampling rather than best-first search for thought-augmented proving (ablation) | Lean-CoT · miniF2F-test | pass rate: 27.0% / 25.4% -> 32.8% | Mixed |
Surprising findings
- Best-first search with average log-probability scoring performed poorly for thought-augmented models (e.g., Lean-CoT 25.4% with beam search vs 32.8% with sampling), so the authors switched to sampling for evaluation.
- Lean-STaR gains grow with sampling budget, whereas sampling without thoughts saturates (SFT-Direct 30.7% at S x K=32 and 30.7% at 64).
Limitations
- Training data is relatively small, which may constrain scalability.
- Reliance on GPT-4 for synthetic thought annotation is costly and may introduce biases.
- Expert iteration is bottlenecked by CPU and IO limits of the Lean ITP.
Experimental setup
Datasets: LeanDojo Benchmark 4 v9 Mathlib via LeanDojo
Benchmarks: miniF2F-test LeanDojo random subset (320 problems)
Metrics: pass@32 pass@64
Baselines: GPT-3.5 few-shot GPT-4 few-shot Llemma-7b ReProver COPRA InternLM2-7b SFT (InternLM2-7b) InternLM2-plus-7b
Builds on: Self-Taught Reasoner (STaR) expert iteration GPT-f ReST-EM LeanDojo
Closest papers by meaning
- MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving (ICML 2025 · similarity 0.91)
- LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.90)
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.90)
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.89)
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problems (NeurIPS 2024 · similarity 0.89)
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.