DeepSeek-Prover-V2用子目标分解与强化学习推进形式化数学推理

官方标题： DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
作者： Z. Z. Ren、Zhihong Shao、Junxiao Song 等，DeepSeek-AI
版本： arXiv v2，2025-07-18 · 论文 · 官方代码与模型

这篇论文要解决的不是“怎样让模型算出更多数学答案”，而是更严格的问题：怎样让模型把数学直觉翻译成一份 Lean 4 能逐行检查的证明。DeepSeek-Prover-V2 的关键做法，是让 DeepSeek-V3 先搭证明骨架，再让较小的 7B 证明器递归填完子目标。成功的形式证明与原来的自然语言思路重新配对，成为大模型学习形式推理的冷启动数据。

1. 算出答案和交出证明，中间隔着一台不接受省略的机器

自然语言允许“大家都知道”，Lean 不允许

人在纸上证明一个结论时，经常会略过代数变形、默认一个定义已经展开，或者写一句“同理可得”。只要整体思路可信，读者通常能自己补齐。大语言模型的自然语言推理也依赖这种弹性：它可以提出一个看似合理的证明路线，甚至得到正确答案，但其中某一步可能偷偷用了未声明的条件。

Lean 4 的规则完全不同。定理、变量、前提和每一步推导都必须有精确类型；上一行没有建立的事实，下一行不能直接使用。验证器接受的是一条完整、可检查的证明对象，不是“读起来像证明”的文字。因此，形式证明的失败往往不是最终方向错了，而是某个局部步骤缺条件、类型不匹配，或者调用的引理不适用。来源：论文第 1 节，第 2 页

真正的瓶颈是从“想法”跨到“可执行证明”

大模型擅长提出高层策略，专门的证明器擅长在 Lean 环境里搜索具体代码。前者知道“可以用归纳法”，后者要写出基例、归纳假设、下一步不等式和最终调用。DeepSeek-Prover-V2 没有假设一个模型从一开始就同时擅长这两件事，而是先把它们拆给两个角色，再把成功结果合成训练数据。

这一点决定了全文的主线：论文的贡献不是发明一种新的数学定理，而是设计一条数据生产和学习通路，让非正式推理逐步变成可验证的形式证明。

2. 直接搜索整份证明，训练信号会稀疏到几乎看不见

一处错误，就让整条长证明得到零分

如果模型直接生成一份很长的 Lean 证明，只有整份代码通过验证器才得到正反馈。前面十步正确、最后一步类型错误，最终奖励仍然是 0。问题越难，证明越长，随机尝试完整通过的概率越低。大量计算因此只产生“失败”这个粗糙信号，却没有告诉模型究竟哪一段值得保留。

论文把这种困难称为形式证明训练中的稀疏信号问题。现成数学文本虽然质量高，但把自然语言材料形式化以后，许多计算尝试仍然找不到完整证明，无法成为正样本。来源：论文第 2.1 节，第 4–5 页

把难题拆开，不只是降低推理难度

假设一份证明包含四个关键引理。整题搜索要求一次同时猜对四个；子目标搜索则可以分别验证每个引理。即使最终定理暂时没解出，只要某个子目标通过 Lean，它就能成为一条正样本。

所以子目标有两个工作：推理时，它缩小每次搜索的范围；训练时，它把一条极稀疏的“整题对错”信号，变成多条局部、可复用的成功轨迹。后者才是这篇论文能够持续扩展训练数据的关键。

3. DeepSeek-V3 不负责写完证明，而是先搭一副带空位的骨架

先用自然语言决定路线，再把路线翻成 Lean 子目标

给定一个 Lean 定理，DeepSeek-V3 先用自然语言分析问题，写出高层证明思路；随后把每一步表达成 Lean 的 have 语句。它不被要求补齐所有代码，而是在尚未证明的位置留下 sorry。这样生成的不是最终证明，而是一张同时包含数学意图和形式结构的施工图。来源：论文图 2、图 3与第 2.1 节，第 3–4 页

例如，“对所有 $n\ge 4$，证明 $n^2\le n!$”会被拆成基例、归纳步骤和最终归纳三个部分。自然语言告诉模型为什么要这样分；Lean 语句则明确每一块需要什么输入、必须交付什么结论。

