Command Palette
Search for a command to run...
Zhihong Shao Yuxiang Luo Chengda Lu Z.Z. Ren Jiewen Hu Tian Ye Zhibin Gou Shirong Ma Xiaokang Zhang

摘要
大型语言模型在数学推理方面取得了显著进展,这不仅为人工智能提供了一个重要的测试平台,若进一步发展,还可能对科学研究产生深远影响。通过采用强化学习方法,以正确最终答案作为奖励信号来扩展推理能力,大型语言模型在一年内便实现了从表现不佳到在AIME和HMMT等定量推理竞赛中达到饱和水平的飞跃。然而,这一方法面临根本性局限:追求更高的最终答案准确率,并不能解决一个核心问题——正确的答案并不意味着推理过程正确。此外,许多数学任务(如定理证明)要求严格的逐步推导过程,而非仅给出数值答案,因此依赖最终答案奖励的机制在此类任务中并不适用。为了突破深度推理的瓶颈,我们认为有必要验证数学推理过程的全面性与严谨性。特别是在测试阶段可扩展计算资源的背景下,自我验证机制尤为重要,尤其适用于那些尚无已知解的开放性问题。为此,我们致力于研究如何训练一个准确且忠实的基于大型语言模型的验证器,用于定理证明任务。随后,我们利用该验证器作为奖励模型来训练一个证明生成器,并激励生成器在最终定稿前主动识别并修正自身证明中的各类问题。为确保随着生成器能力增强而维持生成与验证之间的差距,我们提出通过扩展验证计算资源,自动标注那些难以验证的新证明,从而构建训练数据以持续提升验证器的性能。由此产生的模型——DeepSeekMath-V2,在大规模测试计算资源的支持下,展现出强大的定理证明能力:在2025年国际数学奥林匹克(IMO 2025)和2024年中国数学奥林匹克(CMO 2024)中取得金牌级成绩,在2024年普特南数学竞赛(Putnam 2024)中获得接近满分的118/120分。尽管仍有许多工作有待完成,但这些结果表明,自我验证的数学推理是一个切实可行的研究方向,有望推动更强大数学人工智能系统的构建。