Microsoft Research
Introduction | Core Method | Evaluation Results | Setup Environment | Quick Start | Verify Solutions | Contributing | Citation | Contact | Acknowledgements
## Introduction Recent advancements, such as **DeepSeek-Prover-V2-671B** and **Kimina-Prover-Preview-72B**, demonstrate a prevailing trend in leveraging reinforcement learning (RL)-based large-scale training for automated theorem proving. Surprisingly, we discover that even without any training, careful neuro-symbolic coordination of existing off-the-shelf reasoning models and tactic step provers can achieve comparable performance. We introduces **DSP+**, an improved version of the Draft, Sketch, and Prove framework, featuring a *fine-grained and integrated* neuro-symbolic enhancement for each phase: 1. **In the Draft phase**, we prompt reasoning models to generate concise natural-language subgoals, removing thinking tokens and references to human-written proofs; 2. **In the Sketch phase**, subgoals are autoformalized, and sketch lines containing syntactic errors are masked according to predefined rules; 3. **In the Proving phase**, we integrate symbolic search methods like Aesop with step provers to establish proofs for the sketch subgoals. Experimental results show that, without any additional model training or fine-tuning, DSP+ solves 80.7%, 32.8%, and 24 out of 644 problems from miniF2F, ProofNet, and PutnamBench, respectively, while requiring fewer budgets compared to state-of-the-arts. DSP+ proves **imo_2019_p1**, an IMO problem in miniF2F that is not solved by any prior work. Additionally, DSP+ generates proof patterns comprehensible by human experts, facilitating the identification of formalization errors; For example, eight wrongly formalized statements in miniF2F are discovered. Our results highlight the potential of classical reasoning patterns besides the RL-based training.
| Type | Solution (Model Size) | Sample Budget | miniF2F-test | ProofNet | PutnamBench | miniF2F/IMO |
|---|---|---|---|---|---|---|
| Whole-proof Generation | Goedel-Prover-7B | 32 | 57.6% | 15.2% | 6/644 | -- |
| 512 | 62.7% | -- | 7/644 | -- | ||
| 25600 | 64.7% | -- | -- | -- | ||
| STP-7B | 3200 | 65.0% | 23.9% | 8/644 | -- | |
| 25600 | 67.6% | 26.9% | -- | -- | ||
| Kimina-Prover-Preview-7B | 1 | 52.5% | -- | -- | -- | |
| 32 | 63.1% | -- | -- | -- | ||
| 192 | -- | -- | 10/644 | -- | ||
| 1024 | 70.8% | -- | -- | -- | ||
| Kimina-Prover-Preview-72B | 1 | 52.9% | -- | -- | -- | |
| 8 | 65.2% | -- | -- | -- | ||
| 32 | 68.9% | -- | -- | -- | ||
| 1024 | 77.9% | -- | -- | -- | ||
| 8192 | 80.7% | -- | -- | 40% | ||
| DeepSeek-Prover-V2-7B | 1 | 58.6% | -- | -- | -- | |
| 32 | 75.6% | 23.0% | 11/658 | -- | ||
| 128 | -- | 25.4% | 15/658 | -- | ||
| 1024 | 79.9% | 29.6% | 23/658 | -- | ||
| 8192 | 82.0% | -- | -- | -- | ||
| DeepSeek-Prover-V2-671B | 1 | 61.9% | -- | -- | -- | |
| 32 | 82.4% | 30.5% | 22/658 | -- | ||
| 128 | -- | 33.6% | 33/658 | -- | ||
| 1024 | 86.6% | 37.1% | 49/658 | -- | ||
| 8192 | 88.9% | -- | -- | 50% | ||
| Tree Search | InternLM2.5-StepProver-7B | 2×32×600 | 50.7% | -- | 6/640 | -- |
| 256×32×600 | 65.9% | 27.0% | -- | -- | ||
| DeepSeek-Prover-V1.5-RL-7B + RMaxTS | 4×6400 | 59.6% | 25.3% | -- | -- | |
| 32×6400 | 63.5% | -- | -- | -- | ||
| HunyuanProver-7B | 600×8×400 | 68.4% | -- | -- | 20% | |
| BFS-Prover-7B | 2048×2×600 | 70.8% | -- | -- | 25% | |
| accumulative | 73.0% | -- | -- | -- | ||
| Hybrid | DSP (GPT-4o, Isabelle) | 10 | -- | -- | 4/640 | -- |
| DSP (Minerva-540B, Isabelle) | 100 | 38.9% | -- | -- | 5% | |
| DSP+ (QwQ-32B, V3-671B, BFS-Prover-7B) | 1 | 52.5% | -- | -- | -- | |
| 8 | 68.4% | -- | -- | -- | ||
| 32 | 71.3% | 24.7% | 15/644 | -- | ||
| 128 | 74.2% | 32.8% | 24/644 | -- | ||
| 1024 | 79.5% | -- | -- | 40% | ||
| DSP+ (QwQ-32B, QwQ-32B, BFS-Prover-7B) | 1024 | 79.1% | -- | -- | -- | |
| DSP+ (R1-671B, V3-671B, BFS-Prover-7B) | 1024 | 80.7% | -- | -- | -- | |
| DSP+ (ensemble) | accumulative | 83.6% | 33.9% | 25/644 | 45% |