DeepSeek-Prover-V2 定理证明模型

是什么

DeepSeek-Prover-V2 是 DeepSeek 发布的用于 Lean 4 形式化定理证明（formal theorem proving）的开源模型 ^[1]。Lean 4 既是一门编程语言，也是证明助手（proof assistant）：命题和它的证明都要写成机器能逐行检查的形式。这与用自然语言讲解数学的系统不同，模型的输出是一段证明脚本，Lean 的检查器要么接受、要么拒绝，听起来合理的论证不算数。介绍该模型的论文于 2025 年 4 月 30 日发布到 arXiv，维基百科则把发布时间记为 2025 年 5 月 1 日 ^[1][3]。DeepSeek 发布了 7B 和 671B 两种参数规模的版本，仓库说明模型的使用受 DeepSeek 的 Model License 约束 ^[2]。

训练方式

冷启动训练数据不是人工写的，而来自一条由 DeepSeek-V3 驱动的递归证明流水线：它把问题拆成子目标（subgoal），逐个处理，再把结果整理成训练材料 ^[1]。已经解出的子目标证明，会与 DeepSeek-V3 的逐步推理合并，构成思维链（chain-of-thought）数据，从而把非形式推理与形式证明放进同一个模型 ^[1]。也就是说，模型同时练两件事：用普通的数学语言讲清楚思路，以及把每一步写成 Lean 能通过的形式。论文标题把这一方法概括为用于子目标分解的强化学习 ^[1]。

成绩

在 MiniF2F-test 这一常用基准上，模型的通过率为 88.9% ^[1]。在共含 658 道题的 PutnamBench 上，它解出 49 道 ^[1]。两个数字描述的是不同类型的难度：一个是在精心整理的基准上的高通过率，另一个是在规模更大、题目更难的集合上解出的绝对数量。

ProverBench

论文提出了自己的基准 ProverBench，共 325 道形式化题目，其中 15 道取自 AIME 2024–2025 的竞赛题 ^[1]。这 15 道题提供了一次形式与非形式方法的直接对照：DeepSeek-Prover-V2 解出 6 道，而 DeepSeek-V3 用自然语言作答、在多次尝试中取多数投票，解出 8 道 ^[1]。作者把这一结果解读为形式化数学与非形式数学之间的差距在缩小：形式化训练的模型仍然落后，但两者已经接近到可以拿同一批题目互相比较的程度 ^[1]。

发布信息

7B 版本支持最长 32K tokens 的扩展上下文；仓库没有给出 671B 版本的上下文长度 ^[2]。两个规模都以开放权重形式发布，使用遵循 DeepSeek 的 Model License ^[2]。

在数学模型序列中的位置

DeepSeek-Prover-V2 属于 DeepSeek 的数学模型序列，这条线上排在它之后的是 DeepSeekMath-V2（2025 年 11 月 27 日）^[3]。形式化这条分支之所以值得关注，是因为它的成果可以被检查：证明要么通过编译、要么不通过，所以 MiniF2F-test、PutnamBench 这类基准上的进展是验证出来的，而不是评判出来的。论文在 AIME 题目上的对照，指向的正是这个模型想要探查的更大问题：日常的数学推理，有多少可以转写成机器能够确认的形式。