拿下奥数银牌的Google AlphaProof，首次公开技术细节

去年 7 月，Google DeepMind 宣布其 AI 系统在国际数学奥林匹克竞赛（International Mathematical Olympiad, IMO）中取得银牌成绩，这是 AI 首次在这项赛事中达到奖牌水平。当时团队承诺会公布技术细节，如今，这一承诺得以兑现：11 月 12 日，完整论文发表在《自然》（Nature）杂志上，AlphaProof 系统的技术细节得以全面公开。

图丨相关论文（来源：Nature）

作为汇集了全球最擅长数学的一批青少年的比赛，IMO 的试卷涵盖六道极具挑战性的题目，覆盖代数、组合数学、数论和几何等领域。这些题目的难度往往让人望而生畏，在 2024 年的比赛中，满分 42 分的试卷上，只有不到百分之一的参赛者能够获得满分。许多数学界的菲尔兹奖得主都曾是 IMO 的参赛者，这足以说明这项赛事在数学界的分量。而近年来，IMO 也逐渐成为衡量人工智能系统高级数学推理能力的标杆性挑战。

在 2024 年的 IMO 中，AlphaProof 与专门处理几何问题的 AlphaGeometry 2 系统联手，完成了六道题目中的四道，获得 28 分。这个成绩相当于当年 609 名参赛者中排名前列的银牌获得者的水平。此外，AlphaProof 还成功解决了被认为是当年最难的第六题，这道题目只有五名人类参赛者完全解答出来。这是人工智能系统首次在 IMO 中达到奖牌级别的表现，标志着机器数学推理能力的一个重要里程碑。

（来源：Google）

AlphaProof 的核心优势在于它将形式化数学语言与强化学习深度结合。传统的大语言模型虽然能够生成看似合理的数学推理步骤，但它们存在一个致命弱点——会产生“幻觉”，即生成错误但看起来可信的内容。而数学证明需要的是绝对的严谨性，容不得半点瑕疵。为了解决这个问题，研究团队选择了 Lean 这种形式化语言作为系统的工作环境。

Lean 是一种交互式定理证明助手，它能够自动验证数学证明的正确性。在 Lean 中，每一步推理都必须符合严格的逻辑规则，任何错误都会立即被系统检测出来。这种特性使得 AI 生成的证明可以被自动验证，不需要人工检查，也不会出现幻觉问题。问题在于，Lean 这样的形式化系统虽然严谨，却面临着训练数据稀缺的困境，Lean 的标准数学库 mathlib 只包含约二十万个定理，远远无法满足大规模机器学习的需求。

图丨AlphaProof 核心推理组件（来源：Nature）

研究团队想出了一个办法。他们首先对 Gemini 语言模型进行微调，使其能够将自然语言的数学问题自动转化为 Lean 能够理解的形式化语言。这个过程被称为“自动形式化”。通过这种方法，他们从一百万个自然语言数学命题中生成了八千万个不同的 Lean 形式化语句。这个庞大的合成数据集为后续的强化学习训练提供了充足的素材。

AlphaProof 的架构借鉴了 AlphaZero 的设计思路。系统的核心是一个拥有三十亿参数的编码器-解码器变换器网络，它能够理解 Lean 中的证明状态，并生成两种输出：一个策略网络，用于建议下一步应该采取的证明策略；一个价值函数，用于评估当前证明路径的前景。这两个输出共同指导一个专门设计的树搜索算法，在浩瀚的可能证明空间中寻找正确的路径。

图丨AlphaProof 的学习与适应过程（来源：Nature）

在树搜索的设计上，研究团队引入了一个名为“乘积节点”（product node）的概念。在 Lean 中，证明一个定理往往需要将目标分解为多个独立的子目标——比如使用数学归纳法时，需要分别证明基础情况和递推步骤。“乘积节点”要求其所有子节点都必须被证明，这让搜索算法能够有效追踪哪些子目标已经完成，并将计算资源集中在最困难的分支上。这种设计大大提高了搜索的效率。

但 AlphaProof 最具创新性的技术，或许是它的“测试时强化学习”（Test-Time RL, TTRL）。对于特别重要或困难的问题，系统会在推理时投入大量计算资源进行深度学习。具体来说，它会利用语言模型生成目标定理的众多变体。这些变体难度各异，形成了一个自然的学习课程。通过解决这些较容易的变体，系统能够逐步积累经验和洞察，最终攻克原始的复杂问题。这种方法在解决 2024 年 IMO 第六题时发挥了关键作用。

在训练过程中，AlphaProof 会仔细追踪每个形式化问题的进展，一旦证明某个形式化语句是错误的，就不再浪费资源尝试证明它；而当找到一个成功的证明后，系统还会再次尝试，看能否发现更短、更优雅的证明。训练初期，系统从小规模搜索开始，避免在过难的问题上浪费计算；随着训练深入，逐步增加搜索的规模和深度。这种渐进式的训练策略让系统既能快速找到简单证明，又不会被困在难题上无谓消耗资源。

在实战中，AlphaProof 呈现出与人类选手非常不同的特点。在官方比赛中，学生们有两个 4.5 小时的答题时段。而 AlphaProof 解决某些问题只需几分钟，但处理其他问题却可能需要长达三天时间。这种时间差异引起了一些讨论。对此，研究团队表示，重点不在于比拼速度，而在于验证 AI 是否能达到奥赛水平的推理能力。随着技术进步，这个时间差距会逐渐缩小。

菲尔兹奖得主、IMO 金牌得主 Timothy Gowers 教授在评估 AlphaProof 的解答后说：“作为数学家，我认为这很令人印象深刻，是一个显著的进步。”剑桥大学 AI 与数学专家 Katie Collins 认为，自动化形式化过程的突破对数学界很有意义：“如果研究成果能够用这种证明系统来表述，我们对发表结果的正确性会更有信心，也能促进更多合作。”

值得一提的是，就在今年的 IMO 竞赛中，DeepMind 推出了全新的系统 Gemini Deep Think，实现了端到端的自然语言推理，在 4.5 小时的限制时间内获得了 35 分的金牌成绩。这个系统不再需要形式化语言的中介，直接用自然语言理解问题并生成可读的证明。这表明，从银牌到金牌，从形式化语言到自然语言，AI 数学推理能力正在快速演进。AlphaProof 开创的形式化验证路径和新系统的自然语言能力，或许会在未来某个时刻汇聚融合，带来更加强大和通用的数学 AI 工具。

论文作者之一 Julian Schrittwieser 在博客中提到了一些细节。他特别提到 Test-Time RL 的可扩展性，直言：“限制我们的只是能用上多少 TPU 算力。”这种在推理时投入大量计算资源来获得更好结果的方式，可能为 AI 系统开辟新的优化方向。更重要的是，AlphaProof 表明强化学习与搜索的组合对大语言模型同样有效，这为构建更通用、可验证的 AI 系统提供了思路。

不过，目前所有 IMO 题目都需要人工翻译成形式语言才能让 AlphaProof 理解。虽然团队也试验了基于 Gemini 的自然语言推理系统，但要实现真正自主的数学 AI，还需要解决从自然语言到形式语言的自动转换问题。另外，AlphaProof 在代数和数论上表现不错，但在组合数学上相对较弱，团队正在研究原因。

参考资料：

1.https://www.nature.com/articles/s41586-025-09833-y

2.https://www.julian.ac/blog/2025/11/13/alphaproof-paper/

3.https://www.nature.com/articles/d41586-025-03585-5

运营/排版：何晨龙