DeepMind的突破性模型AlphaProof和AlphaGeometry 2解决了高级数学推理问题，在今年的国际数学奥林匹克竞赛（IMO）中达到银牌水平。AlphaProof基于强化学习进行形式化数学推理，而AlphaGeometry 2则是改进版几何问题解决系统。这些系统解决了本年度竞赛的六道题中的四道，得分28分，与银牌标准相当。
AlphaProof是一种基于强化学习的形式化数学推理系统，能够证明数学陈述的正确性。它结合了预训练语言模型和AlphaZero强化学习算法，使用形式语言Lean进行训练和推理。
AlphaGeometry 2是改进版的几何问题解决系统，采用神经符号混合方法，并在大量合成数据上进行了训练。该系统能够更快、更高效地解决几何问题。
- 国际数学奥林匹克简介：IMO是历史最悠久、规模最大、最负盛名的青年数学竞赛，每年吸引世界顶尖的预科学家参加。
- 模型表现：在今年的IMO中，AlphaProof和AlphaGeometry 2共解决了四个问题，得到了28分，与银牌得主的成绩相当。
- AlphaProof在Lean中创建证明，结合了预训练的语言模型和AlphaZero强化学习算法。
- AlphaGeometry 2是一个神经符号混合系统，能够解决过去25年历史问题的83%。
- 该AI系统旨在加速AI驱动的数学研究，解锁新的知识。并向通用人工智能（AGI）迈进。
图中显示了Deepmind的人工智能系统在 2024 年国际海事组织（IMO）比赛中相对于人类选手的表现。在 42 分的总分中，我们获得了 28 分，达到了与银牌获得者相同的水平。
AlphaProof
- 能力：
- AlphaProof能够理解并解决复杂的数学证明问题。
- 它可以处理代数和数论等领域的问题。
- 在国际数学奥林匹克（IMO）比赛中，AlphaProof成功解决了两个代数问题和一个数论问题，其中包括一个只有五个参赛选手能够解决的极难问题。
- 工作原理：
- 强化学习与形式语言结合：AlphaProof使用强化学习算法，不断尝试和学习，以提高解题能力。通过形式语言Lean，将数学问题转化为机器可以处理的形式。
- Gemini模型的自然语言翻译：为了弥补人类编写的数学数据不足，AlphaProof通过微调Gemini模型，将自然语言中的数学问题翻译成形式化问题，用于训练模型。
- 自动生成与验证证明：面对新问题时，AlphaProof生成多个可能的解法，并通过搜索Lean中的可能步骤来验证或驳斥这些解法。每次成功验证后，这些证明步骤会强化模型的神经网络，使其在解决后续更难问题时表现更佳。
- 持续自我强化：通过训练数百万个问题，AlphaProof不断增强其推理和解题能力。在比赛期间，模型通过自我生成的变体问题进行持续训练，直到找到完整解决方案。
- 应用：
- 数学研究与发现：AlphaProof可以协助数学家发现新理论、验证复杂证明，节省大量时间和精力。
- 教育与学习：在教育领域，AlphaProof可以帮助学生理解复杂的数学概念，并验证他们的解题过程。
AlphaProof 强化学习训练循环过程信息图：约一百万个非正式数学问题被形式化网络翻译成正式数学语言。然后，求解器网络搜索问题的证明或反证，通过 AlphaZero 算法逐步训练自己解决更具挑战性的问题。
AlphaGeometry 2
- 能力：
- AlphaGeometry 2专注于解决几何问题，具有极高的准确性和效率。
- 它在处理几何问题时表现出色，在今年的IMO中，成功解决了一个几何问题，用时仅19秒。
- 它的改进版本相比前代解决了更多的几何问题，在过去25年的IMO几何题中达到了83%的解决率。
- 原理：
- 神经符号混合方法：AlphaGeometry 2结合了神经网络和符号推理的方法。神经网络帮助理解和处理几何题目，符号推理用于精确计算和验证解法。
- 知识共享机制：当面对新问题时，AlphaGeometry 2利用已有的知识库，通过共享和组合不同的搜索树，快速找到解法。
- 高速符号引擎：改进后的符号引擎比前代快了两个数量级，使得AlphaGeometry 2能够更快地处理复杂的几何问题。
- 合成数据训练：通过大量的合成数据进行训练，使模型在处理各种不同类型的几何问题时更加灵活和高效。
- 应用：
- AlphaGeometry 2的几何问题解决能力使其在教育、科学研究和工程应用中具有广泛的潜力。
- 它能够帮助学生和研究人员快速解决几何问题，提高学习和研究效率。
官方博客翻译
AI在解决国际数学奥林匹克问题上达到银牌标准
突破性模型AlphaProof和AlphaGeometry 2解决了数学中的高级推理问题
具备高级数学推理能力的通用人工智能 (AGI) 有望在科学和技术领域开辟新前沿。
我们在开发帮助数学家发现新见解、新算法和解决未解问题的AI系统方面取得了重大进展。但目前的AI系统在解决一般数学问题时仍存在推理能力和训练数据的限制。
今天，我们推出了AlphaProof，这是一个基于强化学习的形式数学推理新系统，还有改进版的AlphaGeometry 2，我们的几何解题系统。这两个系统共同解决了今年国际数学奥林匹克 (IMO) 的六个问题中的四个，首次达到了银牌水平。
解决复杂数学问题的突破性AI表现
IMO是历史最悠久、规模最大、最负盛名的年轻数学家比赛，自1959年起每年举办。
每年，顶尖的预科数学家会训练数千小时，以解决代数、组合数学、几何和数论中的六个异常困难的问题。许多菲尔兹奖得主曾代表他们的国家参加过IMO。
近些年，年度IMO竞赛也被视为机器学习中的一大挑战，并成为衡量AI系统高级数学推理能力的理想基准。
今年，我们的AI系统被应用于IMO主办方提供的竞赛问题。我们的解决方案由著名数学家、IMO金牌得主和菲尔兹奖获得者Timothy Gowers爵士和两次IMO金牌得主、IMO 2024问题选择委员会主席Joseph Myers博士根据IMO评分规则进行评分。
首先，这些问题被手动翻译成我们系统可以理解的形式数学语言。在正式比赛中，学生需要在两个4.5小时的会话中提交答案。我们的系统在几分钟内解决了一个问题，而解决其他问题则花费了三天时间。
AlphaProof解决了两个代数问题和一个数论问题，通过确定答案并证明其正确性。这包括今年IMO中只有五名参赛者解决的最难问题。AlphaGeometry 2解决了几何问题，而两个组合数学问题未能解决。
每个问题可以获得七分，总分为42分。我们的系统最终得分为28分，在每个解决的问题上都获得了满分——相当于银牌类别的最高端。今年，金牌分数线从29分起，共有58名参赛者达到了这个分数。
AlphaProof：形式化推理的新方法
AlphaProof是一个用形式语言Lean证明数学陈述的系统。它结合了预训练语言模型与之前自学掌握国际象棋、将棋和围棋游戏的AlphaZero强化学习算法。
形式语言提供了一个关键优势，可以形式化验证数学推理的证明。然而，之前由于人类编写的数据非常有限，这些语言在机器学习中的应用受到限制。
相比之下，尽管自然语言方法可以使用更多数量级的数据，但在生成中间推理步骤和解决方案时可能会出现合理但不正确的情况。我们通过微调Gemini模型自动将自然语言问题陈述转换为形式陈述，创建了一个包含不同难度形式问题的大型库，在这两个互补领域之间建立了桥梁。
面对一个问题时，AlphaProof会生成解决方案候选，并通过搜索Lean中的可能证明步骤来证明或反驳它们。每个找到并验证的证明都会加强AlphaProof的语言模型，提高其解决后续更具挑战性问题的能力。
在比赛前的几周内，我们通过证明或反驳数百万个问题，涵盖各种难度和数学主题，对AlphaProof进行了训练。比赛期间也应用了训练循环，强化自生成的比赛问题变体的证明，直到找到完整的解决方案。
更强大的AlphaGeometry 2
AlphaGeometry 2是AlphaGeometry的显著改进版。它是一个神经符号混合系统，基于Gemini的语言模型，并从头开始在比前身多一个数量级的合成数据上进行训练。这帮助模型解决了更具挑战性的几何问题，包括物体运动和角度、比率或距离方程的问题。
AlphaGeometry 2使用的符号引擎比前身快两个数量级。面对新问题时，采用了一种新颖的知识共享机制，使不同搜索树的高级组合能够解决更复杂的问题。
在今年的比赛前，AlphaGeometry 2可以解决过去25年所有历史IMO几何问题的83%，而前身的解决率为53%。在IMO 2024中，AlphaGeometry 2在接收到形式化后在19秒内解决了问题4。
问题 4 的示例，要求证明∠KIL 与∠XPY 的和等于 180°。AlphaGeometry 2 提议在直线 BI 上构造点 E，使得∠AEB = 90°。点 E 有助于实现 AB 的中点 L 的目的，从而创建许多对相似三角形，如 ABE ~ YBI 和 ALE ~ IPC，以证明结论。
数学推理的新前沿
作为IMO工作的一部分，我们还尝试了一个基于自然语言推理的系统，建立在Gemini和我们最新研究的基础上，以实现高级问题解决能力。该系统不需要将问题翻译成形式语言，并且可以与其他AI系统结合。我们还在今年的IMO问题上测试了这种方法，结果显示出很大的希望。
我们的团队继续探索多种AI方法以推进数学推理，并计划很快发布更多关于AlphaProof的技术细节。
我们对未来感到兴奋，在这个未来中，数学家可以使用AI工具探索假设，尝试解决长期问题的新方法，并快速完成证明的耗时部分——AI系统如Gemini在数学和更广泛的推理方面变得更有能力。
致谢
我们感谢国际数学奥林匹克组织的支持。
AlphaProof的开发由Thomas Hubert、Rishi Mehta和Laurent Sartran领导；AlphaGeometry 2和自然语言推理工作由Thang Luong领导。
原文：https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
