We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model. The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions (years 24-25). Further evaluation on these 15 AIME problems shows that the model successfully solves 6 of them. In comparison, DeepSeek-V3 solves 8 of these problems using majority voting, highlighting that the gap between formal and informal mathematical reasoning in large language models is substantially narrowing.
核心贡献 · Key contributions
提出利用 DeepSeek-V3 进行子目标分解和形式化的递归定理证明流程。 Proposes a recursive theorem proving pipeline using DeepSeek-V3 for subgoal decomposition and formalization.
通过将形式化证明与 DeepSeek-V3 的思维链推理配对，引入冷启动数据合成。 Introduces cold-start data synthesis by pairing formal proofs with chain-of-thought reasoning from DeepSeek-V3.
开发了使用分解子目标生成渐进困难训练任务的课程学习框架。 Develops a curriculum learning framework using decomposed subgoals to generate progressively harder training tasks.
在 MiniF2F-test 上达到最先进性能（88.9%通过率），并解决 49 个 PutnamBench 问题。 Achieves state-of-the-art performance on MiniF2F-test (88.9% pass ratio) and solves 49 PutnamBench problems.
引入 ProverBench 基准，包含 325 个形式化问题，其中 15 个来自 AIME 24-25。 Introduces ProverBench, a benchmark of 325 formalized problems including 15 from AIME 24-25.
证明从冷启动数据开始的强化学习显著提升了形式化定理证明能力。 Demonstrates that reinforcement learning from cold-start data significantly improves formal theorem proving.
局限 · Limitations
评估仅限于 Lean 4；未验证对其他证明助手的泛化能力。 Evaluation limited to Lean 4; generalization to other proof assistants not verified.
冷启动数据依赖 DeepSeek-V3，可能引入其训练中的偏差。 Cold-start data relies on DeepSeek-V3, which may introduce biases from its training.
由于形式化挑战，在几何和组合问题上的性能有限。 Performance on geometry and combinatorics problems is limited due to formalization challenges.
强化学习使用二元奖励，可能无法捕捉部分进展。 Reinforcement learning uses binary rewards, which may not capture partial progress.
模型规模（671B）带来高计算成本；较小的 7B 变体性能较低。 Model size (671B) incurs high computational cost; smaller 7B variant shows lower performance.
论文章节 · Sections（共 12）
摘要Abstract
1 引言1 Introduction
2 方法2 Method
2.1 通过子目标分解的递归证明搜索2.1 Recursive Proof Search via Subgoal Decomposition
2.2 统一非形式推理与证明形式化2.2 Unifying Informal Reasoning and Proof Formalization
2.3 DeepSeek-Prover-V2 的训练细节2.3 Training Details of DeepSeek-Prover-V2
3 实验结果3 Experimental Results
3.1 MiniF2F 基准测试结果3.1 Results on MiniF2F Benchmark
3.2 本科级基准测试结果3.2 Results on Undergraduate-level Benchmarks
3.3 组合问题结果3.3 Results on Combinatorial Problems
3.4 ProverBench：AIME 与教科书问题的形式化3.4 ProverBench: Formalization of AIME and Textbook Problems