DeepSeek发布新模型DeepSeekMath-V2：迈向自我可验证的数学推理“大规模语言模型在数学推理方面取得了显著进展，这为人工智能提供了一个重要的测试平台，如果进一步发展，可能会对科学研究产生影响。通过使用强化学习来扩展推理，奖励正确的最终答案，LLM（大规模语言模型）在一年内从表现不佳提升到饱和定量推理竞赛，如AIME和HMMT。然而，这种方法面临着根本性的局限。追求更高的最终答案准确性并没有解决一个关键问题：正确的答案并不保证正确的推理。此外，许多数学任务，如定理证明，要求严格的逐步推导，而不是数值答案，这使得最终答案奖励无法适用。为了推动深度推理的极限，我们认为有必要验证数学推理的全面性和严谨性。自我验证对于扩展测试时计算尤其重要，特别是对于没有已知解的开放性问题。为了实现自我可验证的数学推理，我们研究了如何训练一个准确且忠实的基于LLM的定理证明验证器。接着，我们使用验证器作为奖励模型，训练一个证明生成器，并激励生成器在最终定理之前，尽可能识别和解决自身证明中的问题。为了保持生成与验证之间的差距，并随着生成器的增强，我们提出通过扩展验证计算来自动标注新的难以验证的证明，从而创建训练数据，进一步提升验证器。我们最终的模型DeepSeekMath-V2展现了强大的定理证明能力，在IMO 2025和CMO 2024上获得了金奖级别的成绩，并在Putnam 2024上以118/120的接近完美成绩，借助扩展的测试时计算。尽管仍有许多工作需要完成，这些结果表明，自我可验证的数学推理是一个可行的研究方向，可能有助于开发更强大的数学AI系统。”科技先锋官