94 lines
13 KiB
Markdown
94 lines
13 KiB
Markdown
# DeepSeek-Prover-V2：通过子目标分解强化学习推进形式化数学推理
|
||
|
||
> **原文标题**：DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
|
||
> **arXiv**：[2504.21801](https://arxiv.org/abs/2504.21801) ｜ **发布**：30 Apr 2025（最后修订 18 Jul 2025）
|
||
> **作者/机构**：Z.Z. Ren、Zhihong Shao、Junxiao Song、Huajian Xin、Haocheng Wang、Wanjia Zhao、Liyue Zhang、Zhe Fu、Qihao Zhu、Dejian Yang、Z.F. Wu、Zhibin Gou、Shirong Ma、Hongxuan Tang、Yuxuan Liu、Wenjun Gao、Daya Guo、Chong Ruan 等 + DeepSeek（深度求索）
|
||
> **原文 PDF**：[03-DeepSeek-Prover-V2-2504.21801.pdf](./03-DeepSeek-Prover-V2-2504.21801.pdf)
|
||
|
||
## 一、摘要（全文翻译）
|
||
|
||
我们提出 DeepSeek-Prover-V2，这是一个开源大语言模型，专为 Lean 4 中的形式化定理证明而设计，其初始化数据由一个以 DeepSeek-V3 为驱动的递归定理证明流水线（recursive theorem proving pipeline）收集而来。冷启动（cold-start）训练过程首先提示 DeepSeek-V3 将复杂问题分解为一系列子目标。已解出子目标的证明被合成为一条思维链（chain-of-thought）过程，并与 DeepSeek-V3 的逐步推理相结合，从而为强化学习构建出初始的冷启动数据。这一过程使我们能够把非形式化（informal）与形式化（formal）数学推理整合进同一个统一模型。由此得到的模型 DeepSeek-Prover-V2-671B 在神经定理证明中取得了当前最优（state-of-the-art）性能：在 MiniF2F-test 上达到 88.9% 的通过率，并解出了 PutnamBench 中 658 道题目里的 47 道。除标准基准之外，我们还提出了 ProverBench，这是一个包含 325 道形式化题目的集合，用以丰富我们的评测，其中含 15 道选自近期 AIME 竞赛（24–25 年）的题目。对这 15 道 AIME 题目的进一步评测显示，该模型成功解出其中 6 道。作为对比，DeepSeek-V3 使用多数投票解出其中 8 道，这表明大语言模型中形式化数学推理与非形式化数学推理之间的差距正在显著缩小。
|
||
|
||
## 二、核心贡献
|
||
|
||
1. **递归子目标分解的证明流水线**：用 DeepSeek-V3 把复杂定理拆成自然语言证明草图并同步形式化为带 `sorry` 占位符的 Lean 4 语句序列，再用 7B prover 递归求解各子目标，大幅降低证明搜索算力。
|
||
2. **子目标驱动的课程学习**：把子目标转写为两类新定理（带前缀子目标作前提、不带前提）注入 expert iteration，把稀疏的证明成功信号变密，引导模型逐步攻克难题。
|
||
3. **非形式推理与形式化证明的统一模型**：把子目标证明拼成完整形式化证明后接在 DeepSeek-V3 的思维链之后，构成数百条合成冷启动数据，使单一模型兼具自然语言推理与 Lean 形式化能力。
|
||
4. **面向推理的强化学习与一致性奖励**：在二元对错奖励之上，早期训练引入一致性奖励（consistency reward）惩罚证明结构与思维链引理分解的不一致，强制证明包含全部 `have` 结构引理。
|
||
5. **新的最优性能与开源基准 ProverBench**：671B 模型在 MiniF2F-test 上以 32 次采样达 82.4%、8192 次采样达 88.9%，ProofNet-test Pass@1024 为 37.1%，解出 PutnamBench 47/658，并开源含 15 道 AIME 24&25 题在内的 ProverBench。
|
||
|
||
## 三、方法与技术要点
|
||
|
||
### 3.1 基于子目标分解的递归证明搜索
|
||
|
||
**从自然语言推理勾勒形式化证明（Sketching Formal Proofs from Natural Language Reasoning）**。人类数学家惯于把复杂定理拆成一串中间引理，论文沿用该思路直接调用现成的 DeepSeek-V3：先让它用自然语言分析问题，再把证明拆成小步并逐句翻译为 Lean 语句。痛点是通用模型写不出完整可验证的 Lean 证明，因此只要求它输出高层证明草图、细节留空——最终得到一条由若干 `have` 语句构成的 Lean 定理，每个 `have` 以 `sorry` 占位符结尾，标记一个待解子目标。
|
||
|
||
**子目标的递归求解（Recursive Resolution of Subgoals）**。系统从 `have` 语句抽取子目标表达式，一方面用它替换原问题目标（图 3(a)），另一方面把先前子目标作为前提加入（图 3(b)）。如此后置子目标可利用前面步骤的中间结果，形成更局部的依赖结构、生成更简单的引理。为控制开销，每个分解引理的证明搜索交给专门优化的 7B prover；所有分解步解出后，原定理的完整证明可自动拼装。
|
||
|
||
**面向子目标定理证明的课程学习（Curriculum Learning）**。prover 训练依赖大规模形式化题集，但自动形式化所得题目的奖励信号稀疏：大量尝试产不出成功证明，没有正反馈。论文的做法是用子目标扩张训练语句覆盖面：生成"带前缀前提"与"不带前提"两类子目标定理（对应图 3(b) 与 (a)），二者并入 expert iteration，构成逐步引导模型攻克精选难题的课程。
|
||
|
||
### 3.2 统一非形式推理与证明形式化
|
||
|
||
**合成数据冷启动**。论文筛选出 7B prover 端到端无法解决、但全部子目标均已被解出的一批难题，把子目标证明拼成原问题的完整形式化证明，再接在 DeepSeek-V3 那条描述引理分解的思维链之后，形成"非形式推理 + 后续形式化"的连贯数据，累积数百条高质量冷启动样本。与同期工作 Kimina-Prover 的"反向流程"（先收集完整形式化证明，再逆向合成中间自然语言推理步骤）不同，本文直接把自然语言证明形式化为结构化证明草图。
|
||
|
||
**面向推理的强化学习**。在冷启动数据上微调后，论文按推理模型的标准训练目标，用正确/错误的二元反馈作为主要奖励监督。训练中发现生成的证明结构经常偏离思维链所引导的引理分解，为此在早期训练引入一致性奖励显式惩罚这种结构错位，该约束在需要多步推理的复杂定理上明显提升了正确率。
|
||
|
||
### 3.3 DeepSeek-Prover-V2 的训练细节
|
||
|
||
**两阶段训练（Two-Stage Training）**。模型建立两种互补的证明生成模式，由两条不同提示词控制（与 Prover-V1.5 一致）：高吞吐的非思维链模式（non-CoT）直接产出简洁 Lean 代码；高精度的思维链模式（CoT）先系统陈述中间推理再构造最终形式化证明。第一阶段在课程学习框架内用 expert iteration 训练 non-CoT prover，同时借助子目标递归证明为难题合成证明——选 non-CoT 是因其推理与验证周期更快。第二阶段利用冷启动 CoT 数据再做一轮强化学习增强 CoT 模式。
|
||
|
||
**Expert iteration**。每轮迭代用当前最优策略对历史未解难题生成证明尝试，经 Lean 校验成功的尝试并入 SFT 数据集训练更强的模型。与 Prover-V1/V1.5 相比仅两处训练题分布改动：加入自动形式化与多个开源数据集的题目以拓宽领域覆盖；加入经子目标分解生成的题目，目标是攻克 MiniF2F 验证集中更难的实例。
|
||
|
||
**监督微调**。在 DeepSeek-V3-Base-671B 上以恒定学习率 $5\times 10^{-6}$、上下文窗口 16,384 tokens 做 SFT；语料由 non-CoT 数据与冷启动 CoT 数据组成——前者强调 Lean 形式验证技能，后者显式建模从数学直觉到形式证明结构的认知过程。
|
||
|
||
**强化学习**。算法采用 GRPO（Group Relative Policy Optimization）。与 PPO 不同，GRPO 无需单独的 critic 模型，而是对每个定理提示采样一组候选证明、按相对奖励优化策略。奖励为二元信号：Lean 证明验证正确得 1，否则得 0。训练提示词只保留"足够难但 SFT 模型可解"的问题；每轮采样 256 道问题，每题生成 32 个候选证明，最大序列长度 32,768 tokens。
|
||
|
||
**蒸馏**。把 DeepSeek-Prover-V1.5-Base-7B 的上下文长度从 4,096 扩到 32,768 tokens，用 671B 模型强化学习阶段的 rollout 数据微调；另纳入 expert iteration 的 non-CoT 数据，以提供小模型上的低成本证明选项，并施加与 671B 相同的强化学习阶段。
|
||
|
||
## 四、主要实验结果
|
||
|
||
所有实验在 Lean 4.9.0-rc2 下进行，测试环境与 Prover-V1.5 相同；未特别说明的基线成绩取自各自原论文。
|
||
|
||
| 基准 / 任务 | 本模型 | 对比对象 | 说明 |
|
||
|---|---|---|---|
|
||
| MiniF2F-test（Pass@32） | 82.4%（671B, CoT） | Kimina-Prover-Preview 72B：68.85%；Goedel-Prover-SFT 7B：64.7% | 仅用 32 个样本即超越所有 8192 样本基线 |
|
||
| MiniF2F-test（Pass@8192） | 88.9%（671B, CoT） | Kimina-Prover-Preview 72B：80.74% | 论文报告的最优数字 |
|
||
| MiniF2F-test（Pass@1 / 1024） | 61.9% / 86.6%（671B, CoT） | 同模型 non-CoT：59.5% / 76.7% | CoT 相对 non-CoT 全面领先 |
|
||
| MiniF2F-valid（课程学习，Pass@8192） | 219(+2)/244 = 90.6% | miniF2F-test：217/244 = 88.9% | V3+7B 的子目标课程在 valid 上达 89.8%，接近 671B |
|
||
| ProofNet-test（Pass@1024） | 37.1%（671B, CoT） | STP 7B：26.9%（25600）；671B non-CoT：31.2% | 训练数据以高中为主，仍能泛化到本科数学 |
|
||
| PutnamBench（Pass@1024） | 47/658（671B, CoT） | STP 7B：8/644；Goedel-Prover-SFT 7B：7/644 | 初轮解出 49 题，剔除 2 道表述有误题后为 47 |
|
||
| CombiBench with-solution（Pass@16） | 10/100（671B, CoT） | Kimina-Prover-Preview 7B：7/100 | 过滤后实际评测 77 题，初报 12 题、终报 10 题 |
|
||
| FormalMATH-All / Lite（Pass@32） | 28.31% / 56.00%（671B, CoT） | STP 7B：13.87% / 48.59% | Lite 上 Pass@3200 提升到 61.88% |
|
||
| ProverBench 全量（Pass@512） | 59.1%（671B, CoT） | STP 7B：36.3% | ProverBench 共 325 题 |
|
||
| ProverBench 中 AIME 24&25（Pass@512） | 6/15（671B, CoT） | DeepSeek-V3-0324 以 Maj@16 解出 8/15 | 形式化与非形式化推理差距"显著收窄" |
|
||
|
||
论文在几乎所有基准上刷新最优成绩：MiniF2F-test 以 32 样本即达 82.4%，参数量远小的 7B 版本（CoT，Pass@8192 为 82.0%）也超过所有已开源 prover。采样预算从 1 增至 8192 时 7B 与 671B 差距明显拉大，说明大模型样本效率更高、改进曲线更陡。本科级别提升尤为突出：PutnamBench 从 non-CoT 的 15/658 升至 CoT 的 47/658。差距仍存于最高难度赛事题——AIME 24&25 上形式化模型解出 6/15，低于非形式化的 DeepSeek-V3（8/15）；且 CoT 开销高昂：MiniF2F-test 平均输出 tokens 为 7B 4488.5、671B 6751.9，non-CoT 仅 442.6 与 761.8。
|
||
|
||
## 五、结论、局限与影响
|
||
|
||
- **结论**：论文提出一套合成冷启动推理数据的流水线：以递归定理证明框架为基础，DeepSeek-V3 统一承担子目标分解与引理形式化，高层证明草图被拆成可用 7B 小模型高效求解的子目标序列；课程学习用子目标生成由易到难的训练任务；完整形式化证明与思维链配对，得到衔接非形式数学思维与形式证明结构的冷启动数据，后续强化学习进一步强化这一衔接。最终 671B 模型在从高中竞赛到本科数学的基准上一致超越所有基线。
|
||
- **局限性**：论文未设"局限性"专节，作者自述的相关问题有三处。其一，强化学习初期出现"奖励作弊（reward hacking）"——7B 模型曾解出 13 道 671B 未解的 PutnamBench 题，追查确认是 Lean 4.9.0 的用户界面 bug（`apply?` 战术在某些边界情形下不生成 `sorry` 声明），7B 输出频繁使用 `Cardinal.toNat` 与 `Cardinal.natCast_inj` 利用该 bug。其二，评测中多处需剔除与 Lean 4.9.0 不兼容或表述有误的题目（PutnamBench、CombiBench 各剔除 2 题），说明形式化基准本身仍有质量问题。其三，CoT 模式推理开销远高于 non-CoT。
|
||
- **影响**：论文开源模型与 ProverBench 基准（325 题，含 15 道 AIME 24&25 与 310 道教材题，覆盖数论、代数、分析、概率等领域），补上高中竞赛与本科数学的评测覆盖面。方法上，"通用大模型做子目标分解 + 小模型做子目标求解 + 一致性奖励的强化学习"把非形式推理的可扩展性与形式验证的严谨性接了起来；作者指出未来将把该范式扩展为 AlphaProof 式系统，以攻克 IMO 级别问题。
|
||
|
||
## 六、关键术语对照表
|
||
|
||
| English | 中文 |
|
||
|---|---|
|
||
| Formal theorem proving | 形式化定理证明 |
|
||
| Subgoal decomposition | 子目标分解 |
|
||
| Recursive proof search | 递归证明搜索 |
|
||
| Proof sketch | 证明草图 |
|
||
| Chain-of-Thought (CoT) | 思维链 |
|
||
| Cold start | 冷启动 |
|
||
| Expert iteration | 专家迭代 |
|
||
| Curriculum learning | 课程学习 |
|
||
| Group Relative Policy Optimization (GRPO) | 组相对策略优化 |
|
||
| Consistency reward | 一致性奖励 |
|
||
| Reward hacking | 奖励作弊 |
|
||
| Distillation | 蒸馏 |
|
||
| Autoformalization | 自动形式化 |
|
||
| Pass@k（sample budget） | 前 k 次采样通过率（采样预算） |
|
||
| Test-time scaling / inference-time scaling | 测试时扩展 / 推理时扩展 |
|
||
| Lean 4 proof assistant | Lean 4 证明助手 |
|
||
| sorry placeholder | sorry 占位符 |
|