本文对 Anthropic LLM 研究员 Rishi Mehta 在个人博客上发布的 The 2025 International Mathematical Olympiad 进行摘要和原文翻译。作者在此之前在 Google DeepMind 从事强化学习研究。共同领导了 AlphaProof 项目，让一个 LLM 学会了足够的数学知识，在国际数学奥林匹克竞赛中获得银牌，几乎破解了 IMO 的终极挑战。还参与了 Gemini 的后续训练工作。

主要观点

• AI 攻克 IMO 难题: 在 2025 年的国际数学奥林匹克竞赛 (International Mathematical Olympiad, IMO) 中，人工智能首次达到了金牌水平，标志着一个重要的里程碑。OpenAI 和 Google DeepMind 的模型均在竞赛条件下解决了足够多的难题，获得了金牌级别的成绩。
• 通用大语言模型的胜利: 与去年依赖于形式化证明系统（如 Lean）的方法不同，今年的突破主要由通用的、使用自然语言进行推理的大语言模型 (LLM) 实现，这显示了 LLM 推理能力的巨大飞跃。
• AI 发展势头迅猛: 这一成就凸显了当前 AI 领域惊人的发展速度和巨大投入带来的强劲动力。作者认为，这预示着 AI 将在更多复杂领域取得突破，普通人也将在各自领域感受到其变革性影响。

关键细节

背景：IMO 大挑战 (IMO Grand Challenge)

• 里程碑意义: 自 2020 年提出以来，在 IMO 中获得金牌一直被视为衡量 AI 能力的重要标准。
• 作者的经历: 作者曾是 Google DeepMind AlphaProof 团队的成员，该系统在 2024 年的 IMO 中以 1 分之差与金牌失之交臂。
• 去年的局限: AlphaProof 当时存在一些问题：未达金牌分数线、部分解题耗时过长（近 3 天）、且题目需要人工翻译成形式化语言 Lean。

2025 年 IMO 各方成果

• 竞赛背景: 今年的 IMO 题目对参赛者而言相对容易，金牌分数线为 35/42，这为 AI 取得好成绩创造了有利条件。
• OpenAI:
  • 率先公布成果，其模型完全使用自然语言在 4.5 小时的规定时间内完成解题。
  • 其生成的证明过程非常简洁，甚至语法不完整，并夹杂着 “Good.” 或 “Perfect.” 等自我鼓励的词语。
  • 据称，团队规模很小，并采用了一种针对难以验证任务的强化学习 (RL) 方法。
• Google DeepMind:
  • 紧随其后宣布成果，同样使用自然语言并在 4.5 小时内完成。
  • 其证明过程更精炼，风格与人类书写的优秀证明几乎没有区别。
  • 该成果由一个大型团队完成，综合了强化学习、检索增强生成 (RAG) 等多种技术。其声明因经过 IMO 官方审查员的外部验证而被认为更具可信度。
• 形式化系统 (Formal Systems):
  • ByteDance 的 Seed-Prover 和初创公司 Harmonic 的系统也声称达到金牌水平，但它们依赖于 Lean 等形式化语言。
  • 这些系统耗时更长（长达数天），且生成的证明文本极其冗长（例如，一个问题的证明超过 4000 行）。

作者的观点与反思

• 自然语言方法的优越性: 作者认为，既然通用 LLM 能在短时间内用自然语言解决问题，那么耗费数天算力、依赖形式化语言的路线在解决 IMO 这类问题上已显得不那么有吸引力。
• 对 AI 研究的思考:
  1. 动力与能量: 当前 AI 领域汇聚了巨大的能量和动力，只要投入足够资源，几乎所有问题都能被攻克。
  2. 突破的非唯一性: OpenAI 和 Google DeepMind 使用不同技术达到了相同的结果，说明许多 AI 突破并非依赖于某个“唯一”的见解，而是多种路径都可能成功。
• 未来展望:
  • 作者预测，未来的前沿 LLM 可能无需专门训练就能在 IMO 中获得奖牌。
  • AI 有望在未来 6 个月内解决某个有意义的、未解的数学开放问题。
  • 作者以亲身经历感叹，LLM 在数学推理和代码生成等领域的能力进步速度惊人，这种变革性的影响很快会波及更多领域。

原文

2025年的IMO（国际数学奥林匹克竞赛）刚刚结束。今年有一批AI模型参与了挑战。以下是我对比赛结果的一些看法。

终极挑战

