AlphaProof 解出全场仅五人做出的 IMO 难题，AI 数学推理跨过银牌线

核心洞察

这篇东西最让我意外的不是AI做对了题，而是它做对了一道全场只有五个人做出来的题。要知道IMO国际数学奥林匹克竞赛，自1959年起每年举办，是面向年轻数学家的最古老、最大、最负盛名的竞赛。的题目不是靠刷题库能解决的，每道题都是原创的。另外值得注意的一点是，AlphaProof谷歌DeepMind开发的基于强化学习的系统，用于在形式化语言Lean中证明数学命题。的解法在形式化语言Lean一种形式化数学语言，用于编写和验证数学证明。中被逐步验证，这意味着它的推理过程没有跳步，每一步都经得起检查。这跟大语言模型那种“看起来很有道理但中间可能胡说”的路子完全不同。

---

2024年7月25日，科学

AlphaProof与AlphaGeometry团队

突破性模型AlphaProof和AlphaGeometry 2谷歌DeepMind开发的改进版几何求解系统，基于神经符号混合方法。解决了数学中的高级推理问题

注：本文最初发布于2024年7月25日。2025年11月12日，我们在《自然》杂志上发表了一篇论文，介绍了AlphaProof背后的方法论。

具备高级数学推理能力的通用人工智能，有望在科学和技术领域打开新的局面。

我们在构建帮助数学家发现新见解、新算法以及开放问题答案的AI系统方面已经取得了很大进展。但目前的AI系统在解决通用数学问题时仍然吃力，瓶颈在于推理能力和训练数据两个方面。

今天我们介绍AlphaProof，一个基于强化学习的形式化数学推理系统，以及AlphaGeometry 2，我们几何解题系统的改进版。这两个系统联手解决了今年国际数学奥林匹克竞赛六道题中的四道，首次达到了银牌选手的水平。

核心结论

1. AlphaProof与AlphaGeometry 2联手解决了2024年IMO六道题中的四道，总分42分中拿到28分，达到银牌最高档水平（当年金牌线为29分）。

2. AlphaProof解决了一道全场仅五名选手做出的IMO最难题，且其解法在形式化语言Lean中被逐步验证，推理过程无跳步。

3. AlphaProof将预训练语言模型与AlphaZero强化学习算法结合，在Lean中训练，备战期间证明或推翻了数百万道数学题。

4. AlphaGeometry 2在收到形式化题目后19秒内解决了IMO第四题，其符号引擎比前代快两个数量级，赛前已能解决过去25年IMO几何题的83%（前代为53%）。

5. 2025年11月12日，AlphaProof背后的方法论已在《自然》杂志上发表论文。

AI在复杂数学问题上的突破性表现

IMO是面向年轻数学家的最古老、规模最大、最具声望的竞赛，自1959年起每年举办。

每年，顶尖的大学预科数学选手要花上有时数千小时训练，来攻克代数、组合、几何和数论四个领域的六道超难题目。菲尔兹奖是数学界的最高荣誉之一，许多获奖者当年都曾代表自己的国家参加IMO。

近年来，IMO竞赛也成了机器学习领域公认的重大挑战，被视为衡量AI系统高级数学推理能力的标杆。

今年，我们把组合后的AI系统用于IMO组织方提供的竞赛题目。我们的解答由知名数学家根据IMO评分规则进行评判，包括剑桥大学的蒂莫西·高尔斯爵士，他是IMO金牌得主和菲尔兹奖获得者，以及约瑟夫·迈尔斯博士，两届IMO金牌得主、2024年IMO选题委员会主席。

这个程序能想出一个如此不明显的辅助构造，实在令人印象深刻，远远超出了我以为的当前最高水平。

蒂莫西·高尔斯爵士
IMO金牌得主、菲尔兹奖获得者

首先，题目被人工翻译成形式化数学语言，以便我们的系统理解。正式比赛中，学生分两场作答，每场4.5小时。我们的系统解出一道题只花了几分钟，其余题目则花了最多三天。

AlphaProof通过确定答案并证明其正确性，解决了两个代数题和一个数论题。其中包含本次竞赛最难的一道题，全场只有五名选手做出来了。AlphaGeometry 2证明了几何题，两道组合题未能解决。

