DeepSeekMath-V2 技术白皮书：迈向自验证数学推理

引言

近年来，大型语言模型（LLM）在数学推理领域取得了令人瞩目的进展。然而，当前主流的训练方法——基于最终答案正确性进行强化学习——正面临着根本性的局限。这一方法存在两个核心问题：首先，正确的答案并不等同于严谨的推理过程，模型可能通过错误的逻辑或巧合得出正确答案；其次，对于定理证明这类不产生数值答案、而以严谨推导为核心目标的任务，该方法完全不适用。其结果是，即便模型在量化推理任务上表现优异，其生成的自然语言证明也常常包含数学谬误或逻辑矛盾。更关键的是，这类模型在验证能力上存在严重不足，表现出很高的“假阳性”率，即便面对包含明显逻辑漏洞的错误证明，也常常宣称其有效。

为了真正突破深度推理的极限，我们必须转向对数学推理过程本身的严谨性进行验证。本文将详细阐述DeepSeekMath-V2模型所采用的自验证（Self-Verification）方法，这是一种旨在训练模型识别并解决自身推理缺陷的新范式，以期构建更可靠、更强大的数学AI系统。

1. 核心理念：自验证作为数学推理的新范式

从单纯追求“答案生成”到实现“过程自验证”，是推动人工智能进行高级数学推理的必要范式转变。这一转变的核心在于，赋予模型一种类似人类专家的能力——即在没有标准答案的情况下，独立评估和持续改进其自身的推理链条。这种能力是通往解决未知开放性问题的关键一步。

1.1. 分析自验证的理论动机

我们的自验证方法论，源于对数学推理本质的三个核心洞见：

• 类人能力 (Human-like Capability): 人类数学专家即使在面对没有已知解的开放性问题时，也具备识别证明中逻辑谬误的能力。这是AI系统需要学习的关键技能，是实现真正智能推理的基础。
• 置信度代理 (Proxy for Confidence): 如果一个证明在经过大规模、多角度的验证尝试后仍未发现任何问题，那么我们可以高度确信其有效性（validity）。验证的深度和广度，可以作为衡量证明可信度的代理指标。
• 质量衡量与优化 (Measure of Quality for Optimization): 识别一个证明中存在的有效问题所需的努力程度，本身就可以作为衡量该证明质量的反向指标。这一指标可被直接用于优化证明的生成过程，引导模型产出更高质量的推理。

1.2. 构建协同进化框架

基于上述理论动机，我们构建了一个验证与生成相互促进的迭代改进循环（iterative improvement cycle）。该框架通过一个自我增强的闭环系统，持续提升模型的数学推理能力：

1. 验证反馈优化生成： 利用验证器提供的反馈来优化证明生成器的性能，使其产出更严谨的证明。
2. 增强的生成器反哺验证器： 经过优化的、更强大的生成器会产出更具挑战性、难以验证的新证明。通过扩展验证计算，我们可以对这些新证明进行自动化标注，从而为验证器自身创造新的、高质量的训练数据。
3. 增强的验证器驱动新一轮优化： 使用经过数据增强的、能力更强的验证器，来更精准地指导下一轮的证明生成过程，从而开启新一轮的性能提升。

这一核心理念的实现，需要一套创新的技术架构与训练流程作为支撑，我们将在下一章节中进行详细阐述。

2. 核心技术架构与训练流程

本节将深入剖析DeepSeekMath-V2实现自验证能力的技术内核。我们将分步解析证明验证器（Proof Verifier）和证明生成器（Proof Generator）的训练方法，重点阐述元验证（Meta-Verification）和自我评估（Self-Evaluation）等关键创新。最终，我们将揭示两者如何协同进化，形成一个可持续提升的智能系统。

2.1. 第一阶段：构建高精度、高忠实度的证明验证器 (Proof Verifier)

