Research map / Large language models / Agents, code and math
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
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.
Revives the Draft-Sketch-Prove framework as DSP+, coordinating off-the-shelf reasoning models, LLM sketch generation with error-line masking, and step-prover-integrated Aesop search, achieving strong miniF2F/ProofNet/PutnamBench results without any training.
Problem
Automated theorem proving in Lean currently relies on large-scale RL training; the prior inference-only DSP framework has been significantly outperformed. The question is whether careful neuro-symbolic coordination of existing models can match these results without training.
Approach
Fine-grained, integrated neuro-symbolic enhancements to each DSP phase: reasoning models produce concise thinking-stripped drafts; sketches include explicit hypothesis hints and error-line masking; and a step prover (BFS-Prover) is built into Aesop tree search for proving subgoals, with ensembles across model combinations.
Key results
- DSP+ solves 79.5% of miniF2F-test at 1024 workflow attempts (80.7% with DeepSeek-R1 as draft model), and 83.6% with the ensemble setting.
- DSP+ solves 32.8% of ProofNet-test and 24/644 PutnamBench problems at 128 attempts; the ensemble reaches 33.9% and 25/644.
- DSP+ proves imo_2019_p1, an IMO miniF2F problem not solved by prior work, and identifies eight wrongly formalized miniF2F-test statements.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Ensemble multiple model configurations instead of using the default configuration alone | DSP+ · miniF2F-test | accuracy: 79.5% -> 83.6% | Helped |
| Use DeepSeek-R1-671B as the draft model instead of QwQ-32B (ablation) | DSP+ · miniF2F-test | accuracy: 79.5% -> 80.7% | Helped |
| Use QwQ-32B as the sketch model instead of DeepSeek-V3-0324 (ablation) | DSP+ · miniF2F-test | accuracy: 79.5% -> 79.1% | Hurt |
| Remove the proving phase and step prover (ablation) | DSP+ · miniF2F-test | accuracy | Hurt |
| Remove the draft phase (ablation) | DSP+ · miniF2F-test | accuracy | Hurt |
| Remove prompting for concise drafts (ablation) | DSP+ draft phase · miniF2F-test | accuracy | Helped |
| Remove explicit specification of subgoal hypotheses (ablation) | DSP+ sketch phase · miniF2F-test | accuracy | Hurt |
| Remove error line masking (ablation) | DSP+ sketch phase · miniF2F-test | accuracy | Hurt |
| Add explicit specification of subgoal hypotheses (ablation) | DSP+ sketch phase · miniF2F-test | accuracy | Helped |
| Add error line masking for syntactically incorrect sketch lines (ablation) | DSP+ sketch phase · miniF2F-test | accuracy | Helped |
| Add human-written informal proofs to the draft and sketch phases (ablation) | DSP+ · miniF2F | accuracy | No clear effect |
| Use reasoning models rather than non-reasoning models for drafting (ablation) | DSP+ draft phase · miniF2F-test | accuracy | Helped |
Surprising findings
- Removing human-written informal proofs from the draft phase does not hurt and even improves accuracy for reasoning models, unlike the original DSP.
- Using DeepSeek-R1 as the draft model yields higher accuracy than QwQ-32B, while QwQ-32B has stronger instruction following and better sample efficiency.
Limitations
- Design space is underexplored; default configuration not optimal and duplicated searches remain.
- Failure cases in draft phase (hard IMO proofs), sketch formalization difficulty, and proving misalignment with Lean semantics.
- Results sensitive to Lean version (e.g., v4.9.0-rc1 vs v4.17.0-rc1).
Experimental setup
Datasets: miniF2F ProofNet PutnamBench ProverBench
Benchmarks: miniF2F-test ProofNet-test PutnamBench miniF2F/IMO ProverBench
Metrics: pass@k accuracy solved problem count inference tokens per pass
Baselines: DeepSeek-Prover-V2-671B Kimina-Prover-Preview-72B Goedel-Prover-7B STP-7B BFS-Prover-7B InternLM2.5-StepProver-7B DSP (Minerva-540B, Isabelle) HunyuanProver-7B
Builds on: Draft, Sketch, and Prove Aesop BFS-Prover Lean Copilot DeepSeek-Prover-V1.5
Closest papers by meaning
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.91)
- Subgoal-based Demonstration Learning for Formal Theorem Proving (ICML 2024 · similarity 0.90)
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.89)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.89)
- Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers (ICML 2026 · similarity 0.89)
- Lean-STaR: Learning to Interleave Thinking and Proving (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.