谷歌DeepMind团队推出了基于强化学习的新型形式数学推理系统AlphaProof以及几何求解系统的改进版本AlphaGeometry 2。这两个系统解决了今年国际数学奥林匹克竞赛（IMO）六道题目中的四道，首次在竞赛中取得与银牌得主同等的成绩。
近年来，一年一度的国际数学奥林匹克竞赛也被广泛认为是机器学习领域的一大挑战，也是衡量人工智能系统高级数学推理能力的理想基准。
今年，谷歌人工智能系统成功挑战了IMO主办方提供的竞赛赛题。谷歌解决方案由著名数学家、IMO金牌得主和菲尔兹奖得主蒂莫西·高尔斯教授和两届IMO金牌得主、IMO 2024问题遴选委员会主席约瑟夫·迈尔斯博士根据IMO评分规则进行评分。
首先，赛题被手动翻译成正式的数学语言，以便人工智能系统理解。在正式比赛中，学生分两节提交答案，每节4.5小时。
AlphaProof通过确定答案并证明其正确性，解决了两道代数题和一道数论题。其中包括比赛中最难的一道题，今年IMO比赛中只有五名选手解决了这道题；AlphaGeometry 2则解决了几何题目，而两道组合题目仍未解决。
六道题目每道可得7分，总分最高为42分。谷歌人工智能系统最终得分为28分，每道题目都获得满分——相当于银牌类别的最高分。今年，金牌门槛为29分，在正式比赛中，609名参赛者中有58人达到了金牌门槛。
AlphaProof是一个自我训练的系统，以形式语言Lean来证明数学陈述。它将预先训练好的语言模型与AlphaZero强化学习算法结合，后者之前曾自学过如何掌握国际象棋、将棋和围棋游戏。
形式语言的关键优势在于，涉及数学推理的证明可以得到形式化验证，以确保其正确性。相比之下，基于自然语言的方法尽管能够访问数量级更多的数据，却可能产生看似合理但实际上不正确的中间推理步骤和解决方案。谷歌通过微调Gemini模型来自动将自然语言问题陈述转换为形式陈述，从而在这两个互补领域之间建立了一座桥梁，创建了一个包含各种难度的形式化问题大型库。
当遇到问题时，AlphaProof会生成解决方案候选，然后通过搜索Lean中可能的证明步骤来证明或反驳这些候选。每个找到并验证的证明都会用于强化AlphaProof语言模型，从而提高其解决后续更具挑战性题目的能力。
AlphaGeometry 2则是AlphaGeometry的显著改进版本。它是一个神经符号混合系统，其中的语言模型基于Gemini，并使用比其前身多一个数量级的合成数据从头开始训练。这有助于该模型解决更具挑战性的几何题目，包括有关物体运动和角度、比率或距离方程的问题。
AlphaGeometry 2 采用的符号引擎比其前代产品快两个数量级。当遇到新问题时，会使用一种新颖的知识共享机制来实现不同搜索树的高级组合，以解决更复杂的问题。