自2020年IMO终极挑战被提出以来，赢得IMO金牌一直被视为一个重要的人工智能里程碑，关于何时能实现这一目标，一直存在着大量的猜测和争议。我记得在2022年Neurips大会上与AI研究员们的一次大型晚宴中，这个话题被提了出来，当时大多数人认为我们离这个目标还差得很远，有好几个人认为2030年之前都不可能实现。当时（还处于保密状态的）AlphaProof团队的一名成员打赌说2024年就能实现，结果人们真的笑出声来。那时的前沿大语言模型还在为解决简单得多的数学谜题而挣扎，并且没有一条清晰的前进道路。

这曾是Eliezer Yudkowsky和Paul Christiano之间一个著名赌局的主题，其中较为乐观的预测是EY（Eliezer Yudkowsky）提出的“到2025年底有>16%的几率”。也有好几个预测市场在追踪这个问题，特别是Manifold上的这个。

IMO终极挑战在今年被攻克了。¹ Google DeepMind和OpenAI都宣布他们的模型取得了金牌水平的成绩。

我与这个问题的渊源

我在Google DeepMind花了近两年时间研究这个问题，最终我们在2024年IMO之后发布了AlphaProof。它与AlphaGeometry相结合，达到了银牌水平，以一分之差与金牌失之交臂。这给AI和数学界都带来了不小的震动。

当时这还不算完全攻克IMO终极挑战，有几个原因：

1. 该系统没有获得金牌。
2. 部分问题的解答耗时很长，最长的一道题花了近3天时间，远超给人类选手的4.5小时。
3. 题目首先由人类从英语翻译成Lean语言。

不过，感觉我们已经非常接近了。

关于（1），我们以1分之差错失金牌。比赛共有6道题，每题7分——该系统得了28分，而当年的金牌分数线是29分。这还是在题目主题分布对系统不利的情况下发生的。系统最弱的是组合数学，而AlphaProof没能解决的两道题（P3和P5）恰好都是组合数学题。从历史上看，出现两道组合数学题的年份不到一半。

关于（2），这一点可以通过更多工作来解决。关于（3），对于AlphaProof已解决的题目，系统其实也能成功地将它们自动形式化（尽管在竞赛环境中并未使用此功能）。

这促使AlphaProof团队从IMO转向更难的数学问题，也部分促使我转到Anthropic研究代理式编程（agentic coding）。因此，今年能作为旁观者，看着众多AI公司争相成为第一个摘得金牌的公司，对我来说是件很有趣的事——事不关己，但兴致盎然。

今年的赛果

如果要我预测AI模型在今年IMO的表现，我会相当看好至少有某个AI系统能拿到金牌。鉴于去年的结果，某个基于Lean的系统达成目标几乎是板上钉钉的事。

但考虑到各大实验室都对通用大语言模型的推理能力感兴趣，再次使用Lean会有点偏离主题。Google DeepMind和OpenAI在2024年都曾用通用大语言模型尝试过IMO，但当时的系统还不够强大。从那以后，进展速度堪称疯狂，但我当时也只会给通用大语言模型夺金大约50%的几率。

题目

今年的题目包括2道组合数学、2道数论、1道几何和1道函数不等式（尽管有几道题跨越了多个类别）。和去年一样，我发现Dedekind Cuts这个YouTube频道对于理解题目和解法非常有帮助。为了延续题目围绕举办地进行主题创作的传统，今年的题目中出现了许多澳大利亚元素，包括“inekoalaty”（“不等式”inequality与“考拉”koala的结合词）。

参赛选手们觉得今年的题目比去年容易，这次的金牌分数线是35/42分。许多学生都拿到了35分，所以今年颁发了72枚金牌（去年是58枚）。这实际上降低了金牌的门槛，再加上分数线正好与解题数量吻合（即解出5/6道题正好达线），使得今年成为AI尝试的好年份。

OpenAI

OpenAI在周五晚上率先公布了他们的成绩。他们完全使用自然语言，不借助工具，并在4.5小时内完成了作答。

证明过程在这里。这些证明相当奇特。首先，模型的语言极其简洁，尽可能使用缩写，不费心写完整的句子，甚至不顾语法正确性。它还周期性地插入“Good.”（很好）或“Perfect.”（完美）等自我鼓励的词语。

“完整了。很精确。搞定。”

— OpenAI的IMO模型，在完成P5之后

他们在这次访谈中谈及了他们的方法。他们说解锁了一种针对难以验证任务进行强化学习(RL)的方法。似乎是一个非常小的团队完成了这项工作。

Google DeepMind

Google DeepMind在周一紧随OpenAI的公告之后也发布了消息。同样是使用自然语言，并在4.5小时内完成。他们还请IMO官方审查了他们的证明，并证实了其金牌水平的表现。

证明过程在这里。这些证明看起来比OpenAI的要精炼得多，几乎与人类写得好的证明难以区分。

