TLDR
• Google DeepMind 的 AI 系统在国际数学奥林匹克竞赛 (IMO) 中取得了银牌水平的成绩，标志着 AI 在解决高级数学推理问题方面取得了重大突破。
• 这两个名为 AlphaProof 和 AlphaGeometry 2 的 AI 系统，分别在形式数学推理和几何问题解决上展现出强大的能力。
• 自然语言推理系统作为 DeepMind 的未来研究方向，有望进一步提高 AI 在解决数学问题方面的能力。
引言
数学，这门探索数字、结构、空间和变化的学科，长久以来一直被视为人类智慧的巅峰之作。从古巴比伦泥板上的楔形文字到现代数学的抽象符号，人类对数学的探索从未停止。而近年来，人工智能 (AI) 作为一股新兴力量，正在数学领域掀起一场前所未有的革命。
国际数学奥林匹克竞赛 (IMO)，这场被誉为“数学世界杯”的顶级赛事，每年都吸引着来自全球各地的数学天才同台竞技。IMO 的题目以其难度和深度著称，即使对于经验丰富的数学家来说也是一项艰巨的挑战。然而，在 2024 年的 IMO 中，一个不同寻常的选手横空出世，它就是来自 Google DeepMind 的 AI 系统。这个 AI 系统在比赛中取得了令人瞩目的成绩，一举夺得银牌，标志着 AI 在解决高级数学推理问题方面取得了重大突破。
AI 在 IMO 中大放异彩
拥有高级数学推理能力的通用人工智能 (AGI) 有可能开辟科学和技术的未知领域。一直以来，在构建能够帮助数学家发现新见解、新算法以及解答开放性问题的 AI 系统方面取得了巨大进步。但目前的 AI 系统在解决一般数学问题上仍然步履维艰，原因在于推理能力和训练数据的限制。
国际数学奥林匹克竞赛 (IMO) 是全球最负盛名的数学竞赛之一，旨在激发青少年对数学的兴趣和才能。自 1959 年首次举办以来，IMO 已经成为一个全球性的盛会，每年都吸引着来自 100 多个国家和地区的数百名优秀学生参加。IMO 的题目涵盖了代数、组合数学、几何和数论等多个领域，要求参赛者具备极强的逻辑思维能力、问题解决能力和创造力。许多菲尔兹奖（数学家的最高荣誉之一）的获得者都曾代表他们的国家参加过 IMO。
近年来，年度 IMO 竞赛也被广泛认为是机器学习领域的一项重大挑战，是衡量 AI 系统高级数学推理能力的一个重要基准。在 2024 年的 IMO 中，Google DeepMind 的 AI 系统首次参赛便引起了广泛关注。该系统由两个主要部分组成：AlphaProof 和 AlphaGeometry 2。AlphaProof 擅长解决形式数学推理问题，而 AlphaGeometry 2 则专注于几何问题。在比赛中，AI 系统需要解决六道极具挑战性的数学题，这些题目涵盖了 IMO 所涉及的各个领域。
这些解决方案由著名的数学家蒂莫西·高尔斯爵士(IMO 金牌得主和菲尔兹奖得主)和约瑟夫·迈尔斯博士(两届 IMO 金牌得主和 IMO 2024 问题选择委员会主席)根据 IMO 的评分规则进行评分。首先，将问题手动翻译成我们的系统可以理解的正式数学语言。在正式比赛中，学生需要在两场各 4.5 小时的考试中提交答案。而我们的系统解决一道题只需几分钟，而解决其他问题则需要长达三天的时间。
经过激烈的角逐，Google DeepMind 的 AI 系统最终取得了 28 分的优异成绩，相当于银牌组的最高水平。今年，金牌门槛为 29 分，在正式比赛的 609 名参赛者中，有 58 人达到了这一水平。值得一提的是，AI 系统在所有解决的题目上都获得了满分，这充分证明了其在数学推理方面的强大实力。
AlphaProof：形式推理的集大成者
AlphaProof 是一个基于强化学习的 AI 系统，专门用于解决形式数学推理问题，它可以确定答案并证明它是正确的。它将一个预先训练的语言模型与 AlphaZero 强化学习算法相结合，AlphaZero 之前教会了自己如何掌握国际象棋、日本将棋和围棋。
形式语言是数学推理的基石，它提供了一种精确、严谨的方式来表达数学概念和证明数学定理。形式语言的使用可以有效避免自然语言的歧义性和不确定性，确保数学推理的严谨性和可验证性。而强化学习作为一种强大的机器学习方法，可以让 AI 系统通过与环境的交互来学习最佳策略。
在 AlphaProof 中，形式语言和强化学习这两种强大的技术得到了完美融合。AlphaProof 利用预先训练的语言模型来理解和生成数学表达式，并使用 AlphaZero 强化学习算法来不断优化其证明策略。具体来说，AlphaProof 会首先将一个数学问题转化为形式语言表示，然后利用语言模型生成一系列可能的证明步骤。每一步证明都会被送入一个验证器中进行检验，如果证明正确，则 AlphaProof 会得到奖励，否则就会受到惩罚。通过这种不断的试错和学习，AlphaProof 能够逐渐掌握解决形式数学推理问题的技巧，并在面对新的数学挑战时表现出色。
AlphaProof 是一个在形式语言 Lean 中训练自己证明数学陈述的系统。形式语言提供了一个关键优势，即涉及数学推理的证明可以正式验证其正确性。然而，它们在机器学习中的应用以前一直受到可用的手写数据量非常有限的限制。相比之下，基于自然语言的方法可能会虚构出看似合理但不正确的中间推理步骤和解决方案，尽管它们可以访问多得多的数据。通过微调 Gemini 模型来自动将自然语言问题陈述翻译成形式语句，我们在这两个互补的领域之间架起了一座桥梁，创建了一个包含各种难度的大型形式问题库。
当遇到一个问题时，AlphaProof 会生成候选解决方案，然后通过在 Lean 中搜索可能的证明步骤来证明或反驳它们。每个被发现和验证的证明都被用来强化 AlphaProof 的语言模型，增强其解决后续更具挑战性问题的能力。
我们通过证明或反驳数百万个问题来训练 AlphaProof 参加 IMO，这些问题涵盖了各种难度和数学主题领域，为期数周，直至比赛开始。在比赛期间也应用了训练循环，强化对竞赛问题的自生成变体的证明，直到找到完整的解决方案。
AlphaProof 在 IMO 比赛中的出色表现证明了其在解决形式数学推理问题方面的巨大潜力。它不仅能够解决一些经典的数学难题，还能够为数学家提供新的思路和方法。
AlphaGeometry 2：几何问题的征服者
AlphaGeometry 2 是一个神经符号混合系统，在解决几何问题方面表现出色。它结合了深度学习和符号推理的优势，能够更有效地处理几何图形和空间关系。AlphaGeometry 2 是 AlphaGeometry 的一个显著改进版本。它是一个神经符号混合系统，其语言模型基于 Gemini，并从头开始训练，其合成数据量比其前身多出一个数量级。这有助于该模型解决更具挑战性的几何问题，包括关于物体运动以及角度、比率或距离方程的问题。
AlphaGeometry 2 使用比其前身大得多的数据集进行训练，并具有比其前身快两个数量级的符号引擎。此外，AlphaGeometry 2 还采用了一种新颖的知识共享机制，允许不同搜索树之间的信息交流，从而提高了求解复杂问题的效率。当遇到新问题时，将使用一种新颖的知识共享机制来实现不同搜索树的高级组合，以解决更复杂的问题。
在今年的比赛之前，AlphaGeometry 2 可以解决过去 25 年所有历史 IMO 几何问题的 83%，而其前身的解决率为 53%。在 IMO 2024 中，AlphaGeometry 2 在收到其形式化后的 19 秒内就解决了问题 4。
在 IMO 比赛中，AlphaGeometry 2 成功解决了一道几何难题，这道题目需要参赛者证明一个关于三角形和圆的复杂定理。AlphaGeometry 2 利用其强大的混合架构，首先识别出图形中的关键特征，然后利用几何定理进行推理和证明，最终找到了正确的解决方案。
自然语言推理：AI 数学推理的未来
自然语言推理系统是 DeepMind 正在积极探索的未来方向之一。与 AlphaProof 和 AlphaGeometry 2 不同，自然语言推理系统不需要将问题翻译成形式语言，而可以直接理解和处理自然语言表达的数学问题。
作为 IMO 工作的一部分，我们还试验了一个自然语言推理系统，该系统建立在 Gemini 和我们最新的研究成果之上，以实现高级问题解决能力。该系统不需要将问题翻译成形式语言，并且可以与其他 AI 系统相结合。我们还在今年的 IMO 问题上测试了这种方法，结果显示出巨大的潜力。
自然语言是人类日常生活中使用的语言，它比形式语言更加灵活和表达能力更强。然而，自然语言也更加复杂和难以处理，因为它包含了大量的歧义性、隐喻和上下文信息。为了让 AI 系统能够理解自然语言表达的数学问题，DeepMind 的研究人员正在开发新的自然语言处理技术，例如深度语义分析、上下文感知和常识推理等。
自然语言推理系统是 AI 数学推理的终极目标之一，因为它将使 AI 系统能够像人类一样理解和解决数学问题。想象一下，在未来，你可以直接用自然语言向 AI 系统提问：“如何证明勾股定理？”或者“如何求解这个微分方程？”，而 AI 系统则能够像一位经验丰富的数学老师一样，为你提供详细的解答和解释。
结论
AI 在 IMO 中的突破性表现预示着 AI 数学推理的光明未来。随着 AI 技术的不断发展，我们可以预见，AI 将在数学领域发挥越来越重要的作用。AI 不仅可以帮助数学家解决更加复杂的数学难题，还可以为数学教育和数学普及做出贡献。在未来，AI 将成为数学家不可或缺的伙伴，共同推动数学这门古老学科的发展。我们的团队将继续探索多种 AI 方法来推进数学推理，并计划很快发布更多关于 AlphaProof 的技术细节。
我们很高兴看到，在未来，数学家将使用 AI 工具来探索假设，尝试大胆的新方法来解决长期存在的问题，并快速完成耗时的证明元素，并且像 Gemini 这样的 AI 系统在数学和更广泛的推理方面变得更加强大。
相关链接
• Google DeepMind 博客文章：https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
