AI 在国际数学奥林匹克竞赛中的表现：AlphaProof 和 AlphaGeometry 2 如何达到银牌标准

数学推理是人类认知能力的一个重要方面，推动科学发现和技术发展的进步。随着我们努力开发与人类认知相匹配的人工智能，一般性的人工智能，赋予人工智能先进的数学推理能力至关重要。虽然当前的人工智能系统可以处理基本的数学问题，但它们在处理需要复杂推理的高级数学学科如代数和几何时却苦于应付。然而，这种情况可能正在改变，因为谷歌 DeepMind 在提高人工智能系统的数学推理能力方面取得了显著进展。这一突破是在 2024 年的国际数学奥林匹克竞赛（IMO）中实现的。国际数学奥林匹克竞赛成立于 1959 年，是最古老、最负盛名的数学竞赛，向来自世界各地的高中生提出代数、组合数学、几何和数论方面的挑战。每年，年轻数学家的团队竞争解决六个非常具有挑战性的问题。本年，谷歌 DeepMind 介绍了两个人工智能系统：AlphaProof，专注于形式化数学推理，和 AlphaGeometry 2，专门解决几何问题。这些人工智能系统成功解决了四个问题，达到银牌获奖者的水平。在本文中，我们将探讨这些系统如何解决数学问题。

AlphaProof：将人工智能和形式语言结合用于数学定理证明

AlphaProof 是一个旨在使用 Lean 形式语言证明数学陈述的人工智能系统。它集成了 Gemini，一种预训练的语言模型，和 AlphaZero，一种著名的强化学习算法，曾经在国际象棋、将棋和围棋中取得了杰出的成就。

Gemini 模型将自然语言问题陈述转换为形式化的陈述，创建了一个具有不同难度级别的问题库。这种方法有两个目的：将不精确的自然语言转换为精确的形式语言，以验证数学证明，并使用 Gemini 的预测能力生成一个具有形式语言精度的可能解决方案列表。

当 AlphaProof 遇到一个问题时，它会生成潜在的解决方案，并在 Lean 中搜索证明步骤以验证或驳斥它们。这基本上是一种神经符号方法，其中神经网络 Gemini 将自然语言指令转换为符号形式语言 Lean，以证明或驳斥该陈述。与 AlphaZero 的自我对战机制类似，AlphaProof 通过尝试证明数学陈述来训练自己。每次证明尝试都改进了 AlphaProof 的语言模型，成功的证明加强了模型处理更具挑战性的问题的能力。

在国际数学奥林匹克竞赛中，AlphaProof 通过证明或驳斥数百万个涵盖不同难度级别和数学主题的问题进行了训练。这种训练在竞赛期间继续进行，AlphaProof不断改进其解决方案，直到找到问题的完整答案。

AlphaGeometry 2：将大型语言模型和符号人工智能集成用于解决几何问题

AlphaGeometry 2 是 AlphaGeometry 系列的最新版本，旨在以增强的精度和效率解决几何问题。它在其前身的基础上采用了一种神经符号方法，将大型语言模型（LLM）与符号人工智能集成。这种集成将基于规则的逻辑与神经网络的预测能力相结合，用于识别辅助点，这对于解决几何问题至关重要。AlphaGeometry 的 LLM 预测新的几何构造，而符号人工智能应用形式逻辑来生成证明。

当面临一个几何问题时，AlphaGeometry 的 LLM 评估多种可能性，预测出解决问题的关键构造。这些预测作为有价值的线索，引导符号引擎朝着准确的推理和解决方案迈进。这一创新方法使 AlphaGeometry 能够解决超出传统场景的复杂几何挑战。

AlphaGeometry 2 的一个关键增强是集成了 Gemini LLM。这个模型从头开始在大量合成数据上进行训练，使其能够处理更困难的几何问题，包括涉及物体运动和角度、比率或距离方程的问题。另外，AlphaGeometry 2 的符号引擎运行速度快了两个数量级，使其能够以前所未有的速度探索替代解决方案。这些进步使 AlphaGeometry 2 成为解决复杂几何问题的强大工具，在该领域设定了新的标准。

AlphaProof 和 AlphaGeometry 2 在 IMO

今年的国际数学奥林匹克竞赛中，参赛者面临六个不同类型的问题：两个代数问题、一个数论问题、一个几何问题和两个组合数学问题。谷歌研究人员将这些问题翻译成形式化的数学语言，以便 AlphaProof 和 AlphaGeometry 2 使用。AlphaProof 解决了两个代数问题和一个数论问题，包括本次竞赛中最困难的问题，只有五名人类参赛者解决了它。同时，AlphaGeometry 2 成功解决了几何问题，尽管它没有解决两个组合数学挑战。

每个问题在 IMO 中都值 7 分，总分为 42 分。AlphaProof 和 AlphaGeometry 2 获得了 28 分，在它们解决的问题上获得了满分。这使它们达到银牌级别的高端。今年的金牌门槛是 29 分，共有 609 名参赛者中有 58 名达到这一标准。

下一步：自然语言用于数学挑战

AlphaProof 和 AlphaGeometry 2 已经展示了人工智能在数学问题解决方面的显著进步。然而，这些系统仍然依赖人类专家将数学问题翻译成形式语言以进行处理。此外，尚不清楚这些专门的数学技能如何融入其他人工智能系统中，例如用于探索假设、测试创新解决方案和高效管理证明的时间-consuming 方面。

为了克服这些局限性，谷歌研究人员正在开发一个基于 Gemini 和他们最新研究的自然语言推理系统。这个新系统旨在提高问题解决能力，而无需形式语言翻译，并设计为与其他人工智能系统无缝集成。

结论

AlphaProof 和 AlphaGeometry 2 在国际数学奥林匹克竞赛中的表现标志着人工智能在解决复杂数学推理方面的一个显著飞跃。两种系统都展示了银牌级别的性能，解决了四个具有挑战性的问题，展示了形式化证明和几何问题解决方面的显著进步。尽管它们取得了成就，这些人工智能系统仍然依赖于人类输入来翻译问题成形式语言，并面临着与其他人工智能系统集成的挑战。未来的研究旨在进一步增强这些系统，可能通过集成自然语言推理来扩展其能力，以应对更广泛的数学挑战。