Research map / Large language models / Agents, code and math
STP: Self-play LLM Theorem Provers with Iterative Conjecturing 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.
Proposes STP, a self-play framework where an LLM alternates as conjecturer and prover, training the conjecturer on barely-provable conjectures to keep generating harder, useful training signal for whole-proof theorem proving in Lean and Isabelle.
Problem
Formal theorem proving with LLMs is limited by scarce training data and sparse rewards: expert iteration and RL plateau because few generated proofs are correct on unproved statements.
Approach
A single LLM plays both conjecturer and prover; the conjecturer is rewarded for producing conjectures with low but positive prover pass rates, filtered by an elegancy criterion and re-weighted via a Wasserstein projection toward unproved statements, so the curriculum self-adapts without new data.
Key results
- On LeanWorkbook, STP proves 28.5% of statements with 51.3B generated tokens, versus 13.2% for expert iteration.
- STP reaches 65.0% pass@3200 on miniF2F-test and 23.9% pass@3200 on ProofNet-test, state of the art among whole-proof methods reported.
- STP solves 8/644 PutnamBench problems at pass@3200, versus 6 for the prior best.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use STP instead of expert iteration | DeepSeek-Prover-V1.5-SFT · LeanWorkbook | cumulative pass rate: 13.2% -> 28.5% | Helped |
| use STP instead of DeepSeek-Prover-V1.5-RL | miniF2F-test · miniF2F-test, pass@3200 | pass rate: 54.9% ± 0.7% -> 65.0% ± 0.5% | Helped |
| use STP instead of DeepSeek-Prover-V1.5-RL | ProofNet-test · ProofNet-test, pass@3200 | pass rate: 22.0% ± 0.5% -> 23.9% ± 0.6% | Helped |
| add proofs of generated conjectures to final retraining (ablation) | STP · miniF2F-test, pass@128 | pass rate: 58.3% ± 0.7% -> 61.2% ± 0.6% | Helped |
| add proofs of generated conjectures to final retraining (ablation) | STP · ProofNet-test, pass@128 | pass rate: 17.4% ± 0.4% -> 19.5% ± 0.7% | Helped |
Surprising findings
- Expert iteration on Isabelle checkpoints produced only 131 correct proofs out of 2.5M attempts on unproved statements, so finetuning had almost no effect.
- Manual check of 20 unproved LeanWorkbook statements suggests only 7 are provable, so the best achievable pass rate is estimated at 38.7% to 68.5%.
Limitations
- Formal LeanWorkbook statements are not always provable (some are mistranslations or false), which bounds achievable pass rates.
- Isabelle experiments disable advanced tactics such as sledgehammer, smt and sos, reducing verification strength.
- Compute-heavy: 32 TPU-v4 nodes, with 75% of wall-clock time spent generating proofs.
Experimental setup
Datasets: LeanWorkbook Mathlib4 miniF2F-valid ProofNet-valid AFP miniF2F-test ProofNet-test PutnamBench
Benchmarks: miniF2F-test ProofNet-test PutnamBench LeanWorkbook
Metrics: pass@k cumulative pass rate
Baselines: DeepSeek-Prover-V1.5-SFT DeepSeek-Prover-V1.5-RL expert iteration parallel sampling ReProver PACT GPT-f HTPS Lean-STaR InternLM2.5-StepProver DSP TheoremLlama
Builds on: expert iteration DeepSeek-Prover-V1.5 Llemma PISA vLLM
Closest papers by meaning
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.89)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.88)
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.88)
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.88)
- Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers (ICML 2026 · similarity 0.88)
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.88)
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.