从致谢部分来看，这似乎是一个庞大的团队在做这件事，其中包括许多参与了2024年尝试的成员。看起来他们混合使用了多种技术，包括并行的测试时计算、强化学习(RL)、翻译过来的形式化证明、基于过往解法的RAG（检索增强生成），以及提示工程/框架搭建（prompting/scaffolding）。他们还发布了该系统的一个轻量版，该版本在非数学推理任务上也表现出色。

形式化系统

一些形式化系统也声称获得了金牌。

字节跳动发布了Seed-Prover，它解决了P1-P5，但耗时4天。其证明过程有些疯狂，例如P1的证明超过4000行。他们的技术同时依赖于形式化数据和自然语言数据，其测试时扩展（test-time scaling）使用了库学习（library learning）和测试时猜想生成（test-time conjecture generation）。

Harmonic，一家专注于Lean的初创公司，也声称获得了金牌。他们的证明可读性更强，但仍然极长，例如P1超过1400行。我想起去年AlphaProof的P6解法已经很长了，而那也只有300行。他们没有分享太多关于其流程的细节——听起来他们运行的时间可能比字节跳动更长，并且不清楚是用什么模型生成的答案，以及他们是否训练了自己的基础模型。

我对结果的看法

OpenAI和Google DeepMind的结果都极其令人印象深刻。特别是，如果OpenAI所说的“在不可验证任务上进行RL的这种技术具有足够的通用性，可以扩展到其他困难任务”的说法成立，那听起来非常有前景。从证明中可以清楚地看出，该模型经过了非常激进的RL训练。我猜测可能是一个经过训练的评分模型，利用参考解法进行某种形式的学习，再配合一些防止奖励“作弊”（reward hacking）的RL技巧，但我很可能猜错了。

关于基于Lean的证明器，从字节跳动发布的基准数据来看，其证明能力与去年的AlphaProof相似。但既然现在我们有了现成的基础模型，这些模型显然可以通过框架搭建，用纯英文引出金牌水平的解法，那么再用Lean花上几天计算来解决同样的问题，就显得很难自圆其说了。

关于AI研究的本质

IMO的故事凸显了当前AI研究的几个方面，我想深入谈谈。

能量与势头

现在AI背后有如此巨大的势头，感觉只要有足够多的人投入精力，我们几乎可以攻克任何问题。几乎没有什么东西是推不动的。

大多数研究突破并非独一无二

OpenAI和Google DeepMind使用相当不同的技术，得出了完全相同的结果。字节跳动使用与去年AlphaProof截然不同的方法，达到了相似的Lean证明能力。

这在当今许多AI进展中都是如此。有很多好的想法应该可行，但没有哪个实验室有资源去尝试所有这些想法。此外，哪些技术能奏效可能取决于路径——它们可能在特定实验室的设置/基础设施/人员配置下效果最好。而且，源于规模化的能力正在掀起一股浪潮，不断改变着可能奏效的方法的格局。

当然，有一些突破是“瓶颈”，即每个人都需要汇聚到同一个见解上才能取得进展（一个明显的例子是Transformers）。但许多其他的“突破”并非独一无二。

未来

我预计明年AI挑战IMO仍会吸引一些兴趣。前沿的大语言模型可能无需任何专门优化，开箱即用就能获得奖牌。

与数学家交流后，我感觉相对于当前的能力，攻克一些有一定难度（但不是特别令人兴奋）的开放性问题“并没有那么难”。我预计这在未来6个月内就会发生。

在AI for Math领域，Lean仍然扮演着重要角色。在某些方面，随着我们转向越来越难的问题，Lean的优势会变得更加明显，因为在那些问题上，评判证明的正确性变得极其困难。当前定理证明研究的范式是“Lean专用基础模型，加上大量的测试时计算”。当更大的基础模型在自然语言数学证明方面表现不佳时，这种范式很有道理。额外的计算资源最好用于通过一个更小的专用模型生成更多貌似可行的证明候选，因为Lean会告诉你何时找到了答案。我认为现在是时候改变这种模式，将两种能力构建到同一个模型中。

在过去3年里，我曾多次亲自评估大语言模型在IMO问题上的表现，它们取得的进步令我震惊。我记得在2023年中期，我曾手动检查Gemini和GPT-4对每一道近期IMO数值解答题的解法，发现只有一个问题它能拿到部分分数（其余都是零分）。仅仅两年后就以5/6的成绩获得金牌，这代表了疯狂的进步速度。如果你正埋头于改进模型目前不擅长的某个方面，很容易会忽略大局。

另一个让我真切“感受到AGI气息”的领域是代理式编程。当前这批模型与之前的任何模型相比，都处在完全不同的水平，我已能隐约看到明年乃至后年的发展路径。这种情况将会在许多其他领域发生，如果你的领域还没有感受到，那也只是时间问题。