六道题每题满分七分，总分最高42分。我们的系统最终得分28分，每道解出的题都拿了满分，相当于银牌区间的最高档。今年金牌线从29分起步，全场609名参赛者中有58人达到。

图表展示我们的AI系统在2024年IMO中相对于人类选手的表现。总分42分中我们拿到28分，达到了银牌选手的水平。

AlphaProof：形式化的推理路径

AlphaProof是一个用形式化语言Lean来训练自己证明数学命题的系统。它把一个预训练语言模型和AlphaZero强化学习算法结合在一起，后者此前曾自学掌握了国际象棋、将棋和围棋。

形式化语言有一个关键优势：涉及数学推理的证明可以被形式化验证其正确性。但它在机器学习中的使用此前一直受限于人工编写数据量太少。

相比之下，基于自然语言的方法虽然能获取多出几个数量级的数据，却可能生成看似合理但实际错误的中间推理步骤和解答。我们在两个互补领域之间搭了一座桥：微调一个Gemini模型，让它自动把自然语言问题陈述翻译成形式化陈述，从而创建了一个包含各种难度形式化问题的大型库。

面对一道题时，AlphaProof会生成候选解，然后在Lean中搜索可能的证明步骤来证明或推翻它们。每一个被找到并验证的证明都会用来强化AlphaProof的语言模型，提升它解决后续更难问题的能力。

备战IMO期间，我们在数周内让AlphaProof证明或推翻了数百万道题，覆盖各种难度和数学领域。训练循环在竞赛期间也持续运行，不断强化对竞赛题自生成变体的证明，直到找到完整解答。

AlphaProof强化学习训练循环流程图：约一百万个非形式化数学问题被形式化网络翻译成形式化数学语言。然后求解网络搜索这些问题的证明或反证，通过AlphaZero算法逐步训练自己解决更具挑战性的问题。

更具竞争力的AlphaGeometry 2

AlphaGeometry 2是AlphaGeometry的大幅改进版。它是一个神经符号混合系统，语言模型基于Gemini，用比前代多一个数量级的合成数据从头训练。这帮助模型应对更具挑战性的几何问题，包括涉及物体运动和角度、比例或距离方程的问题。

AlphaGeometry 2配备的符号引擎比前代快两个数量级。面对新问题时，一种新的知识共享机制被用来实现不同搜索树的高级组合，以处理更复杂的问题。

在今年竞赛之前，AlphaGeometry 2已经能解决过去25年IMO历史几何题中的83%，而前代只有53%。在2024年IMO中，AlphaGeometry 2在收到形式化题目后19秒内就解决了第四题。

第四题示意图：要求证明∠KIL与∠XPY之和等于180度。AlphaGeometry 2提出构造点E，位于直线BI上，使得∠AEB等于90度。点E为AB的中点L赋予了意义，创造出多对相似三角形，如ABE相似于YBI、ALE相似于IPC，这些都是证明结论所需要的。

数学推理的新前沿

在IMO工作之外，我们还试验了一个自然语言推理系统，基于Gemini和我们最新的研究，具备高级解题能力。这个系统不需要把题目翻译成形式化语言，可以与其他AI系统组合使用。我们也在今年的IMO题目上测试了这种方法，结果很有前景。

我们的团队正在继续探索多种AI方法来推进数学推理，我们已在《自然》论文中发布了AlphaProof的更多技术细节。

我们期待这样一个未来：数学家和AI工具一起探索假设、尝试大胆的新方法来解决长期未解的问题、快速完成证明中耗时的部分，而像Gemini这样的AI系统在数学和更广泛的推理方面变得更强。

致谢

感谢国际数学奥林匹克组织对我们的支持。

AlphaProof的开发由Thomas Hubert、Rishi Mehta和Laurent Sartran领导；AlphaGeometry 2和自然语言推理工作由Thang Luong领导。