构建一个可靠的验证器是整个自验证体系的基石。验证器的核心任务是根据一套高级评估准则（high-level rubrics I_v），对给定的数学证明进行深入分析，识别其中存在的问题，并给出一个综合评分。

评分体系分为三个等级：

• 1分: 证明完全正确、严谨，所有逻辑步骤清晰合理。
• 0.5分: 证明的整体逻辑框架正确，但存在次要的计算错误或细节遗漏。
• 0分: 证明存在根本性的逻辑错误或关键性空白，完全无效。

2.1.1. 验证器的初步训练

为了冷启动强化学习（RL）过程，我们首先构建了一个初始数据集。我们从知名数学竞赛网站 Art of Problem Solving (AoPS) 爬取了17,503个需要证明的问题，使用基础模型生成候选证明，并邀请数学专家根据上述评分准则进行人工标注。

随后，我们通过RL训练验证器 π_φ，其目标是最大化期望奖励。该RL目标函数定义如下： max_{π_φ} E[…] [R_format(V’_i) · R_score(s’_i, s_i)] 其中，奖励由两个部分组成：

• 格式奖励 (R_format): 这是一个指示函数，确保验证器的输出严格遵循格式要求，即必须包含问题总结和最终得分两个部分。
• 分数奖励 (R_score): 该奖励旨在使验证器预测的分数 s’_i 与专家标注的分数 s_i 保持一致，其计算公式为 R_score = 1 - |s’_i - s_i|。

2.1.2. 创新引入：元验证 (Meta-Verification)

仅依赖分数奖励存在一个潜在的风险：验证器可能会通过捏造不存在的问题来“欺骗”奖励函数，从而在预测分数正确的同时，降低其分析内容的忠实度（faithfulness）。

为解决这一问题，我们引入了“元验证”这一关键创新。元验证的核心作用是引入一个更高层级的评估，判断验证器所识别出的问题是否真实存在，以及这些问题是否能从逻辑上支撑其给出的分数。

元验证器的训练和应用流程如下：

1. 我们首先训练一个专门的元验证器 π_η，其任务是根据一套元验证准则 I_mv 来评估验证器分析报告的质量。
2. 然后，我们将元验证器给出的质量评分 R_meta 作为一个新的奖励项，整合进验证器的总奖励函数中，形成 R_V = R_format · R_score · R_meta。
3. 通过引入元验证，我们观察到验证器分析报告的平均质量分（由元验证器评估）从0.85显著提升至0.96，同时保持了分数预测的准确性，这表明模型的忠实度得到了极大增强。

经过这一阶段的训练，最终得到的模型具备了执行证明验证和元验证的双重能力。

2.2. 第二阶段：训练具备自我评估能力的证明生成器 (Proof Generator)

在拥有了一个可靠的验证器后，下一步便是训练一个能够利用该验证器进行自我提升的证明生成器。

2.2.1. 基础生成器训练

初始步骤相对直接：我们将训练好的验证器 π_φ 作为生成式奖励模型，通过强化学习来训练证明生成器 π_θ。其核心RL目标是最大化由验证器给出的证明分数 R_Y： max_{π_θ} E[…] [R_Y]

2.2.2. 核心增强：融合自验证能力

我们观察到一个关键现象：标准的生成器在外部反馈的指导下可以修正其证明，但它缺乏主动识别自身错误的“内省”能力，因而倾向于高估自己工作的正确性。

为了解决此问题，我们训练生成器 π_θ 在产出证明（Y）自我分析（Z）。这份自我分析遵循与验证器完全相同的格式和评估准则 I_v。用于训练的复合奖励函数如下：

R = R_format(Y,Z) · (α · R_Y + β · R_Z)，其中 α=0.76，β=0.24。

这里的关键在于自我分析的奖励 R_Z，它由验证器进行评估，其计算方式为： R_Z = R_score(s’,s) · R_meta(Z)

其中，s’ 是生成器在自我分析中给自己打的分数，s 是外部验证器给出的真实分数。R_score 奖励自我评分的准确性，而 R_meta 则奖励自我分析文本内容的忠实度和质量。