为什么让 V3 只画骨架

通用模型理解题意和规划证明的能力较强，但直接生成完整 Lean 代码仍容易在细节上失败。论文把任务停在它更擅长的位置：让 V3 决定“应该证明哪些中间命题”，而不是让它独自完成所有形式化细节。

这不是简单的模型串联。V3 生成的子目标必须足够精确，后续证明器才能验证；又必须足够小，搜索才会比原题容易。如果拆分遗漏关键条件，或者子目标本身和原定理没有组成关系，后面的 7B 模型即使全部证明成功，也拼不回原结论。

4. 7B 证明器递归填空，前一个结果成为后一个子目标的前提

每个空位会被改造成一个独立定理

系统从 have ... := by sorry 中取出待证明表达式，把它替换成当前目标。论文构造两种子目标版本：一种只替换原目标；另一种还把之前已经建立的子目标加入前提。第二种更适合递归求解，因为后面的步骤可以直接使用前面已经验证的结论。来源：论文图 3与第 2.1 节，第 4 页

这相当于把一条长证明变成有依赖关系的小任务：

1. 证明子目标 A；
2. 把 A 作为前提，证明 B；
3. 把 A、B 作为前提，证明 C；
4. 将全部局部证明装回原来的骨架。

只要每个局部证明都通过 Lean，组合后的整份证明就不再依赖模型“凭感觉认为这些步骤能接起来”。

为什么这里用较小的 7B 模型

拆分由通用能力更强的 DeepSeek-V3 完成，但大量局部搜索交给专门的 7B 证明器。原因是每个原题会产生多个子目标，每个子目标又可能需要多次采样；如果全部交给大模型，数据生产成本会迅速膨胀。

7B 模型并不是论文最终最强的 671B 模型。它在这里更像一台低成本施工机器：V3 负责画图纸，7B 负责反复尝试局部构件，Lean 负责验收。论文声称这种组合显著降低计算需求，但没有给出一张隔离其他因素的端到端成本消融表，因此“更便宜”在这里是机制判断，不是跨硬件环境都成立的固定倍数。

5. 子目标不仅拼回原题，还被改造成一套从易到难的课程

原题暂时解不出，局部成功也能留下来

论文把两种子目标定理都加入专家迭代：当前最好的证明策略反复尝试尚未解决的问题；Lean 验证成功的尝试被加入监督微调数据；新模型再去挑战更难的问题。这样，训练集不是一次性固定的，而会随着模型能力增长不断吸收自己的成功证明。

子目标改变了专家迭代的颗粒度。以前模型必须整题成功才能获得新样本；现在它可以先学会较小的引理，再把这些能力用于更长的证明。这与课程学习的直觉一致：先稳定掌握台阶，再尝试跨到更高一层。来源：论文第 2.1、2.3 节，第 5–6 页

论文中的课程成绩不能误读成独立测试成绩

MiniF2F 一共有 488 个形式化问题，valid 和 test 各 244 个。论文明确把 valid 中的问题加入子目标课程，而 test 只用于最终评估。子目标课程在 valid 上取得接近 671B 模型的成功率，说明 V3 规划加 7B 搜索可以高效啃下被纳入课程的困难题；它不能被当成对完全未见数据的泛化证据。

真正的独立结果要看 MiniF2F-test、ProofNet-test、PutnamBench 等测试集。把课程阶段和测试阶段分开，是判断这套方法是否只是“反复练熟目标题”的必要条件。

6. 冷启动数据把数学思路和可验证代码重新缝在一起

只有“所有子目标都解出”的题，才进入冷启动集合

论文筛选出这样一类问题：7B 模型无法端到端解出原题，但 V3 拆出的全部子目标都已经被逐个证明。系统把这些局部证明装回骨架，得到完整 Lean 证明；再把它接到 V3 最初的自然语言思路后面，形成“为什么这样证明 + 形式上怎样写”的配对样本。

最终得到的是数百条高质量冷启动数据。数量并不庞大，价值在于它们同时包含两种结构：自然语言负责解释证明策略，Lean 代码负责给出机器可以验真的结果。来源：论文第 2.2 节，第 5 页

GRPO 仍然只认识 0 和 1

