Research map / Large language models / Agents, code and math
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
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 MPS-Prover, a stepwise Lean prover on Qwen2.5-Math-7B that prunes ~40% of training data and uses multi-perspective tree search (one critic pick plus three heuristic picks per expansion) to reach state-of-the-art 7B results on miniF2F and ProofNet.
Problem
Stepwise LLM-based theorem provers in Lean suffer from biased critic guidance, unprovable states, and ineffective tactic use, leading to inefficient search and long proofs.
Approach
Combine a learned distance critic with three heuristic selection rules (tactic effectiveness scoring, minimizing case splits, shortest state preference) in best-first tree search, and curate training data by removing short proofs (≤3 steps) and ineffective tactics.
Key results
- MPS-Prover solves 185/244 miniF2F problems (75.82%) under accumulative search, the best step-level result, above BFS-Prover's 72.54%.
- MPS-Prover reaches 32.97% on ProofNet-test, the best among reported 7B models, above DeepSeek-Prover-V2 (CoT) at 29.6%.
- Mean proof length is 3.44 Lean steps versus 15.91 for Kimina-Prover and 52.16 for DeepSeek-Prover-V2 on 170 common miniF2F problems.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use MPS multi-perspective search instead of BFS under approximately equivalent computational budgets | stepwise theorem proving · miniF2F | success rate: 66.39% to 67.62% | Helped |
| use MPS-Prover instead of the strongest reported 7B baseline | 7B theorem provers · ProofNet-test | performance: 29.6% to 32.97% | Helped |
| use MPS-Prover instead of Kimina-Prover | proof generation · 170 common miniF2F problems | mean proof length (Lean steps): 15.91 to 3.44 | Helped |
| use MPS-Prover instead of DeepSeek-Prover-V2 | proof generation · 170 common miniF2F problems | mean proof length (Lean steps): 52.16 to 3.44 | Helped |
| remove post-training data curation (ablation) | MPS-Prover · miniF2F | problems solved: one fewer problem | Hurt |
| replace critic score-based node selection with random node selection (ablation) | MPS-Prover · miniF2F | problems solved: 177 to 164 problems solved | Hurt |
| replace the tactic effectiveness heuristic with random selection (ablation) | MPS-Prover · miniF2F | performance | Hurt |
| replace the minimizing case splits heuristic with random selection (ablation) | MPS-Prover · miniF2F | performance | Hurt |
| replace the shortest state preference heuristic with random selection (ablation) | MPS-Prover · miniF2F | performance | Hurt |
Surprising findings
- Removing the data curation strategy costs only one miniF2F problem while using 40% more training data.
- The 7B DeepSeek-Prover-V2 distilled CoT model (82.0% miniF2F) still outperforms MPS-Prover on miniF2F, which the authors attribute to distillation from a larger model.
Limitations
- Stepwise search cannot introduce and prove auxiliary lemmas (e.g., via have with sub-proofs) in the way whole-proof methods can.
- Heuristic tactic scores are manually assigned from expert experience and not tuned automatically.
- Results on miniF2F trail the distilled 7B DeepSeek-Prover-V2 CoT model.
Experimental setup
Datasets: Lean Workbook Numina AoPS-Instruct miniF2F ProofNet
Benchmarks: miniF2F ProofNet
Metrics: pass rate / accuracy average proof length proof tactic diversity
Baselines: Kimina-Prover-Preview DeepSeek-Prover-V2 Goedel-Prover-SFT STP Leanabell-Prover-GD-RL Kimina-Prover-Preview-Distill InternLM2.5-StepProver HunyuanProver BFS-Prover Deepseek-Prover-V1.5-RL
Builds on: BFS-Prover expert iteration InternLM2.5-StepProver
Closest papers by meaning
- Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers (ICML 2026 · similarity 0.91)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.90)
- 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes (NeurIPS 2025 · similarity 0.89)
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.89)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.89)
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · 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.