高级数学推理是现代人工智能的关键能力，谷歌DeepMind再一次展示了它在这一领域的卓越实力。
近日，谷歌宣布其混合人工智能系统在2024年的国际数学奥林匹克竞赛（IMO）中表现优异，获得了相当于银牌的成绩，且仅仅差1分就能摘得金牌。这一突破被认为是AI研究领域的又一个里程碑，被许多人称为“数学界的AlphaGo时刻”。
在IMO中，AlphaGeometry 2在接收到形式化的第4题后，仅用19秒就解决了这个问题。
具体来说google展示了第一个以银牌级别解决国际数学奥林匹克问题的人工智能。
它结合了 AlphaProof（一种新的突破性形式推理模型）和 AlphaGeometry 2（之前系统的改进版本）。
国际数学奥林匹克竞赛是全球最悠久、规模最大、最具声望的青年数学家比赛，自1959年起每年举办一次。参赛者需要解决六道涉及代数、组合学、几何和数论的极其困难的问题。许多菲尔兹奖得主曾在青年时期代表国家参加过IMO。近年来，IMO也成为了机器学习领域的一个重要挑战，被视为衡量人工智能系统高级数学推理能力的标杆。
在今年的比赛中，DeepMind的AI系统获得了28分（满分42分），相当于银牌获得者的水平。这一成绩仅差1分就能达到金牌标准，而在今年的609名参赛者中，只有58人获得了金牌。
AlphaProof：形式化数学推理的突破
AlphaProof系统采用强化学习方法，将预训练的语言模型与AlphaZero算法相结合。这种方法的优势在于可以正式验证涉及数学推理的证明的正确性。为了克服形式化语言训练数据不足的问题，研究团队通过微调Gemini模型，创建了一个包含各种难度的形式化问题库。
AlphaProof是一个自学习系统，专门用于在形式化数学语言Lean中证明数学陈述。它的核心创新在于结合了预训练语言模型和AlphaZero强化学习算法。
工作流程如下：
问题转化：首先，使用经过微调的Gemini模型将自然语言的数学问题自动转换为Lean的形式化语言。这一步骤创建了一个大型的形式化问题库，涵盖不同难度级别。
解决方案生成：面对一个新问题时，AlphaProof会生成可能的解决方案
证明搜索：系统在Lean中搜索可能的证明步骤，试图证明或反驳这些解决方案
强化学习：每找到并验证一个证明，就用它来强化AlphaProof的语言模型，提高系统解决后续更具挑战性问题的能力
持续训练：在准备IMO比赛期间，AlphaProof在数周内证明或反驳了数百万个问题，覆盖各种难度和数学主题。在比赛过程中，它还继续应用这个训练循环，通过证明自己生成的比赛问题变体来增强能力，直到找到完整解决方案
AlphaGeometry 2
AlphaGeometry 2是AlphaGeometry的改进版本，它的语言模型基于Gemini，并在比前代多一个数量级的合成数据上进行了训练。
AlphaGeometry 2是一个神经符号混合系统。主要改进包括：
增强的语言模型：基于Gemini，从头开始训练，使用了比前代多一个数量级的合成数据。这大大提高了模型处理复杂几何问题的能力，包括物体运动、角度方程、比例或距离等问题。
更快的符号引擎：新版本的符号处理引擎速度提高了两个数量级，大大加快了问题解决速度。
知识共享机制：引入了新的知识共享机制，能够高级组合不同的搜索树，以解决更复杂的问题。
性能提升：在接受今年IMO比赛前，AlphaGeometry 2能够解决过去25年IMO几何问题的83%，远超前代系统53%的解决率
实时表现：在今年的IMO中，AlphaGeometry 2在接收到形式化的第4题后，仅用19秒就解决了这个问题。
DeepMind的研究团队还在探索基于自然语言推理的系统，这种系统不需要将问题转换为形式化语言，可能与其他AI系统结合使用。这种方法在今年的IMO问题上也显示出了巨大的潜力。
采用神经符号方法
AlphaGeometry是一套神经符号系统，由神经语言模型加符号推导引擎组成，希望两相结合以寻求对复杂几何定理的证明。这类似于“快、慢思考相结合”的理念，一个系统提供快速、“直观”的想法，另一系统则做出更加深思熟虑的理性决策。
由于语言模型更擅长发现数据中的一般模式和关系，所以能够快速预测可能有用的潜在构造，但却往往缺乏严格推理并解释其决策的能力。另一方面，符号推导引擎则基于形式逻辑，依靠明确的规则来得出结论。后者更理性、可解释性更强，但往往比较“缓慢”且不够灵活——这一点在单独处理大型复杂问题时体现得尤其明显。
AlphaGeometry的语言模型会引导其符号推导引擎为几何问题寻求可能的解。
奥数几何问题的题干大多基于图表，需要添加新的几何构造才能解决，例如点、线或圆。AlphaGeometry的语言模型可以从无数种可能性中预测添加哪些新构造更有助于解题。这些线索能够填补空白，引导符号引擎对图表做进一步推论并逐步趋近正确答案。
AlphaGeometry解决的一个简单问题：给定问题图及其定理前提（左），AlphaGeometry（中）首先使用符号引擎来推导关于图的新表述，直到找出正确解或用尽新表述。
如果找不到可行的解，AlphaGeometry语言模型会添加一种可能有用的构造（蓝色部分，即辅助线）为符号引擎开辟新的推导路径。整个循环不断重复，直到找到正确解为止（右）。在此示例中，只需要一种新构造（一条辅助线）。
AlphaGeometry提出的每一道奥数题解法，都经过计算机检查和验证。DeepMind还将结果与之前的AI方法以及人类选手在奥赛中的表现做出比较。此外，数学教练、前奥数竞赛金牌得主Evan Chen也帮助对AlphaGeometry的解题思路进行评估。