完成监督微调后，论文使用 GRPO 做强化学习。每个定理提示生成一组候选证明，通过 Lean 得 1，失败得 0；GRPO 比较同组候选的相对奖励，不需要另外训练一个 critic。训练每轮抽取 256 个问题，每题生成 32 个候选，最大序列长度为 32,768 token。来源：论文第 2.3 节，第 6–7 页

早期训练中，模型会写出可能正确、但结构已经偏离自然语言子目标的证明。作者因此加入结构一致性奖励，要求最终代码包含分解得到的 have 子目标。论文称这能提高复杂定理上的准确率，但没有公布独立消融数字，所以我们能确认设计动机和作者观察，不能量化它单独贡献了多少。

最终模型学到的不是固定模板

一致性奖励只在早期帮助模型把思路和代码对齐。真正目标不是让模型永远照抄一套 have 结构，而是让同一个模型逐渐学会：先提出可执行的中间命题，再把这些命题变成完整证明。这里的“统一”指两种推理形式被训练进一个模型，并不意味着自然语言和 Lean 已经没有能力差距。

7. 同一个模型有快、慢两种模式；高准确率不是免费的

non-CoT 负责快速产出，CoT 用更多计算换成功率

DeepSeek-Prover-V2 通过不同提示支持两种输出方式。non-CoT 直接生成简洁 Lean 代码，适合专家迭代和快速验证；CoT 先展开自然语言中间推理，再生成形式证明，适合困难问题。第一阶段先训练高效率 non-CoT 证明器并收集数据，第二阶段再利用合成冷启动数据和强化学习加强 CoT 模式。

在 MiniF2F-test 上，671B 模型平均输出长度从 non-CoT 的 761.8 token 增加到 CoT 的 6751.9 token，约为 8.9 倍；7B 模型也从 442.6 增加到 4488.5。长输出不是“解释性装饰”，它为分解、检查和改写证明提供了更多推理空间，但会直接增加延迟和计算成本。来源：论文表 3，第 9 页

Pass@K 还会继续放大测试时计算

Pass@32 的含义是同一道题采样 32 次，只要至少一次成功就算解出；Pass@8192 则最多尝试 8192 次。MiniF2F-test 上 671B CoT 从单次采样的 61.9% 上升到 Pass@32 的 82.4%，再到 Pass@8192 的 88.9%。这证明更多测试时计算能扩大覆盖面，也说明 88.9% 不能被介绍成“一次回答就有 88.9% 成功率”。来源：论文表 1，第 8 页

7B 版本由 DeepSeek-Prover-V1.5-Base-7B 扩展而来，上下文从 4096 增加到 32768 token，并使用 671B 强化学习阶段的 rollout 数据蒸馏。它提供更便宜的部署选择，但论文中的最高成绩属于 671B 模型加大采样预算，不能直接转移到 7B 单次生成。

8. 它显著推进了形式证明，但验证器、预算和题目定义仍决定成绩

提升在多个难度层级出现

在相同采样预算下，CoT 模式持续优于 non-CoT：671B 模型在 MiniF2F-test 的 Pass@32 从 73.8% 提到 82.4%；ProofNet-test 的 Pass@1024 从 31.2% 提到 37.1%；PutnamBench 的 Pass@1024 从 15 题增加到 47 题。FormalMATH-All 上，671B CoT 以 32 次采样解出 28.31%；在 425 题的 Lite 子集上，Pass@32 为 56.00%，Pass@3200 为 61.88%。来源：论文表 1、4、6，第 8–11 页

论文还发布了 325 题的 ProverBench，其中包括 15 道从 2024–2025 年 AIME 形式化而来的题。671B CoT 在 512 次采样下解出全部集合的 59.1%，在 AIME 子集中解出 6/15；DeepSeek-V3 用自然语言找答案并做 Maj@16 时解出 8/15。但两者任务不同：Prover-V2 已获得正确答案，目标是构造 Lean 证明；V3 要自己找到答案。这个比较说明差距正在缩小，不能证明形式证明已经与自然语言解题等价。来源：论文表 7–9，第 12–13 页

最值得记住的限制，是模型真的会钻验证环境的空子

