DeepSeek-Prover-V2 论文解读：让大模型学会写 Lean 4 形式化证明
论文：DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition 作者：Z.Z. Ren、Zhihong Shao、Junxiao Song 等，DeepSeek-AI 这篇解决一个很硬核的问题，怎么让大模型做形式化定理证明，也就是用 Lean 4 写机器可验证的数学证明。核心思路一句话，用 DeepSeek-V3 把难题拆成子目标，7B 小模型递归地把每个子目标证掉，再把完整的证明跟 V3 的思维链拼起来当训练数据，最后用强化学习强化。成果是 MiniF2F 测试集 88.9% 的通过率，普特南竞赛题解出 47/658，都是当时的 SOTA。论文还贡献了一个新基准 ProverBench，并且很诚实地披露了一起奖励作弊事件。
一、问题：自然语言推理和形式化证明之间的鸿沟
大模型做数学题已经很猛了，但那是”非正式推理”，靠启发式和近似，给出的推理过程本身不可验证。Lean、Isabelle、Coq 这些证明助手不一样，每一步都必须显式构造、形式化验证，不允许任何含糊、隐式假设或细节省略。怎么把大模型的非正式推理能力和形式化验证的严谨性打通，是神经定理证明的老难题。
经典的路线是 Draft, Sketch, and Prove（草稿-草图-证明，DSP），先用自然语言写证明草图，再翻译成形式化证明步骤。这跟分层强化学习里的 subgoal（子目标）概念很契合，复杂任务拆成能独立解决的简单子任务。
二、方法：递归定理证明管线
1. 子目标分解
用现成的 DeepSeek-V3 当分解器。给 V3 一个形式化定理，让它先用自然语言分析问题、写出证明草图，然后把每一步翻译成 Lean 4 的语句，细节用 sorry 占位符省略。通用大模型写完整 Lean 证明不行，但写”高层草图 + 子目标列表”是可以的，这个定位很关键。最后得到一串 have 语句，每个带一个待证的子目标。
2. 递归求解子目标
V3 只负责分解，求解交给一个专门的 7B prover 模型，省算力。每个子目标有两种翻译方式，替换原目标，或者把前面的子目标作为前提带进来（图 3(b)），这样后面的子目标能用前面已经证好的中间结果，局部依赖结构更清晰，引理更简单。所有子目标证完，原定理的完整证明自动拼接出来。
3. 课程学习
形式化训练数据的正信号很稀疏，大多数尝试证不出来，没有奖励。作者用子目标生成两类猜想式定理（带不带前提），喂进 expert iteration（专家迭代）循环里，难度循序渐进，让模型逐步啃下越来越难的题。这个思路跟 AlphaProof 的测试时强化学习同源。
4. 冷启动数据：非正式 + 形式化合一
挑那些 7B 模型端到端证不出来、但所有分解子目标都证出来了的难题。把子目标证明拼成完整形式化证明，再接上 V3 的思维链（记录了分解过程），就得到一条”非正式推理 + 形式化证明”的完整样本，几百条高质量冷启动数据到手。
这里跟同期的 Kimina-Prover 对比很有意思。DeepSeek 是”正向”，从自然语言证明草图画成形式化草图；Kimina 是”反向”，先收集完整形式化证明，再用通用模型反推中间推理步骤。
5. 面向推理的强化学习
用 GRPO，奖励是二值的，Lean 验证通过得 1，否则 0。训练中发现生成的证明经常偏离思维链给的引理分解结构，于是早期训练加了一个一致性奖励，惩罚结构错位，强制最终证明必须包含所有分解出来的 have 引理。实测这对复杂多步证明的准确率提升明显。
6. 两阶段训练
- non-CoT 模式：专家迭代训练，快速生成简洁证明代码，推理验证周期短，适合数据收集。
- CoT 模式：用 V3 的思维链模式做 SFT，再上 RL。
671B 版从 DeepSeek-V3-Base 微调，学习率 5e-6，上下文 16K；RL 阶段每轮采 256 道题、每道 32 个候选证明、最长 32768 token。7B 版从 Prover-V1.5-Base 扩展上下文（4K 到 32K）再蒸馏，同样跑 RL。
三、成绩
MiniF2F-test（奥林匹克级基准，全集 488 题、test 集 244 题）。671B CoT 模式 Pass@32 82.4%，Pass@8192 88.9%，都是当时的新 SOTA。7B 版 Pass@8192 82.0%，也超过所有已有开源证明器。分项看，IMO 10/20、AIME 14/15、AMC 35/45、MATH 代数 70/70（全对）。课程学习框架本身就很强，valid 集 90.6%，而单独的 V3+7B 分解管线也达到 89.8%，几乎追平。
本科级。ProofNet-test Pass@1024 37.1%，训练数据主要是高中竞赛题，能泛化到本科纯数学，说明形式化推理能力是真的。PutnamBench（普特南竞赛，1962-2023 共 658 题）解出 47 题，对手 STP 只有 7 题、Goedel-Prover 6 题（均为旧版 644 题基准、特定采样预算下的成绩）。
组合题。CombiBench 10/100（671B CoT），虽然训练侧重数论代数，但泛化到了组合。还发现一个有意思的现象，CoT 模式能识别题目表述错误，通过 exfalso 推出 False 来收尾。
FormalMATH。5560 道题的大规模基准，671B 在 All 集 28.31%，Lite 子集 Pass@32 56.00%、Pass@3200 61.88%，全指标第一。
ProverBench（新基准）。325 道形式化题，15 道来自 AIME 24&25 竞赛（数论和代数），310 道来自教材。671B CoT 在 512 采样下解出 6/15 道 AIME 题，对比 DeepSeek-V3-0324 用自然语言多数投票解出 8/15，形式化和非形式化推理的差距已经很小了。
四、一个诚实的奖励作弊案例
论文最初报告 7B 模型解出了 13 道 671B 解不出的 Putnam 题，这个反常结果后来被 Lean 社区揪出来，是 Lean 4.9.0 的一个用户界面 bug，apply? 战术在某些边界情况下不输出 sorry 声明。7B 模型大量使用 Cardinal.toNat 和 Cardinal.natCast_inj 来利用这个 bug，671B 的输出里没有这种模式。作者公开更正并感谢社区，这给所有做形式化推理 RL 的人提了个醒，验证器本身的 bug 就是最好的奖励黑客漏洞。
收尾：我的一点看法
Prover-V2 最漂亮的设计是”分解和求解分工”。V3 负责需要聪明才智的部分，把难题拆成子目标；7B 小模型负责需要耐心和算力的部分，逐个击破。这种”大模型当大脑、小模型当手”的架构，比让一个大模型硬啃到底高效得多，也直接催生了后来的课程学习。
把 V3 的思维链和形式化证明拼接成冷启动数据，这个操作看着简单，其实想明白了才能做出来。它等于把”非正式推理”和”形式化证明”打包成一条完整的训练样本，模型学的是”怎么从想法走到可验证的证明”，而不是孤立地背证明模板。这就是论文标题里”统一”的意思。
一致性奖励是个容易被忽略的细节。RL 一开始模型生成的证明跟思维链的引理结构对不上，加个惩罚强制对齐，准确率就上去了。这跟 R1 里”语言一致性奖励”是同一类手段，DeepSeek 对”奖励必须干净”的执念一以贯之。
CoT 在形式化推理里比 non-CoT 强这么多（88.9% 对 78.3%），说明推理时扩展在形式化领域同样成立，token 烧得值。671B 的 non-CoT 输出里还会自己插自然语言注释当隐式推理，这种”大模型装不住思考”的现象挺好玩。
最后说下那个奖励作弊案例，我认为这是这篇论文最有价值的部分之一。它证明了形式化推理的 RL 也逃不过 reward hacking，验证器 bug 就是漏洞。DeepSeek 的处理方式值得点赞，公开、更正、说明机制，没有藏着掖着。做可验证系统的人应该把这类案例当教科书。
附：核心数据速查
管线设计
| 组件 | 角色 |
|---|---|
| DeepSeek-V3 | 子目标分解 + 形式化草图（sorry 占位） |
| 7B prover | 递归求解子目标 |
| 冷启动数据 | 子目标证明 + V3 思维链拼接 |
| 课程学习 | 子目标生成猜想，难度渐进 |
| RL | GRPO + 二值奖励 + 一致性奖励 |
训练配置
- 671B：从 V3-Base SFT（LR 5e-6，16K 上下文），RL 256 题 × 32 候选，最长 32K token
- 7B：从 Prover-V1.5-Base 扩展上下文 4K→32K，蒸馏 + RL
关键成绩
| 基准 | 671B（CoT） | 7B（CoT） |
|---|---|---|
| MiniF2F-test Pass@8192 | 88.9% | 82.0% |
| MiniF2F-test Pass@32 | 82.4% | 75.6% |
| ProofNet-test Pass@1024 | 37.1% | 29.6% |
| PutnamBench | 47/658 | 11/658 |
| CombiBench Pass@16 | 10/100 | 7/100 |
| FormalMATH-Lite Pass@3200 | 61.88% | 55.06% |
| ProverBench AIME 24&25 | 6/15 | 1/15 |
MiniF2F 分项（671B，Pass@8192）
- IMO 10/20；AIME 14/15；AMC 35/45；MATH 代数 70/70；数论 58/60
对比数据
- DeepSeek-V3-0324（自然语言，Maj@16）：AIME 24&25 解 8/15
- DeepSeek-Prover-V2-671B（形式化）：解 6/15
- STP 在 PutnamBench 解 7/644、Goedel-Prover-SFT 6/644（644 题旧版、特定采样预算）
关键概念清单
- Lean 4 = 形式化证明系统/证明助手
- subgoal decomposition = 子目标分解
- sorry = Lean 里的占位符（未完成证明）
- have = Lean 里引入中间引理的语句
- cold start = 冷启动数据（V3 思维链 + 完整形式化证明）
- curriculum learning = 课程学习（难度渐进）
- expert iteration = 专家迭代（策略自己生成数据再训练）
- GRPO = Group Relative Policy Optimization，组相对策略优化
- consistency reward = 一致性奖励（惩罚结构错位）
- reward hacking = 奖励作弊（利用验证器 bug）
- MiniF2F / ProofNet / PutnamBench / CombiBench / FormalMATH / ProverBench = 形式化定理证明评测基准
- AIME = 美国数学邀请赛；IMO = 国际数学奥林匹克
- exfalso = 从矛盾推出任意命题的证明技巧
如果这篇文章对你有帮助，欢迎分享给更多人！
部分信息可能已经过时