AlphaProof 与 AlphaGeometry 2 解出 IMO 竞赛 4 题：首次达银牌水平

高中生奥数一直被当成机器推理的试金石。顶级人类选手在国际数学奥林匹克（IMO）赛场上苦练成千上万个小时，而大语言模型哪怕能写代码、做翻译，碰上这类需要长链条严密逻辑的考题，常常几步就露出马脚，开始一本正经地胡说八道。

Google DeepMind 拿出两套专打奥数的系统：AlphaProof 和升级版的 AlphaGeometry 2。它们联手解出了 2024 年 IMO 六道大题中的四道，最终拿到 28 分，刚好压在银牌上限，距离今年 29 分的金牌门槛只差一分。

让 AlphaZero 进军形式化数学

今年 IMO 的题目先被人工翻译成形式数学语言 Lean，再交由 AI 解题。判分过程找来了两位权威人物：菲尔兹奖得主 Timothy Gowers 教授，以及 2024 年 IMO 选题委员会主席 Joseph Myers 博士。两位评审完全按照赛规打分，给解出来的四道题都打了 7 分满分。

整个过程中最抢眼的是新系统 AlphaProof。它把大语言模型和强化学习算法 AlphaZero 绑在一起，专门在 Lean 环境里自我博弈、寻找严格证明。它负责搞定两道代数题和一道数论题，其中还包括本届比赛里最难的那道题，当时全场 609 名全球尖子生里，只有 5 个人做出了这道题。

另一边，专门攻克几何的 AlphaGeometry 2 表现也很亮眼。它基于 Gemini 训练，引入了比前代快 100 倍的符号引擎。在收到题目形式化表达后，它只花了 19 秒就解出了第 4 题。不过，剩下的两道组合数学题，两个系统都没能做出来。

解题时间也是个有趣的对比。真人选手分成两场，每场 4.5 小时；AI 解出一道题只要几分钟，但啃下其他难题最长花了整整三天。

解决幻觉的关键是 Lean

为什么以前的大模型解不好数学？自然语言训练的数据虽然海量，但模型容易在推理中间步骤编造逻辑，看似合理其实漏洞百出。

AlphaProof 的解法很聪明：它让预训练的 Gemini 模型把自然语言题目翻译成 Lean 代码，建起一个庞大的形式化题库。在 Lean 环境下，系统每走一步推导，编译器都能瞬间验证真伪，对就是对，错就是错，彻底杜绝了模型幻觉。

在比赛前几周，AlphaProof 靠着证明和证伪数以百万计的题目不断强化自己。甚至在比赛进行中，它还在围绕赛题自动生成变体自我训练，直到搜出完整的证明链条。

为什么重要

这是 AI 第一次在国际公认的顶级数学赛事中达到银牌水准。这证明强化学习加形式验证这条路，不仅能在围棋这类固定规则的棋类里通关，完全可以迁移到深奥的抽象数学领域。

对研究人员和数学家来说，这意味着未来的科研工具正在成型。你不需要担心 AI 给出的证明步骤是在胡言乱语，因为 Lean 会帮你把关。数学家可以用它来暴力验证繁琐的子命题，或者探索那些原本需要耗费数月甚至数年人工推导的猜想。

但也要看到它的局限。目前的系统依然高度依赖人工把人类语言“翻译”成形式化代码，没有人工这一步预处理，系统根本不知道题目在说什么。而且两道组合题剃了光头、部分题目耗时三天，说明机器在缺乏明确直觉引导和巨大搜索空间的离散数学问题上，依然会被算力消耗拖垮。但无论如何，人类在顶尖纯逻辑思维上的领地，又被机器切走了一大块。