谷歌 DeepMind 的 IMO 金牌模型，完整技术全公开了！

延续 DeepMind 的命名传统，这次叫：AlphaProof。

依然是 Nature 刊发的形式，放出了 AlphaProof 的完整论文，首次详细公开了其背后的技术架构和训练方法。值得一提的是，无师自通的下棋 AlphaZero，也在这次论文里被多次提及。

作者 Tom Zahavy 也趁此机会分享了一些开发过程中的细节：

AlphaProof 团队规模并不大。大部分时间里只有大约 10 个人，临近 IMO 比赛时才有更多人加入。

真正带来突破的核心团队成员是 IMO 金牌得主 Mikl ó s Horv á th。

他想出一个方法可以创建 AI 正在处理的问题的各种变体，并将它们作为初始状态，让智能体在这些变体上进行训练。

在整整一年里，这只团队还探索了各种研究思路，虽然很多都失败了，但成功的那些都被整合到了 AlphaProof 系统里，现在全面公开。

把数学证明当游戏来玩

AlphaProof 的核心思路其实很直接：把数学证明过程变成一个可以反复训练的游戏。

系统基于 Lean 定理证明器构建了一个强化学习环境。在这个环境中，每个数学命题就是一个新的游戏关卡，AI 需要通过选择合适的策略（tactics）来推进证明。

如果某个策略成功了，就会得到新的子目标；如果所有目标都完成了，就意味着证明完成。

论文揭示，AlphaProof 使用了一个 30 亿参数的编码器 - 解码器 transformer 模型作为 " 大脑 "。

这个证明网络不仅要理解当前的证明状态，还要同时输出两个关键信息：

一是建议接下来尝试哪些策略，二是估计完成证明还需要多少步。

这种设计让系统能够更智能地分配计算资源，优先探索最有希望的证明路径。

搜索算法方面，AlphaProof 采用了受 AlphaZero 启发的树搜索，但做了关键改进。

比如引入了 AND-OR 树结构来处理证明中的多个独立子目标，当一个证明需要同时满足多个条件时，系统会把它们分解成独立的子问题分别攻克。另外还加入了渐进采样机制，让系统在关键路径上能够探索更多样的证明策略。

训练 AlphaProof 面临的最大挑战是：哪来那么多数学题？

他们首先用约 3000 亿个 token 的代码和数学文本对模型进行预训练，让它理解基本的逻辑结构和数学语言。接着用 Mathlib 库中约 30 万个人工编写的证明进行微调，让模型学会 Lean 的语法和证明技巧。

真正的突破来自于自动形式化过程。团队基于 Gemini 1.5 Pro 开发了一个专门的翻译系统，能够把自然语言的数学问题转换成 Lean 可以理解的形式语言。通过反复迭代和改进，这个系统最终从约 100 万道自然语言数学题生成了约8000 万道形式化问题，远超所有现有数据集。

主强化学习循环是整个训练的核心。系统会不断尝试证明或反证这些自动生成的命题，成功的证明会被用来更新神经网络。

即使自动形式化的结果不完全准确，只要它是一个有效的形式命题，AlphaProof 都能从尝试证明它的过程中学到东西。

整个主训练阶段消耗了约 8 万 TPU 天的计算资源。

论文中的核心架构图展示了 AlphaProof 的两个学习循环是如何协同工作的。

在主强化学习循环中，约 100 万道非正式数学问题首先经过形式化系统的处理，被翻译成大约 8000 万道 Lean 能够理解的形式化问题。证明网络配合树搜索算法在 Lean 环境中不断尝试，无论是成功找到证明、找到反证，还是超时失败，每一次尝试都会产生经验数据反馈给学习系统。

测试时强化学习循环则展现了一种更加精细的适应机制。

当面对一道特别困难的目标问题时，变体生成器会围绕这道题产生大约 40 万个相关变体，相当于为一道题专门创建了一个小型数据集。

这些变体包含了各种数学直觉：简化特殊情况、推广到更一般的形式、探索类似的结构等。

系统会启动一个独立的 AlphaZero 式学习过程，专门在这些变体上训练，逐步积累解决原问题所需的洞察。这个机制可以并行处理多个目标问题，每个问题都有自己的变体课程和专属的学习进程。

IMO 赛场上临时突破

