日媒关注中国AI推理模型“Seed-Prover”：性能超越谷歌

中国科技公司字节跳动的研究人员发表了论文《Seed-Prover:Deep and Broad Reasoning for Automated Theorem Proving（Seed-Prover：自动化定理证明的广度和深度推理）》，内容有关相当于在国际数学奥林匹克竞赛（IMO）上获得金牌水平的AI推理模型“Seed-Prover”的研究报告。该论文近日引起了日本技术研究类媒体人山下裕毅的关注。

日媒关注中国AI推理模型“Seed-Prover”。（IT Media网站报道截图）

IT Media网站20日报道，在评价AI的数学水平时，通常使用国际数学奥林匹克竞赛作为标准。2月，谷歌DeepMind开发的AI系统“AlphaGeometry2”（AG2）在几何学问题中获得了相当于金牌的成绩。今年7月，OpenAI也宣布其模型获得了2025年国际数学奥林匹克竞赛中金牌级别的成绩。

此论文提到的自动化定理证明模型“Seed-Prover”，成功证明了2025年国际数学奥林匹克竞赛中6道题中的5道题，显示出与人类金牌得主相当的实力。不仅是2025年的竞赛，在过去的竞赛问题中，“Seed-Prover”也实现了78.1%的证明成功率。

“Seed-Prover”在基准测试中也表现出卓越的性能。它在“MiniF2F”中获得了验证集100%、测试集99.6%这样几乎完美的成绩。这大大超过了之前的最高纪录92.2%。在美国面向大学生的数学竞赛“PutnamBench”的题目中，“Seed-Prover”成功证明了657道问题中的331道（50.4%），比86道题的最高纪录提高了约4倍。

在几何学问题中，字节跳动使用“Seed-Prover”和几何推理专用引擎“Seed-Geometry”进行挑战。其性能超过谷歌的AI模型“AlphaGeometry2”，解决了国际数学奥林匹克竞赛的50道几何题中的43道。值得一提的是，“Seed-Prover”仅用2秒就证明了2025年国际数学奥林匹克竞赛的几何问题。

用C++重写的推理引擎比使用Python的速度快100倍，并且建立了超过2.3亿个几何问题的数据库。

山下表示，“Seed-Prover”的算法就像人类数学家一样，首先生成有用的中间引理，然后组合它们来证明主定理。技术方面，“Seed-Prover”利用名为Lean的编程语言，构建了能够自动验证证明正确性的机制。

编辑：万鲤