DeepSeek-Prover-V2:把「模型说它对」换成「Lean 说它对」
deepseek-prover-v2
DeepSeek 的形式化定理证明模型:671B MoE 底座(与 DeepSeek-V3 同源)、目标语言 Lean 4,是在旗舰级底座上做形式化对齐。核心创新是冷启动的递归子目标分解:竞赛级命题一步证成功率极低、RL 几无正样本,于是先让 DeepSeek-V3 把命题拆成子目标串,再由 7B 小模型逐个证,合成的完整证明成了训练数据,即用可分解性换数据密度;RL 奖励二元,信号来自 Lean 内核。读数(厂商自报):MiniF2F-test 88.9%(pass@8192)、PutnamBench 49/658(约 7.4%)、自建 ProverBench 325 题。三个数一起读:MiniF2F 在该采样预算下已近饱和,换普特南立刻掉一个数量级;ProverBench 自家题自家跑要打折。公开仓库(约 1304 stars)含证法 ZIP,可直接在 Lean 里跑,可核验性比闭源高一档。边界:pass@8192 意味着八千多个候选再筛,与 pass@1 不可比。与 Kimina-Prover 的 92.2% 协议不可通约,本站并列收录不排名。置信度 C(厂商宣称):未在自有 Lean 4 + mathlib 环境复算。
- 置信度
- 厂商宣称
- 只有官方模型卡/发布会,无独立复测
- 关键指标
- MiniF2F-test
- 厂商宣称 · 2025-07
- 成熟度
- 研究
- 研究 → 演示 → 产品 → 生产
我们的判断我们给它 C 档(厂商宣称)。这个判断看起来和「数学可机械核验」矛盾,其实不矛盾:可核验的是证明文本,不是那个 88.9%。仓库公开、证法可下载,意味着任何人有足够算力都能复核;但本站没有做这件事,所以我们不把自己没跑过的数字升成 A。C 档在这里是诚实,不是贬低。
它真正的贡献是那条递归子目标分解的冷启动路线。形式化证明的 RL 长期卡在「正样本太稀疏」:难题一步证不出来,就没有奖励可学。让强模型拆题、让 7B 小模型证子目标、再合回完整证明,是把数据密度问题转化成可分解性问题,这个思路对整个自动证明领域都比它自己的分数更有价值。二元奖励直接来自 Lean 内核也很关键——它让 reward hacking 在这条路线上结构性地难以发生。
水位要读落差而不是读单点:MiniF2F 88.9% 与 PutnamBench 49/658(约 7.4%)之间的差距,才是这个域的真实位置——竞赛级形式化数学接近饱和,真正的难题还在个位数百分比。另外 pass@8192 的采样预算意味着生产成本是八千次生成量级,拿它和 pass@1 比是不成立的;autoformalization(自然语言到 Lean 命题)那一步的错误率也不在 88.9% 里,而它在真实使用中往往是失败的主要来源。
它解决的问题:让「模型说它对」换成「Lean 说它对」
数学推理是 AGI 讨论里最难自证的一块:模型给出一个证明,你怎么知道它不是看起来对的胡说?DeepSeek-Prover-V2 走的是形式化验证这条路——输出不是自然语言的推理链,而是 Lean 4 代码,由 Lean 内核逐行检查。检查器说通过,就是通过;这一层不依赖任何人的判断,也不依赖模型自己的置信度。
这也是本站在置信度体系里最看重的一类证据形态:数学是少数有形式化真值的领域。所以哪怕这个模型的分数是厂商自报(我们记 C 档),它自报的那个东西本身是可机械核验的,和「我们的模型在内部评测上更好」不是一回事。
模型规格与训练路线
| 维度 | 读数 | 为什么重要 |
|---|---|---|
| 规模与结构 | 671B MoE(与 DeepSeek-V3 同源) | 不是小模型硬训出来的证明器,是旗舰级底座上做形式化对齐 |
| 目标语言 | Lean 4 | 当前主流证明助手,库(mathlib)生态最厚 |
| 冷启动数据 | 由 DeepSeek-V3 做递归子目标分解,再用 7B 小模型逐个证子目标,合成训练数据 | 这是 V2 相对 V1 的核心工程创新:难题拆成小模型能证的小题,再合回大证明 |
| 强化学习 | 二元奖励(证明通过 / 不通过) | 奖励信号来自 Lean 内核而非人类偏好,不存在 reward hacking 到「看起来对」的空间 |
| 可获取性 | GitHub 公开仓库(约 1304 stars),含证法 ZIP 下载 | 可核验性比闭源模型高一档:证明文本可以直接拿去 Lean 里跑 |
递归子目标分解这一段是整条路线的关键,值得展开。竞赛级命题直接让模型一步证出来,成功率极低,于是 RL 阶段几乎没有正样本可学。V2 的做法是先让强模型把命题拆成一串子目标,再让一个 7B 的小模型去证每个子目标——小题的通过率高得多,于是合出来的完整证明就成了高质量训练数据。这本质上是「用可分解性换数据密度」,和 AlphaProof 那条靠海量搜索换质量的路是两种不同的成本结构。
基准读数(厂商自报)
- MiniF2F-test:88.9%(pass@8192 口径)。这是形式化竞赛数学最常用的公开基准,88.9% 在 2025-07 的时间点上处于公开读数的最高一档。
- PutnamBench:49 / 658。普特南竞赛题的难度远高于 MiniF2F,分母 658 说明这个榜还在早期,49 题是当时公开可读的领先读数之一。
- ProverBench(自建):325 题,其中包含 AIME 2024/2025 的 15 道题。自建基准的意义是覆盖 MiniF2F 之外的题型,但它同时也是最容易过拟合的地方,读这个数要打折。
三个数放在一起看的正确姿势:MiniF2F 的 88.9% 说明「形式化竞赛数学」这件事在 pass@8192 这个采样预算下已接近饱和;PutnamBench 的 49/658(约 7.4%)说明换成真正难的题,能力立刻掉一个数量级。这个落差就是当前形式化证明的真实水位,比任何一个单独的百分比都更有信息量。
与 Kimina 那条线的关系
本站同时收录了 Moonshot 的 Kimina-Prover。两条线的技术选择很不一样:Kimina 走「从 Qwen2.5-72B 出发做 RL + 整证生成(不给 prover 中间反馈)」,并在 2025-07 用 Kimina-Prover-72B 把 miniF2F 推到 92.2%;DeepSeek-Prover-V2 走「671B MoE + 递归子目标分解冷启动」,读数 88.9%。
直接比这两个数字要非常小心:两者的采样预算(pass@k)、miniF2F 版本(Kimina 还发布过修正版,指出原基准至少 5 道题有错)、以及是否使用 prover 中间反馈都不同。本站不把它们排成名次,而是并列收录,理由就是协议不可通约。这也是这个域至今没有第三方统一榜的后果:所有读数都是各家自己跑的。
边界
- pass@8192 是很大的采样预算:意味着要生成八千多个候选证明再筛。生产里的真实成本是这个数字,不是单次调用。拿它和 pass@1 的读数比是不成立的。
- 形式化 ≠ 解题:它证的是已经形式化好的命题。把一道自然语言题变成 Lean 命题(autoformalization)是另一道工序,这一步的错误率不在 88.9% 里。
- 671B MoE 的部署成本:即使 MoE 激活参数远小于总量,自托管仍需要多卡大显存,绝大多数团队只能走 API 或复用官方证法。
- ProverBench 是自建基准:自家题自家跑,存在过拟合与选择性报告的结构性风险。
- 只覆盖可形式化的数学:分析、几何直观、建模选择这些难以 Lean 化的部分不在能力面里。
我们的核验状态
事实来自 DeepSeek-Prover-V2 的 GitHub 仓库 README(实读全文,含训练路线、三个基准读数、证法 ZIP 说明)与其技术报告 arXiv:2504.21801。仓库是公开的,证明文本可下载并在 Lean 4 里独立核验,这一点比闭源模型强。
但置信度记 C(厂商宣称),原因很具体:本站没有跑过这些证明。我们没有在自有环境里下载证法 ZIP、用 Lean 4 + mathlib 复算 MiniF2F-test 的 88.9%,也没有独立复算 PutnamBench 的 49/658。基准数字全部来自厂商自报,采样预算与基准版本也是自报口径。要升到 A 档,需要:在固定的 Lean 4 + mathlib 版本上复算 MiniF2F-test 通过率与 pass@8192 的实际采样次数、把证法 ZIP 逐条喂给检查器统计真实通过率、以及在 Kimina 发布的修正版 miniF2F 上重跑以便与 Kimina 的读数可比。