跳转至

DeepSeekMath-V2：迈向可自验证的数学推理

暂无精读笔记。以下展示中文译文（点「译文」进入独立译文页）。

跳转：原文 EN · 译文 ZH · 原文 PDF

DeepSeekMath-V2：迈向可自验证的数学推理

中文结构化译文草稿，基于同目录 main_en.md 和本地 PDF。
作者与组织：DeepSeek-AI。
本地材料：paper.pdf、main_en.md、figures_png/、source/。

摘要翻译

传统数学推理 RL 通常用最终答案是否匹配 ground truth 作为 reward。这对 AIME、HMMT 等最终答案型竞赛足够有效，但有两个根本问题：第一，最终答案正确不等于推理正确，模型可能靠错误逻辑或偶然抵消得到正确答案；第二，该机制不适用于 theorem proving，因为证明题往往没有短数值答案，核心目标是严谨推导。

DeepSeekMath-V2 试图训练 LLM 具备自然语言证明的验证能力：模型不仅要生成证明，还要识别证明中的问题，并利用验证反馈迭代改进证明。论文构建 verifier、meta-verifier 和 proof generator 的协同训练流程，使生成器能够进行 faithful self-verification。最终模型在 IMO 2025、CMO 2024、Putnam 2024 等高难数学竞赛上取得很强结果。

论文定位

这篇论文的核心不是 final-answer RL，而是把数学推理推进到“自然语言证明 + 自验证”。它把 verifier 当作 proof generator 的 reward model，并进一步训练 generator 学会像 verifier 一样审查自己的证明。

方法

证明验证器

给定问题 \(X\) 和证明 \(Y\)，verifier 输出 proof analysis，然后给出三档分数：

  • 1：完整、严谨，所有逻辑步骤清楚。
  • 0.5：整体逻辑成立，但有小错误或细节缺失。
  • 0：存在致命逻辑错误或关键缺口。

初始数据来自 AoPS contest problems，优先选择 olympiad、team selection tests 和 2010 年后的 proof-required problems，总计 17,503 道。候选证明由 DeepSeek-V3.2-Exp-Thinking 的变体生成，再由数学专家按 rubric 标分。

verifier 的 RL reward 包括：

\[ R_{\text{format}} \]

用于约束输出格式，以及：

\[ R_{\text{score}}(s_i', s_i)=1-|s_i'-s_i| \]

用于奖励预测分数接近专家标注。

Meta-verification

只奖励 verifier 预测正确分数会带来漏洞：对于错误证明，verifier 可能预测出正确低分，却 hallucinate 不存在的问题。为解决这个问题，论文训练 meta-verifier 来评估 verifier 的分析本身是否准确、是否能支撑它给出的分数。

meta-verifier 数据形如：

\[ \mathcal{D}_{mv}=\{(X_i,Y_i,V_i,ms_i)\} \]

其中 \(V_i\) 是 verifier 对证明的分析，\(ms_i\in\{0,0.5,1\}\) 是数学专家标注的分析质量分数。

增强后的 verifier reward 为：

\[ R_V=R_{\text{format}}\cdot R_{\text{score}}\cdot R_{\text{meta}} \]

这样 verifier 不仅要给对分数，还要提出真实、合理的问题。

证明生成器和自验证

proof generator 用 verifier 的证明分数作为 reward：

\[ \max_{\pi_\theta}\mathbb{E}_{X_i,Y_i}[R_Y] \]

但论文发现，直接让 generator 一次性生成证明并自评时，它往往会虚假声称自己的证明正确。因此训练时要求 generator 输出证明 \(Y\) 和自分析 \(Z\)，并由 verifier 同时评估证明质量和自分析质量。

总 reward 为：

\[ R=R_{\text{format}}(Y,Z)\cdot(\alpha R_Y+\beta R_Z) \]

其中 \(\alpha=0.76,\beta=0.24\)。这让模型承认错误、修正错误比盲目宣称正确更有利。

实验结果

评测包括：

  • in-house CNML-level theorem proving problems：91 题，覆盖 algebra、geometry、number theory、combinatorics、inequality。
  • IMO 2025、CMO 2024、Putnam 2024。
  • IMO Shortlist 2024。
  • IMO-ProofBench basic / advanced。

主要结果：

  • one-shot 生成中，DeepSeekMath-V2 在 CNML-level 各类题上超过 GPT-5-Thinking-High 和 Gemini 2.5 Pro，分数由论文自家 verifier 评估。
  • sequential refinement 中，模型先生成 proof+self-analysis，再基于自验证结果多轮修改；在 IMO Shortlist 2024 上，Pass@1 与 Best@32 随迭代次数提升。
  • high-compute search 中，每题初始化 64 个 proof samples，每个 proof 生成 64 个 verification analyses；之后选高分证明并用问题分析继续 refine，最多 16 轮或直到 proof 通过全部 64 次验证。
  • 人类专家评估显示，模型在 IMO 2025 解出 5/6 题，CMO 2024 解出 4 题并有一题部分分，Putnam 2024 得到 118/120。

图表要点

  • Figure 1：CNML-level 各类别平均证明分数，说明 one-shot 下 DeepSeekMath-V2 在多数学科上领先；但该图依赖论文自家 verifier。
  • Figure 2：IMO Shortlist 2024 的 sequential refinement 曲线，展示自验证迭代能提高证明质量。
  • Figure 3：IMO-ProofBench basic / advanced 的专家评估，显示 DeepSeekMath-V2 在 basic 上很强，在 advanced 上与 Gemini Deep Think IMO Gold 仍有竞争关系。
  • Table 1：IMO 2025、CMO 2024、Putnam 2024 的高算力搜索结果，其中 Putnam 2024 为 118/120。

局限

论文的 in-house 和 refinement 曲线大量依赖自家 verifier，因此不是完全独立评估。最终竞赛题结果有专家评估支撑，但 verifier 在训练和 test-time scaling 中仍是核心假设。另一个局限是它关注自然语言证明，不是 Lean/Coq 形式化证明，因此严谨性仍需人类或更强验证器抽查。