该奖励结构为模型创造了三重激励机制：

• 激励忠实性: 忠实地承认自身证明中存在的错误（s’接近s，且R_meta高），比虚假地声称其完美无缺能获得更高的奖励。
• 激励高质量: 产生完全正确的证明（R_Y高），并准确地认识到其严谨性（R_Z高），能够获得最高奖励。
• 激励主动修正: 这种机制引导生成器的最佳策略是在最终确定答案前，尽可能多地识别并解决自身证明中的潜在问题，从而实现主动的自我优化。

2.3. 第三阶段：验证与生成的协同进化与自动化

验证器与生成器之间由此形成了一个协同促进、螺旋上升的良性循环。随着生成器能力的增强，它产生的新证明对验证器的挑战也越来越大，这反过来为验证器的持续改进提供了宝贵的、高难度的训练数据。

最初，为了提升标注效率，我们采用了AI辅助的标注流程，即为每个待标注证明生成多个验证器分析报告，以帮助人类专家快速定位潜在问题。我们从这一过程中发现，审查验证器指出的问题（即元验证）比从零开始发现问题要容易得多。这一洞见促使我们设计了一套全自动化标注流程，以彻底突破人工标注的瓶颈。其核心步骤如下：

1. 生成多样化验证: 对每一个待标注的新证明，我们生成 n 份独立的验证分析报告。
2. 元验证筛选有效问题: 对于那些指出问题（评分为0或0.5）的分析报告，我们再进行 m 次独立的元验证评估，以确认其发现的问题是否真实有效。
3. 自动化打分决策: 如果在所有验证尝试中，有至少 k 个指出最低分数的分析报告被元验证确认为有效，则系统自动将该最低分赋予此证明。若所有验证尝试均未发现任何有效问题，则该证明被自动标注为满分（1分）。否则，该证明将被丢弃或交由人类专家进行最终裁定。

在我们最后两次的训练迭代中，这一全自动化流程完全取代了人工标注，且其标注质量与专家判断高度一致，成功构建了一个可持续进化的训练闭环。

在这一先进的技术架构和训练流程下，DeepSeekMath-V2取得了卓越的性能表现，为下一章节的实证分析铺平了道路。

3. 性能评估与实证分析

本节旨在通过一系列严格的基准测试和顶级数学竞赛评估，全方位展示DeepSeekMath-V2模型的实际能力。评估将从基础的单次生成能力、多轮自我迭代优化的效果，直至极限算力下的巅峰表现，系统性地验证自验证数学推理方法的有效性和先进性。

3.1. 单次生成（One-Shot）定理证明能力

此项评估旨在测试模型在不进行任何迭代修正的情况下，一次性生成正确证明的能力。我们使用了内部构建的、难度与中国高中数学联赛（CNML）相当的问题集进行测试。结果如下表所示，DeepSeekMath-V2在所有五个数学类别中均一致地超越了其他顶尖模型。

表1：在CNML难度级别问题集上的平均证明分数（数据源自原报告Figure 1）

3.2. 序贯自我优化（Sequential Self-Refinement）的有效性

对于国际数学奥林匹克（IMO）、中国数学奥林匹克（CMO）等级别的难题，单次生成往往难以一步到位。因此，评估模型通过多轮自我验证和修正来提升证明质量的能力至关重要。在该实验中，模型首先生成一个带自我分析的证明，然后根据自我分析中发现的问题进行迭代修正，直至它为自己打出满分或达到最大迭代次数。

根据原报告图2（Figure 2）的数据分析，我们观察到两个关键指标：Pass@1（每次独立优化线程最终得到的证明的平均分）和Best@32（在32次独立优化中，由模型自评选出的最佳证明的得分）。实验结果揭示了两个核心结论：

