
总部位于中国的人工智能实验室DeepSeek发布了一款新的开放权模型DeepSeekMath-V2。
据人工智能实验室介绍,该模型在数学中展现出强大的定理证明能力,并在2025年国际数学奥林匹克竞赛(IMO)中获得了金级成绩。
它解决了2025年国际海军组织(IMO 2025)6个问题中的5个。
“想象一下,免费拥有世界上最顶尖数学家之一的大脑,”Hugging Face联合创始人兼首席执行官克莱门特·德朗格在X上的一篇帖子中说。
“据我所知,目前没有任何聊天机器人或API能让你访问IMO 2025金牌得主模型,”他补充道。
今年7月,谷歌DeepMind的Gemini模型的高级版本和OpenAI的实验推理模型也获得了IMO 2025金奖。与DeepSeek的新模型类似,OpenAI和谷歌的模型也解决了6个问题中的5个。这些是首批获得金级分数的AI模型。
IMO常被认为是全球最难的高中数学竞赛。在2025年IMO的630名学生中,有72人获得金牌。
除了IMO 2025竞赛外,DeepSeekMath-V2还在中国最艰难的全国竞赛——中国数学奥林匹克竞赛(CMO)中取得了顶尖成绩,并在本科普特南考试中取得了接近满分的成绩。
DeepSeek表示:“在Putnam 2024这项顶级本科数学竞赛中,我们的模型完全解决了12个问题中的11个,其余问题中存在轻微错误,得分为118/120,超越了人类最高分90分,”DeepSeek表示。
DeepSeek认为,近期的AI模型在数学基准测试如AIME和HMMT中表现优异,但往往缺乏合理的推理。
“许多数学任务,如定理证明,需要严格的逐步推导,而非数值答案,因此最终答案奖励不适用。”
为此,DeepSeek强调需要能够判断和完善自身推理的模型。团队认为,“自我验证对于扩展测试时间计算尤其重要,尤其是对于没有已知解的未解决问题。”
作为背景介绍,测试时计算指的是在推理过程中分配大量计算——而非训练阶段——以便模型推理更长时间,探索多种解并完善其答案。
DeepSeek 的方法训练一个专门的验证器,评分证明质量而非答案,然后用该验证器指导独立的证明生成模型。生成器只有在修正自己的错误时才会得到奖励,而不是隐藏错误。
正如论文所解释的,他们“用验证器作为奖励模型训练证明生成器,并激励生成器在最终确定证明前尽可能多地识别和解决自己的证明问题。”
为了防止系统对自身检查器过拟合,DeepSeek不断提高验证过程的难度。
它通过增加计算量并自动标记难度证明来实现这一点,确保验证器与生成器同步演进。
用他们的话说,这使他们“能够”扩展验证计算,自动标记新的难以验证的证明,创建训练数据以进一步改进验证器“。
该模型的重量可以在Hugging Face上下载。“这就是人工智能和知识的民主化,字面意义上的体现,”德朗格说。
DeepSeek在发布了一个低成本、开源的模型后崭露头角,该模型可与美国AI系统抗衡。其DeepSeek-R1推理的发布引发了人们对开放模型是否会侵蚀封闭产品商业优势的质疑,短暂动摇了投资者对英伟达等AI巨头的信心。