AlphaProof的主要贡献者包括Hussain Masoom、Aja Huang、Miklós Z. Horváth、Tom Zahavy、Vivek Veeriah、Eric Wieser、Jessica Yung、Lei Yu、Yannick Schroecker、Julian Schrittwieser、Ottavia Bertolli、Borja Ibarz、Edward Lockhart、Edward Hughes、Mark Rowland、Grace Margand。Alex Davies和Daniel Zheng领导了非形式化系统的开发，如最终答案确定，主要贡献者包括Iuliya Beloshapka、Ingrid von Glehn、Yin Li、Fabian Pedregosa、Ameya Velingker和Goran Žužić。Oliver Nash、Bhavik Mehta、Paul Lezeau、Salvatore Mercuri、Lawrence Wu、Calle Soenne、Thomas Murrills、Luigi Massacci和Andrew Yang作为Lean专家提供了建议和贡献。过往贡献者包括Amol Mandhane、Tom Eccles、Eser Aygün、Zhitao Gong、Richard Evans、Soňa Mokrá、Amin Barekatain、Wendy Shang、Hannah Openshaw、Felix Gimeno。本工作由David Silver和Pushmeet Kohli指导。

AlphaGeometry 2的开发由Trieu Trinh和Yuri Chervonyi领导，主要贡献者包括Mirek Olšák、Xiaomeng Yang、Hoang Nguyen、Junehyuk Jung、Dawsen Hwang和Marcelo Menegali。自然语言推理系统的开发由Golnaz Ghiasi、Garrett Bingham、YaGuang Li领导，主要贡献者包括Swaroop Mishra、Nigamaa Nayakanti、Sidharth Mudgal、Qijun Tan、Junehyuk Jung、Hoang Nguyen、Alex Zhai、Dawsen Hwang、Mingyang Deng、Clara Huiyi Hu、Jarrod Kahn、Maciej Kula、Cosmo Du。AlphaGeometry和自然语言推理系统均由Quoc Le指导。

David Silver、Quoc Le、Demis Hassabis和Pushmeet Kohli协调和管理了整个项目。

我们还感谢Insuk Seo、Evan Chen、Zigmars Rasscevskis、Kari Ragnarsson、Junhwi Bae、Jeonghyun Ahn、Jimin Kim、Hung Pham、Nguyen Nguyen、Son Pham和Pasin Manurangsi帮助评估我们语言推理系统的质量。Jeff Stanway、Jessica Lo、Erica Moreira、Petko Yotov和Kareem Ayoub在计算资源提供和管理方面的支持。IMO理事会的Gregor Dolinar教授和Geoff Smith博士MBE的支持与合作；以及Tu Vu、Hanzhao Lin、Chenkai Kuang、Vikas Verma、Yifeng Lu、Xinyun Chen、Denny Zhou、Vihan Jain、Henryk Michalewski、Xavier Garcia、Arjun Kar、Lampros Lamprou、Kaushal Patel、Kelvin Xu、Ilya Tolstikhin、Olivier Bousquet、Anton Tsitsulin、Dustin Zelle、CJ Carey、Sam Blackwell、Abhi Rao、Vahab Mirrokni、Behnam Neyshabur、Ethan Dyer、Keith Rush、Moritz Firsching、Dan Shved、Ihar Bury、Divyanshu Ranjan、Hadi Hashemi、Alexei Bendebury、Soheil Hassas Yeganeh、Shibl Mourad、Simon Schmitt、Satinder Baveja、Chris Dyer、Jacob Austin、Wenda Li、Heng-tze Cheng、Ed Chi、Koray Kavukcuoglu、Oriol Vinyals、Jeff Dean和Sergey Brin的支持和建议。

最后，感谢Lean和Mathlib项目的众多贡献者，没有他们，AlphaProof不可能实现。

常见问题（FAQ）

AlphaProof和AlphaGeometry 2在2024年IMO中解决了哪些题目？

AlphaProof解决了两个代数题和一个数论题，包括全场仅五人做出的最难题；AlphaGeometry 2解决了几何题。组合系统共解出六题中的四题，得分28分，达到银牌水平。

AlphaProof如何保证推理过程的正确性？

AlphaProof使用形式化数学语言Lean逐步验证证明，每一步都经得起检查，没有跳步。它结合预训练语言模型和AlphaZero强化学习算法，通过搜索和验证证明来训练自己。

AlphaGeometry 2相比前代有哪些改进？

AlphaGeometry 2使用多一个数量级的合成数据从头训练，符号引擎快两个数量级，并引入新的知识共享机制。它能解决过去25年IMO几何题的83%，而前代仅53%。