1. 自我评估的准确性: Best@32的分数显著高于Pass@1的平均分，这有力地证明了生成器能够准确地从众多候选方案中识别出高质量的证明。
2. 自我修正的有效性: Pass@1的分数随着最大迭代次数的增加而显著提升，这表明自验证机制能够有效指导模型系统性地、逐步地改进其推理过程。

3.3. 极限算力搜索（High-Compute Search）下的巅峰表现

为了解决最顶级的数学难题，我们采用了扩展验证和生成计算的策略。该方法维护一个包含64个候选证明的池子，在每次迭代中，根据验证器给出的平均分选出最优的64个证明，并结合那些指出问题的分析报告进行配对，生成新的候选证明。此过程最多进行16轮迭代，或直到某个证明通过全部64次独立验证。

在三大顶级数学竞赛中，DeepSeekMath-V2均取得了历史性的突破。特别是在面向大学生的普特南数学竞赛（Putnam 2024）中，其118/120的得分远超人类历史最高分90分。

表2：DeepSeekMath-V2在顶级数学竞赛中的成绩（数据源自原报告Table 1）。灰色问题表示完全解决，带下划线的问题表示获得部分分数。

根据Luong et al. (2025) 提供的基准数据，在与DeepMind的DeepThink (IMO Gold) 等模型的对比中，DeepSeekMath-V2在IMO-ProofBench基础集上表现更优，在高级集上也展现出强大的竞争力。一个重要的观察是：对于那些未能完全解决的难题，生成器通常能通过自验证准确识别出其自身证明中的真正问题，这再次有力地证明了大型语言模型验证器在评估复杂证明方面的可靠性。

DeepSeekMath-V2的卓越表现，是建立在对前人工作的继承与创新之上，这也引出了我们对相关工作与未来的思考。

4. 总结与展望

本白皮书详细阐述了DeepSeekMath-V2模型所采用的自验证数学推理方法。该方法通过训练模型识别并解决自身推理中的问题，成功地超越了传统基于最终答案奖励的范式局限，在多个顶级数学竞赛中取得了突破性成果。

4.1. 核心贡献回顾

本研究的核心技术贡献可总结为以下四点：

1. 高精度验证器: 我们成功训练了一个能够准确且忠实地评估数学证明的LLM验证器。
2. 元验证机制: 通过创新性地引入元验证，我们显著减少了验证器捏造问题的情况，确保了验证反馈的质量。
3. 自验证生成器: 我们激励证明生成器通过自我评估来最大化证明质量，从而实现了主动发现并修正错误的能力。
4. 自动化标注闭环: 我们利用规模化验证计算实现了对高难度证明的自动化标注，构建了可持续进化的训练闭环，最终摆脱了对昂贵人工标注的依赖。

4.2. 相关工作与定位

此前，以最终答案为导向的推理模型在AIME、HMMT等数值竞赛中取得了巨大成功，但它们在需要严谨过程的定理证明任务上存在天然的局限性。近期，包括Gemini-2.5 Pro和DeepMind的DeepThink在内的一些工作也开始探索证明验证，而DeepSeekMath-V2则是在推动自然语言自验证推理方向上的一次具体的、开源的实现。

同时，形式化证明助手（如Lean、Isabelle）和相关系统（如AlphaProof、Seed-Prover）通过严格的逻辑语言保证了证明的绝对可靠性。我们相信，自然语言定理证明的进步将对形式化推理产生巨大的推动作用。本工作的长远愿景正是结合非形式化推理的洞察力与形式化验证的可靠性。

4.3. 未来展望

DeepSeekMath-V2的成功证明了，让大型语言模型为复杂推理任务发展出有意义的自我评估能力，是一条完全可行的技术路线。尽管前方仍面临巨大挑战，例如处理更抽象的数学领域和提升推理的原创性，但我们已经迈出了坚实的一步。

我们希望本研究方向能够为最终创建出能够解决研究级别数学问题的、可自我验证的通用人工智能系统做出贡献。