DeepSeekMath-V2 — 自验证推理：用验证器指导定理证明

DeepSeekMath-V2

发布日期： 2025-11-27 来源： arXiv 2511.22570 工程范式： 自验证数学推理——用训练好的验证器作为奖励模型指导证明生成。

设计哲学

DeepSeekMath-V2 回答了一个根本问题：当最终答案不再是唯一标准（定理证明中正确答案不等于正确推理），RL 应该怎么继续提升？V1 靠 GRPO 用最终答案做奖励信号刷 AIME/HMMT 分数，但这对定理证明无效。V2 的核心转向是”验证推理过程本身”——训练一个准确且忠实的 LLM 验证器（verifier），用它作为证明生成器的奖励模型。关键设计是维护”生成-验证差距”：随着生成器变强，验证器也需要通过验证时计算扩展（scaling verification compute）来自动标注更难验证的证明，持续提升验证能力。这形成了一个自我强化的飞轮：更强的生成器暴露更难正确验证的证明 → 自动标注 → 更强验证器 → 更优奖励信号 → 更强生成器。

关键架构决策

• 基座： 从 DeepSeek 持续演进的数学推理模型
• 验证器即奖励模型： 训练 LLM 作为证明验证器，评估推理过程的完整性和严谨性
• 生成-验证飞轮： 扩展验证时计算，自动标注高难度证明，持续提升验证器质量
• 推理时扩展： 利用验证器在 test-time 进行搜索和自我修正

关键结果

DeepSeekMath-V2 在 IMO 2025 和 CMO 2024 上达到金牌级别分数。Putnam 2024 上以扩展 test-time compute 达成接近满分的 118/120。这些结果说明”自验证推理”路径在最高难度数学竞赛上验证有效。

范式对比

与 DeepSeekMath V1（答案驱动 RL）相比，V2 验证了”过程验证驱动 RL”在定理证明等高要求场景的优越性。与 DeepSeek-Prover 系列（用 Lean 验证器做外部反馈）不同，Math-V2 训练一个独立的 LLM 验证器，使其可泛化到没有形式验证器的场景。

可复用工程经验

1. 最终答案奖励在定理证明中存在天花板——过程验证是必要升级
2. 验证器-生成器对抗训练（保持差距）是持续提升的关键机制
3. 验证时计算扩展可以弥补验证器初始能力的不足
4. 自验证推理是通向真正数学推理智能的重要方向