DeepSeekMath-V2: Pushing the Limits of Self-Verifiable Mathematical Reasoning
原标题 + 中文标题
DeepSeekMath-V2: Self-Verifiable Mathematical ReasoningDeepSeekMath-V2：推动可自验证数学推理的极限
一句话摘要
DeepSeekMath-V2 基于 DeepSeek-V3.2 构建，首创"验证器优先"训练流水线，通过证明生成器与验证器的双模型协作架构，在 2024 年 Putnam 竞赛中取得 118/120 的近乎满分成绩，在 IMO 2025 和 CMO 2024 中均达到金牌水平。
完整核心内容翻译
项目背景
2025 年 11 月 27 日，DeepSeek AI 团队正式发布 DeepSeekMath-V2——新一代数学推理模型。该模型聚焦于定理证明和自验证能力，旨在解决大语言模型在数学推理中"答案正确但推理过程不严谨"的根本性问题。
模型架构
DeepSeekMath-V2 基于 DeepSeek-V3.2-Exp-Base 构建，这意味着它继承了 DeepSeek 最新的 MoE 架构基础设施。模型采用多种数值精度格式（BF16、F8_E4M3、F32）以及稀疏注意力机制，以高效处理极长的证明推导过程。
核心创新：双模型协作的自验证系统
DeepSeekMath-V2 最大的创新在于构建了一套证明生成器与验证器协同工作的闭环系统：
- 证明生成器（Proof Generator）：负责生成初始数学证明
- 验证器（Verifier）：评估推理过程的逻辑严谨性和完整性
工作流程为迭代式运行：生成器产出证明 → 验证器识别逻辑缺陷 → 生成器进行修正 → 循环往复直至验证通过。
三阶段训练流水线
第一阶段：验证器训练 使用正确/错误证明对，训练验证器精确识别推理过程中的微妙逻辑错误。这一阶段的目标是让验证器具备"数学审稿人"级别的鉴别能力。
第二阶段：生成器强化学习 将训练好的验证器作为奖励信号源，通过 GRPO（Group Relative Policy Optimization）算法对生成器进行强化学习训练。验证器不仅评判最终答案的正确性，更关注推理过程的每一步是否严谨——这激励生成器学会自我纠正。
第三阶段：验证器持续提升 通过扩展验证计算量来自动标注困难样本，并引入**元验证器（Meta-Verifier）**来维持验证器与生成器之间的能力差距，确保验证器始终领先于生成器。
竞赛级表现
| 竞赛/基准 | 成绩 | 等级 |
|---|---|---|
| IMO 2025（国际数学奥林匹克） | 金牌水平 | 顶尖 |
| CMO 2024（中国数学奥林匹克） | 金牌水平 | 顶尖 |
| Putnam 2024（北美大学生数学竞赛） | 118/120 | 近乎满分 |
| IMO-ProofBench | 超越 Gemini DeepThink | 领先 |
开源与可获取性
- 许可协议：Apache 2.0
- 发布渠道：HuggingFace 和 GitHub
- 支持场景：定理证明、形式化验证、竞赛数学
技术要点
"验证器优先"训练范式：颠覆传统"先训练生成器再附加验证"的顺序，首先训练强大的验证器，再以其为锚点引导生成器的能力提升。这确保了模型不仅"会做题"，更"知道为什么对"。
GRPO 强化学习与过程奖励：不同于仅基于最终答案正确性的稀疏奖励，GRPO 算法结合验证器实现了对推理过程的密集奖励信号，让模型学会在每一步推理中追求逻辑严谨性。
元验证器机制：为防止生成器能力增长后"欺骗"验证器，引入元验证器层来持续校准和提升验证器能力，保持系统的动态平衡。
Putnam 118/120 的突破性意义：Putnam 竞赛是北美最负盛名的大学生数学竞赛，中位分通常仅为 0-2 分。118/120 的成绩意味着模型在复杂分析、代数和组合数学中的推理能力已接近人类顶尖水平。
形式化证明的实用化：模型不仅能给出答案，还能生成可机器验证的完整证明过程，这为数学研究辅助工具的实用化铺平了道路。
深度解读
DeepSeekMath-V2 的核心贡献不在于"解题更快更准"，而在于提出了一种全新的范式来解决 AI 数学推理中最棘手的问题：推理过程的可靠性。
在此之前，大多数数学模型的评估标准是"最终答案是否正确"。但在实际数学研究中，一个碰巧得出正确答案但中间推理存在逻辑跳跃的证明是没有价值的。DeepSeekMath-V2 通过"验证器优先"的设计哲学，从根本上将评价标准从"结果正确"提升到了"过程严谨"。
三阶段训练流水线的精妙之处在于其自举特性：验证器的能力提升推动生成器改进，生成器产出更高质量的证明又反过来为验证器提供更有挑战性的训练材料。这种"军备竞赛"式的共同进化，使得系统的整体能力远超单一模型所能达到的上限。
元验证器的引入则体现了对 RL 训练中"奖励攻击"问题的深刻理解——当策略模型变得足够强大时，它可能学会生成"看起来正确"但实际有缺陷的证明来骗过验证器。元验证器作为"验证者的验证者"，有效遏制了这一问题。
延伸思考
从竞赛数学到数学研究：118/120 的 Putnam 成绩令人印象深刻，但竞赛数学与前沿数学研究之间存在质的差距。模型能否从"解决已知有解的问题"跨越到"探索未知领域"，将是下一个关键里程碑。
自验证范式的迁移性：这种"生成器-验证器"协作架构是否可以迁移到代码生成（生成代码 + 自动测试验证）、科学推理（提出假设 + 实验验证）等更广泛的领域？
形式化验证的民主化：如果 AI 能够稳定地生成可机器验证的证明，这可能根本性地改变数学教育和研究的方式——每个数学结论都可以附带一份机器验证过的完整证明。
原文链接
- GitHub 仓库：https://github.com/deepseek-ai/DeepSeek-Math
- MarkTechPost 报道：https://www.marktechpost.com/2025/11/28/deepseek-ai-releases-deepseekmath-v2-the-open-weights-maths-model-that-scored-118-120-on-putnam-2024/
- 技术分析：https://dev.to/czmilo/2025-major-release-how-does-deepseekmath-v2-achieve-self-verifying-mathematical-reasoning-3pje