AlphaProof 在 2024 年 IMO 上的表现堪称惊艳，现在背后更多开发细节被公开。

面对 IMO 级别的难题，仅靠增加搜索时间往往不够。这时候，前面介绍的测试时强化学习（TTRL）就派上了用场，也就是生成大量相关的变体问题（比如简化版、推广版、类比版等），然后专门训练一个 " 专家 " 模型来攻克这道题。

以 2024 年 IMO 的第一题为例，这道题要求找出所有满足特定整除性质的实数 α。AlphaProof 生成的变体包括：只考虑有理数的情况、假设 α 满足更强的性质、证明 α 必须接近某个整数等等。通过在这些变体上训练，系统逐渐掌握了解决原问题的关键。

在实际比赛中，AlphaProof 成功解决了代数和数论的三道题（P1、P2、P6），其中 P6 是整个比赛最难的题目，609 名参赛选手中只有 5 人完全解出。

每道题的 TTRL 过程需要 2-3 天的计算时间，虽然远超人类选手的 9 小时限制，但考虑到此前最先进的 AI 系统连最简单的 IMO 题都很难解决，这个成就已经相当了不起。

Tom Zahavy 在回忆中提到，比赛期间他们通过部分证明系统就已经确定的成绩只能拿到铜牌水平，但 TTRL 还在后台运行。

三天后，当三个完整证明陆续出现时，才终于确定能拿到金牌，团队兴奋地敲锣打鼓庆祝。

数学 AI 的下一步在哪里

AlphaProof 夺金后，谷歌 DeepMind 已经向科学界开放 AlphaProof 的能力，研究人员可以通过申请获得使用权限，多位数学家在 Nature 上分享了他们试用 AlphaProof 的体验。

罗格斯大学的数学家 Alex Kontorovich 发现，AlphaProof 特别擅长找出反例：

每次它指出我的陈述有问题时，我都能很快找出遗漏了什么假设，调整陈述后再次尝试。这种来回迭代对于得到正确的形式化陈述至关重要。

伊利诺伊大学的 Talia Ringer 教授让她的两个博士生各提供了一个他们觉得棘手的引理。AlphaProof 在一分钟内证明了其中一个，而另一个则被反证了，原来是定义中有个漏洞。

她评价 "AlphaProof 倾向于找反证的特性可能是它最令人惊讶的有用功能 "。

当然，数学家们也测试出了 AlphaProof 也有局限性。

伦敦帝国理工学院的 Kevin Buzzard 在尝试用它翻译费马大定理的证明时遇到了困难。他发现当证明中充满了 " 定制化的定义 " 时，AlphaProof 就不太管用了。

这也印证了 AlphaProof 团队在论文中的发现：系统在处理 Mathlib 中已有概念时表现出色，但面对全新定义时就会遇到瓶颈。

Tom Zahavy 也分享了自己对于 AI 在数学界应用的思考：

AlphaProof 面临的一大挑战在于它对 Lean 定理证明器的依赖。Lean 虽然功能强大且拥有活跃的社区，但其持续演进为 AlphaProof 创造了一个不稳定的环境。这意味着在 Lean 的高级策略更为成熟的数学子领域，AlphaProof 的性能往往更佳。

另一个关键问题是 " 数据有限性 "。独特的数学题和数量是有限的。为了使强化学习智能体真正具备通用性，它需要能够生成自己的问题。虽然目前在创建 IMO 级别的问题变体方面取得了一些成功，但这个方向还需要进一步拓展。

Hinton 在今年 6 月份的访谈中指出，AI 未来在数学方面很可能会比人类强得多：由于它能够在封闭的数学系统中即时共享知识并生成自己的训练数据。

AlphaProof 的方法，正是这一预言的预演。

论文地址：

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

参考链接：

[ 1 ] https://www.tomzahavy.com/post/how-we-achieved-an-imo-medal-one-year-before-everyone-else

[ 2 ] https://www.nature.com/articles/d41586-025-03585-5

一键三连「点赞」「转发」「小心心」

欢迎在评论区留下你的想法！

—  完  —

  年度科技风向标「2025 人工智能年度榜单」申报即将于 11 月 17 日截止！点击了解详情

❤️‍   企业、产品、人物 3 大维度，共设立了 5 类奖项，最后时刻一起冲刺 

一键关注 点亮星标

科技前沿进展每日见