具有高级数学推理能力的通用人工智能（AGI）有望在科学和技术领域开辟新的前沿。当前的 AI 系统由于推理技能和训练数据的局限性，在解决一般数学问题时仍存在困难。就在昨天，Google DeepMind 的 AlphaProof 和 AlphaGeometry 团队推出了一个基于强化学习的形式数学推理新系统 AlphaProof，以及几何解题系统的改进版本 AlphaGeometry 2。
这两个系统共同解决了今年国际数学奥林匹克竞赛（IMO）六个问题中的四个，首次达到银牌获得者的水平。近年来，IMO 年度竞赛被广泛认为是机器学习的一大挑战，也是衡量 AI 系统高级数学推理能力的理想基准。今年，Google DeepMind 将其联合 AI 系统应用于 IMO 组织者提供的问题。
他们的解决方案根据 IMO 的评分规则进行了评分，评分者包括著名的数学家、IMO 金牌得主和菲尔兹奖得主 Timothy Gowers 教授，以及两次 IMO 金牌得主、2024 年 IMO 问题选择委员会主席 Joseph Myers 博士。
AlphaProof 是一个系统，它自我训练以在 Lean 的形式语言中证明数学陈述。它将一个预训练的语言模型与 AlphaZero 强化学习算法相结合，后者之前自学掌握了国际象棋、将棋和围棋的游戏。形式语言提供了关键优势，即涉及数学推理的证明可以正式验证其正确性。然而，它们在机器学习中的应用之前受到了人类编写数据极其有限的制约。
AlphaGeometry 2 是 AlphaGeometry 的显著改进版本。它是一个神经符号混合系统，其语言模型基于 Gemini，并在比其前身多一个数量级的合成数据上从头开始训练。这帮助模型解决更具有挑战性的几何问题，包括关于物体运动和角度、比例或距离的方程问题。AlphaGeometry 2 使用的符号引擎比其前身快两个数量级。
面对新问题时，一种新颖的知识共享机制被用来实现不同搜索树的先进组合，以解决更复杂的问题。