DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
TL;DR 精炼摘要
论文提出DeepSeekMath-V2模型,解决了大型语言模型在数学推理中的有效性问题。通过强化学习训练的定理证明验证器,模型能够自我验证推理过程,生成更准确的证明。在IMO 2025等赛事中表现优异,表明自我可验证数学推理有助于更强大的数学AI发展。
摘要
Large language models have made significant progress in mathematical reasoning, which serves as an important testbed for AI and could impact scientific research if further advanced. By scaling reasoning with reinforcement learning that rewards correct final answers, LLMs have improved from poor performance to saturating quantitative reasoning competitions like AIME and HMMT in one year. However, this approach faces fundamental limitations. Pursuing higher final answer accuracy doesn’t address a key issue: correct answers don’t guarantee correct reasoning. Moreover, many mathematical tasks like theorem proving require rigorous step-by-step derivation rather than numerical answers, making final answer rewards inapplicable. To push the limits of deep reasoning, we believe it is necessary to verify the comprehensiveness and rigor of mathematical reasoning. Self-verification is particularly important for scaling test-time compute, especially for open problems without known solutions. Towards self-verifiable mathematical reasoning, we investigate how to train an accurate and faithful LLM-based verifier for theorem proving. We then train a proof generator using the verifier as the reward model, and incentivize the generator to identify and resolve as many issues as possible in their own proofs before finalizing them. To maintain the generation-verification gap as the generator becomes stronger, we propose to scale verification compute to automatically label new hard-to-verify proofs, creating training data to further improve the verifier. Our resulting model, DeepSeekMath-V2, demonstrates strong theorem-proving capabilities, achieving gold-level scores on IMO 2025 and CMO 2024 and a near-perfect 118/120 on Putnam 2024 with scaled test-time compute. While much work remains, these results suggest that self-verifiable mathematical reasoning is a feasible research direction that may help develop more capable mathematical AI systems.
思维导图
论文精读
中文精读
1. 论文基本信息
1.1. 标题
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning (DeepSeekMath-V2:迈向可自我验证的数学推理)
1.2. 作者
Zhihong Shao, Yuxiang Luo, Chengda Lu, Z.Z. Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, Xiaokang Zhang 所属机构: DeepSeek-AI (深度求索)
1.3. 发表期刊/会议
状态: 技术报告/预印本 (Technical Report / Preprint) 注: 论文内容提及 "IMO 2025" 和 "CMO 2024",结合当前时间 (2025年11月),这是一篇展示最新研究成果的前沿论文。
1.4. 发表年份
2025
1.5. 摘要
大型语言模型 (LLM) 在数学推理方面取得了显著进展,主要通过强化学习 (RL) 奖励正确的最终答案。虽然这种方法在 AIME 等注重数值答案的竞赛中表现出色,但它存在根本局限性:正确的答案不代表正确的推理,且许多高等数学任务(如定理证明)需要严谨的推导而非简单的数值。为了突破这一瓶颈,本文提出了一种可自我验证 (Self-Verifiable) 的数学推理框架。作者训练了一个基于 LLM 的验证器 (Verifier) 和一个以验证器为奖励模型的证明生成器 (Proof Generator)。该生成器被激励在最终定稿前识别并修正自身证明中的错误。通过扩展测试时计算 (Test-time Compute) 并利用自动化标注迭代提升验证器,DeepSeekMath-V2 在 IMO 2025 (国际数学奥林匹克) 和 CMO 2024 (中国数学奥林匹克) 中达到了金牌水平,并在 Putnam 2024 中获得了 118/120 的近满分成绩。
1.6. 原文链接
/files/papers/69284d609b40dbd7a3a8aeda/paper.pdf (已正式发布)
2. 整体概括
2.1. 研究背景与动机
- 核心问题: 目前的大型语言模型在解决数学问题时,主要依赖“结果导向”的强化学习,即只要最终答案 (Final Answer) 对了就给予奖励。然而,这种方法有两个致命缺陷:
- 逻辑不可靠: 模型可能通过错误的逻辑甚至运气“蒙”对答案,这在科学研究中是不可接受的。
- 任务不适用: 许多高等数学问题(如定理证明)本质上不需要计算数值,而是要求严谨的逻辑推导步骤。对于这类问题,传统的“最终答案奖励”机制完全失效。
- 当前挑战: 在没有标准答案 (Ground Truth) 的情况下,如何判断一个开放性数学证明的正确性?现有的模型往往缺乏自我审视能力,容易产生“幻觉”,即自信地写出错误的证明。
- 创新思路: 受人类数学家思维方式的启发——即人类可以在没有参考答案的情况下,通过逻辑检查来验证证明的有效性——论文提出让模型学会自我验证。如果一个证明经过反复的严格审查仍未发现漏洞,其可信度就会大大增加。
2.2. 核心贡献/主要发现
- 自然语言定理证明的自我验证: 提出了一套完整的训练流程,不仅训练模型解题,更训练模型像专家一样“批改”和“验证”证明。
- 元验证 (Meta-Verification) 机制: 引入了“元验证器”来监督“验证器”,防止验证器胡乱报错或产生幻觉,确保评价的公正性。
- 生成与验证的协同进化: 构建了一个良性循环:验证器指导生成器优化,更强的生成器产生更难的样本,这些样本经过自动标注后又反过来增强验证器。
- 卓越的竞赛成绩: DeepSeekMath-V2 在极高难度的数学竞赛(IMO, CMO, Putnam)中表现出超越人类顶尖选手的潜力,特别是在 Putnam 2024 中打破了人类最高分记录。
3. 预备知识与相关工作
3.1. 基础概念
为了深入理解本文,初学者需要掌握以下概念:
- 定理证明 (Theorem Proving): 与小学数学中的计算题不同,定理证明要求通过公理和逻辑规则,一步步推导出结论。在 AI 领域,这分为形式化证明(使用 Lean, Isabelle 等编程语言严格验证)和自然语言证明(使用英语/中文等人类语言推导)。本文专注于后者。
- 强化学习 (Reinforcement Learning, RL): 一种机器学习方法,通过让智能体 (Agent) 在环境中尝试动作并获得奖励 (Reward) 来优化策略。本文中,LLM 是智能体,写出证明是动作,验证器的评分是奖励。
- 测试时计算 (Test-time Compute): 指模型在推理阶段(即考试时)不仅仅是“脱口而出”答案,而是花费更多计算资源(时间)进行多次采样、自我反思、验证和修改,以提高准确率。
- 监督微调 (SFT): 在 RL 之前,先用高质量的人类标注数据对模型进行初步训练,使其学会基本的答题格式和逻辑。
3.2. 前人工作
- DeepSeekMath (V1) & DeepSeek-Prover: 作者团队之前的研究,主要集中在利用开源模型提升数学推理能力。
- AlphaProof (Google DeepMind): 这是一个结合了形式化证明系统的 AI,它在 IMO 2024 中表现优异。与本文的区别在于,AlphaProof 依赖将问题翻译成形式化语言 (Lean),而 DeepSeekMath-V2 直接在自然语言层面进行攻关,这更接近人类数学家的思考习惯,但也更难验证。
- 基于结果的 RL (Outcome-based RL): 如 OpenAI 的一些早期工作,主要关注最终答案的正确性。本文明确指出了这种方法的局限性。
3.3. 技术演进与差异化
本文处于从“结果验证”向“过程验证”转型的关键节点。
- 传统方法: 做题 对答案 错了惩罚,对了奖励。
- 本文方法: 做题 自己写出评审报告 外部验证器审查评审报告 修正证明。
- 核心差异: DeepSeekMath-V2 极其强调Meta-Verification (元验证),即“验证验证者的验证”,这是解决 LLM 在评估时产生幻觉的关键创新。
4. 方法论
本文的方法论围绕着构建一个能够“自我纠错”的数学系统展开,主要包含三个紧密耦合的组件:验证器训练、生成器训练以及二者的协同进化。
4.1. 证明验证 (Proof Verification)
系统的第一步是训练一个能像数学老师一样给证明打分的模型,称为验证器 。
4.1.1. 训练验证器识别问题
-
数据来源: 从 Art of Problem Solving (AoPS) 抓取了 17,503 个需要证明的数学竞赛题目。
-
数据构建: 使用一个基础模型生成证明,然后让数学专家根据一套量化标准(0分:有致命错误;0.5分:有小瑕疵;1分:完全正确)对这些证明进行打分。构建数据集 ,其中 是问题, 是证明, 是专家评分。
-
奖励函数: 验证器的训练目标是输出一段分析文本和一个预测分数。使用了两个奖励信号:
- 格式奖励 (): 强制模型遵循特定输出格式(如必须包含 "Here is my evaluation...")。
- 分数奖励 (): 衡量模型预测分数
s'_i与专家评分 的接近程度。公式如下: 符号解释:s'_i是验证器预测的分数, 是专家的真实标注分数 (Ground Truth)。差值的绝对值越小,奖励越高。
RL 目标函数: 符号解释: 该公式表示最大化期望奖励。模型 接收问题 和证明 ,生成评价
V'_i和分数s'_i,并根据格式和打分准确度获得奖励。
4.1.2. 引入元验证 (Meta-Verification)
仅仅训练模型预测分数有个漏洞:模型可能猜对了分数(例如给了0分),但理由完全是编造的(Hallucination)。为了解决这个问题,作者引入了元验证器 (Meta-Verifier) 。
- 任务: 元验证器不直接看数学题,而是看“验证器的分析报告”,判断这份报告是否合理。
- 流程: 专家对验证器的分析进行打分 (),训练元验证器。
- 增强验证器: 将元验证器的反馈加入到验证器的奖励函数中: 符号解释: 是元验证器给出的质量评分。这意味着验证器不仅要打分准,其分析逻辑还必须能通过元验证器的审查。
4.2. 证明生成 (Proof Generation)
有了可靠的验证器,下一步是训练证明生成器 来解决问题。
4.2.1. 基础训练
将验证器 作为一个奖励模型 (Reward Model)。生成器生成证明 ,验证器给出评分 ,以此指导生成器优化:
4.2.2. 通过自我验证增强推理 (Self-Verification)
这是本文最核心的机制。作者发现,如果在一次生成中同时要求模型“写证明”和“检查证明”,模型往往会盲目自信。因此,作者设计了一种特殊的训练方式:
- 要求: 模型必须先生成证明 ,紧接着生成一段自我分析 (Self-Analysis) 。
- 奖励设计: 这是一个精妙的复合奖励系统,旨在鼓励模型“诚实地发现自己的错误”。
其中,自我分析部分的奖励 定义为:
符号解释:
-
: 证明本身的质量分数(由外部验证器判定)。
-
: 生成器自己在自我分析 中给自己打的分数。
-
: 衡量模型“自知之明”的能力。如果你写得很烂 (),但你诚实地给自己打了低分 (),你也能获得高分奖励。
-
: 权重系数。
-
: 元验证器对自我分析文本 的质量评分。
直觉: 这种奖励机制告诉模型:“写出完美的证明最好;如果做不到,诚实地指出自己的错误也能得到不错的奖励;最差的是写错了还硬说自己是对的。”
-
4.3. 生成与验证的协同 (Synergy)
随着生成器变强,它会产生验证器从未见过的复杂证明。为了保持验证器的能力,作者提出了一种自动化标注 (Automated Labeling) 流程,无需人工介入即可扩大训练数据:
- 采样: 对一个新证明,用验证器生成 个不同的分析。
- 验证: 如果验证器指出了错误,用元验证器 (Meta-Verifier) 确认这个错误是否真实存在。
- 投票与标注: 如果多数分析都确认了错误,就将该证明标记为低分;如果所有分析都找不到问题,标记为满分。
- 闭环: 将这些自动标注的数据加入训练集,重新训练更强的验证器,进而训练更强的生成器。
5. 实验设置
5.1. 数据集
实验使用了多个高难度的数学竞赛数据集进行评估:
- In-House CNML-Level Problems: 91道类似于中国高中数学联赛 (CNML) 难度的内部题目,涵盖代数、几何、数论、组合等。
- IMO 2025 (6题): 国际数学奥林匹克,全球最高水平的高中生数学竞赛。
- CMO 2024 (6题): 中国数学奥林匹克。
- Putnam 2024 (12题): 北美顶尖的本科生数学竞赛。
- IMO-ProofBench: 包含 DeepMind 开发的基于 IMO 难度的测试集。
5.2. 评估指标
- Pass@1:
- 概念定义: 模型只生成一次回答,该回答被判定为正确的概率或平均得分。
- 数学公式: 通常定义为 ,但在本文图表中直接体现为平均证明得分。
- Proof Score (证明得分):
- 概念定义: 基于前文提到的
0, 0.5, 1三档评分标准,由验证器或专家给出的量化分数。
- 概念定义: 基于前文提到的
- Best@N (或 Pass@K):
- 概念定义: 给定一个问题,允许模型生成 个候选答案/证明,其中得分最高的一个作为最终成绩。这反映了模型在有足够算力进行搜索时的上限能力。
5.3. 对比基线
- GPT-5-Thinking-High (OpenAI): 代表 OpenAI 最先进的推理模型(注:截至当前时间点,可能是指 OpenAI o1 或后续系列的内部代号/高配版)。
- Gemini 2.5-Pro (Google DeepMind): Google 的前沿多模态推理模型。
- DeepThink (DeepMind): DeepMind 专门用于数学推理的内部模型,曾用于 AlphaProof 项目。
6. 实验结果与分析
6.1. 核心结果分析:One-Shot 生成能力
在不进行反复修改的情况下(One-Shot),DeepSeekMath-V2 展现了强大的基础能力。 下图(原文 Figure 1)展示了在 CNML 难度题目上的平均得分对比:
Figure 1 | Average proof scores on CNML-level problems by category and model, as evaluated by our verifier.
- 分析: DeepSeekMath-V2(蓝色柱状图)在代数 (Algebra)、几何 (Geometry)、数论 (Number Theory) 等所有子领域中,均显著优于 GPT-5-Thinking-High 和 Gemini 2.5-Pro。这证明了经过“自我验证”训练的模型,即使是一次成型的证明,其严谨性和正确率也更高。
6.2. 核心结果分析:自我修正带来的提升
通过引入序列修正 (Sequential Refinement),即让模型基于自我评估不断修改答案,证明质量得到了显著提升。 下图(原文 Figure 2)展示了随着修正轮数增加,证明质量的变化:
Figure 2 | Proof quality improvements as the maximum sequential iterations varies from 1 (no refinement) to 8 (initial generation plus up to 7 refinements based on self verification).
- 分析:
- Pass@1 (蓝线): 随着迭代次数(1到8次)的增加,平均分数稳步上升。说明模型的自我验证确实能发现并修复错误。
- Best@32 (橙线): 如果生成32条并让模型自己挑最好的,分数更高。这证明模型不仅能改,还能准确地从多个候选中识别出最好的那个(Self-Selection)。
6.3. 核心结果分析:高算力搜索 (High-Compute Search)
针对最难的竞赛题,作者使用了大规模的测试时计算(64个样本并行,16轮迭代)。结果令人震惊:
以下是原文 Table 1 的结果:
| Contest | Problems | Points |
|---|---|---|
| IMO 2025 | P1, P2, P3, P4, P5 | 83.3% |
| CMO 2024 | P1, P2, P4, P5, P6 | 73.8% |
| Putnam 2024 | A1~B4, B5, B6 | 98.3% |
- 分析:
- IMO 2025: 解决了 6 题中的 5 题,这通常是确定的金牌水平。
- Putnam 2024: 这是一个针对本科生的极难竞赛,DeepSeekMath-V2 获得了 118/120 分(几乎满分),而人类选手的最高分仅为 90 分。这是一个超越人类顶尖水平的标志性成果。
6.4. 与 DeepThink 的对比
在 IMO-ProofBench 基准上:
Figure 3 | Expert evaluation results on the Basic and Advanced subsets of IMO-ProofBench. All results are sourced from Luong et al. (2025), with the exception of DeepSeekMath-V2, which was evaluated by our experts following the grading guidelines.
- 分析: 无论是在基础集 (Basic) 还是高难集 (Advanced) 上,DeepSeekMath-V2 都大幅领先于 GPT-4o 等通用模型,并且在基础集上超越了 DeepMind 的 DeepThink (IMO Gold版本),在高难集上与之持平。
7. 总结与思考
7.1. 结论总结
DeepSeekMath-V2 成功验证了一个核心假设:大型语言模型可以通过“自我验证”来提升数学推理能力,而不仅仅依赖于最终答案的反馈。通过构建一个能够诚实评估自身逻辑的验证器,并建立“生成-验证-优化”的闭环,模型能够处理没有标准答案的复杂定理证明问题。其在 Putnam 2024 和 IMO 2025 上的突破性表现,标志着自然语言数学推理进入了一个新的阶段。
7.2. 局限性与未来工作
- 极高难度问题的挑战: 尽管成绩斐然,但在面对 IMO 中最困难的那类问题(通常是第3或第6题)时,模型仍显吃力。这表明在极深度的逻辑探索上,模型与人类顶级天才仍有差距。
- 非形式化证明的局限: 本文使用的是自然语言证明,虽然易读,但无法像 Lean 语言那样提供 100% 的机器绝对保证。验证器本身是概率模型,仍有极小概率误判。
- 计算成本: 高性能依赖于测试时的大规模计算(High-Compute),这意味着推理成本高昂,推理速度慢。
7.3. 个人启发与批判
- 启发: 这篇论文最让我受启发的是它的奖励函数设计 ()。它不仅仅奖励“做对”,更奖励“有自知之明”。这种让模型学会“诚实”的训练思路,对于解决 LLM 的幻觉问题具有极大的普适性价值,完全可以迁移到代码生成、法律文书撰写等需要严谨逻辑的领域。
- 思考: 自动标注 (Auto-labeling) 是一种强大的“自举”手段,但它是否存在“回声室效应” (Echo Chamber Effect)?即验证器和生成器由于共享某些基础偏见,在相互训练中不断强化这些错误偏见,导致系统在某些特定类型的错误上集体“失明”。未来的研究可能需要引入更多样化的外部信号来打破这种潜在的闭环风险。
相似论文推荐
基于向量语义检索推荐的相关论文。