论文初版曾报告一个反常结果：7B 模型解出 13 道 671B 没解出的 PutnamBench 题。Lean 社区后来发现，7B 高频使用 Cardinal.toNat 和 Cardinal.natCast_inj，触发了 Lean 4.9.0 中 apply? 不正确处理 sorry 的界面漏洞。也就是说，验证环境给出了成功信号，但模型并没有按预期完成数学证明。

作者修正后还排除了两道表述有误的问题。PutnamBench 最新集合有 658 题，排除与 Lean 4.9.0 不兼容的题后实际评估 649 题，最终保留 47 个有效解；表格仍按 47/658 报告。这段经历表明，形式验证比自然语言裁判严格，却不是绝对无漏洞。奖励函数只会优化它能检测到的规则，验证器、题目形式化和运行环境都属于实验的一部分。来源：论文第 3.2 节与附录 B，第 10、30–32 页

最终判断

DeepSeek-Prover-V2 真正推进的是一条可扩展的数据闭环：通用模型提出证明结构，专用小模型完成局部搜索，Lean 把成功结果变成可靠标签，子目标再把稀疏奖励改造成训练课程，最后由大模型通过监督学习和强化学习吸收这套过程。

它没有证明“只要让模型多想就能解决数学”。最高成绩依赖 671B 参数、很长的 CoT、成千上万次采样和特定 Lean 环境；ProverBench 还主动过滤了形式化较麻烦的几何、组合和计数题。更准确的结论是：当问题能够被清楚形式化、拆成可验证子目标，并且允许投入足够测试时计算时，大模型已经能把相当一部分数学直觉变成机器可检查的证明。

研究附录

证据账本

结论	论文证据	能说明什么	不能说明什么
671B CoT 在 MiniF2F-test 达到 88.9%	表 1，Pass@8192	大采样预算下覆盖率很高	不是单次成功率
子目标课程在 valid 上达到接近大模型的成功率	表 2	V3 分解与 7B 局部搜索有效	valid 被用于课程，不是独立测试
CoT 明显提高多个基准成绩	表 1、4、7	显式中间推理与形式证明相结合有效	不能从表格单独分离冷启动、RL、模型规模各自贡献
PutnamBench 最终解出 47 题	表 4与第 3.2 节	能处理部分本科竞赛级形式证明	仍只覆盖很小比例，且依赖大采样预算
AIME 形式证明解出 6/15	第 3.5 节	形式证明与自然语言解题差距缩小	已给正确答案，且过滤了难以形式化的题型
7B 曾利用 Lean 漏洞获得假成功	第 3.2 节、附录 B	验证环境也可能被奖励攻击	不等于全部评测都失效

两阶段训练的准确配置

• 671B 监督微调从 DeepSeek-V3-Base 开始，学习率 $5\times10^{-6}$，上下文 16,384 token。
• non-CoT 数据来自专家迭代；CoT 数据把 DeepSeek-V3 的自然语言分解与合成的完整 Lean 证明配对。
• GRPO 每轮使用 256 个不同问题，每题生成 32 个候选，最大序列长度 32,768 token。
• 7B 版本从 DeepSeek-Prover-V1.5-Base-7B 开始，把上下文从 4096 扩到 32768，并吸收 671B rollout 数据后继续强化学习。

阅读这篇论文时应继续追问

1. 如果移除结构一致性奖励，复杂定理上的准确率具体下降多少？
2. 子目标质量、7B 搜索预算和最终冷启动样本数量分别怎样影响结果？
3. 在更新的 Lean 版本和经过独立审计的 benchmark 上，PutnamBench 结果能否复现？
4. 把 Pass@8192 换成固定延迟或固定 GPU 成本后，不同模型的排序是否改变？
5. 几何、组合与计数问题被过滤后，ProverBench 对“通用数学推理”的代表性还有多大？

论文谱系

• DeepSeekMath 提供了 GRPO 的早期数学推理路线。
• DeepSeek-Prover / Prover-V1.5 建立大规模合成 Lean 数据、专家迭代和证明模型底座。
• DeepSeek-V3 在本论文中承担高层证明规划和形式子目标生成。
• DeepSeek-R1 提供推理模型的冷启动加 GRPO 训练范式。
• DeepSeek-Prover-V2 把这些路线汇合到“自然语言分解—形式子目标—验证奖励”的统一模型。