梦晨 发自 凹非寺
量子位 | 公众号 QbitAI谷歌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垒富优配提示：文章来自网络，不代表本站观点。
