让AI自检数学证明过程,提升推理可靠性。
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
- 用自验证机制训练模型,确保每步推导都正确
- 在普特南、国际奥数等竞赛中取得接近满分成绩
- 适合需要严谨推理的数学证明与科研场景
大语言模型在数学推理方面取得显著进展,成为人工智能的重要测试基准。通过强化学习提升最终答案准确率,模型在一年内达到AIME和HMMT等竞赛的饱和水平。然而,该方法存在根本缺陷:正确答案不等于正确推理。许多数学任务如定理证明需要严格的逐步推导,无法仅靠最终答案奖励来优化。为突破深度推理瓶颈,我们提出自验证机制,训练一个基于LLM的可靠验证器用于定理证明。随后以该验证器作为奖励模型训练生成器,激励其主动发现并修正自身证明中的问题。为应对生成器变强后验证能力不足的问题,我们通过扩大验证计算资源自动标注难验证的证明,持续提升验证器性能。最终模型DeepSeekMath-V2在IMO 2025和CMO 2024中取得金牌级表现,在普特南2024竞赛中以118/120接近满分,展现强大定理证明能力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。