人工智能迎战数学奥林匹克的新挑战 [译]

高中数学奥林匹克选手们要注意了，AlphaGeometry 正在挑战你们在数学领域的成就。

计算机科学家 Trieu Trinh 过去四年致力于解决一个深层次的数学难题：创建一个能够解答国际数学奥林匹克中几何题目的人工智能模型。这个国际赛事汇聚了全球最优秀的数学天才高中生。

上周，Trinh 博士在纽约大学成功答辩了他的博士论文，本周他在《自然》杂志上发表了他的研究成果。这个名为 AlphaGeometry 的系统，已经能够接近人类金牌选手的水平，解决奥林匹克数学竞赛中的几何题。

在项目开发过程中，Trinh 博士向谷歌的两位研究科学家展示了这一项目，结果他被邀请成为 2021 至 2023 年间的驻地研究员。AlphaGeometry 加入了谷歌 DeepMind 的人工智能系统行列，这些系统以挑战大问题而闻名。最著名的例子可能是 AlphaZero，一个深度学习算法，在 2017 年征服了国际象棋界。与国际象棋的有限解决方案不同，数学问题的解决路径有时是无限的，这增加了难度。

Trinh 博士坦言：“我曾多次走入死胡同，误入岐途。”他是该项目的主要作者和灵魂人物。

该论文的共同作者还包括他的博士导师纽约大学的 He He 博士、曾是谷歌员工、现为 xAI（前谷歌）联合创始人的 Yuhuai Wu（Tony）、谷歌 DeepMind 的 Thang Luong 和 Quoc Le。

Trinh 博士的不懈努力最终获得了回报。“我们的成果不仅仅是一点点改进，”他说，“这是在结果上的一大飞跃，一个真正的突破。”

重大突破

Trinh 博士向我们展示了 AlphaGeometry 系统在解决一组由 2000 至 2022 年奥林匹克几何题组成的测试集中的表现。该系统成功解答了其中的 25 题；而在同一时期，平均每位人类金牌得主能解答 25.9 题。此外，Trinh 博士还将这些题目交给了 20 世纪 70 年代开发的、公认最强的几何定理证明器，而该系统仅解答了 10 题。

近几年来，谷歌 DeepMind 致力于多个探索人工智能在数学领域应用的项目。在这方面的研究普遍上，奥林匹克数学题已成为衡量标准；OpenAI 和 Meta AI 在此领域也取得了一些成果。此外，为了增加竞争激励，设立了I.M.O.大挑战，以及最近宣布的人工智能数学奥林匹克奖，设立 500 万美元奖金，颁给首个在奥林匹克中夺金的人工智能。

AlphaGeometry 的研究报告认为，证明奥林匹克定理“代表了自动推理达到人类水平的一个重要里程碑”。然而，爱丁堡大学的数学和科学历史学家 Michael Barany 对此表示质疑，他认为这是否构成数学上的一个重要成就还有待商榷。“奥林匹克的考题与绝大多数数学家所从事的创造性数学大相径庭，”他如是说。

陶哲轩，加州大学洛杉矶分校的数学家，同时还是年仅 12 岁便成为奥林匹克竞赛史上最年轻的金牌得主，他认为 AlphaGeometry 的研究成果“相当出色”，并表示这项工作取得了“意料之外的显著成就”。他指出，虽然将 AI 系统专门调整以解决奥林匹克数学题目可能不会直接增强其深入研究的能力，但在这个过程中获得的经验可能比最终结果更加宝贵。

Trinh 博士认为，数学推理虽然只是众多推理方式中的一种，但它有一个显著优势：易于验证。他表示：“数学是揭示真理的语言。” “构建 AI 的时候，打造一个追求真理、值得信赖的可靠 AI 系统显得尤为重要，尤其是在那些安全至关重要的应用领域。”

AlphaGeometry 是一种创新的“神经符号”系统，它巧妙地结合了一种类似于 ChatGPT 但规模更小的神经网络语言模型（擅长模拟人类的直觉判断）和一种类似于逻辑计算器的符号处理引擎（擅长进行逻辑推理）。

这个系统专为几何学设计，非常适合进行自动推理。福特汉姆大学的几何学家，同时也是计算机验证推理的专家 Heather Macbeth 博士（她曾在青少年时期获得两枚国际数学奥林匹克竞赛奖牌）认为：“欧几里得几何学是自动推理的理想实验场，因为它是一个规则固定、自成体系的领域。”她评价 AlphaGeometry 是一个“显著的进步”。

该系统的两大创新之处引人注目。首先，神经网络的训练完全基于算法生成的数据，高达一亿个几何证明，而且没有使用任何人类编写的示例。这种从零开始创造的合成数据，成功解决了自动定理证明领域的一个难题：缺乏能被机器解读的人类证明训练数据。何博士坦言：“最初，我对这种方法能否成功抱有一些疑虑。”

第二个创新点是，一旦 AlphaGeometry 开始解决一个问题，符号处理引擎就会介入。如果处理过程中遇到难题，神经网络便会提出增强证明论点的方法。这个循环一直持续，直到找到解决方案或耗尽时间（最长四个半小时）。这种增强过程在数学术语中被称为“辅助构造”。无论是学生还是专业数学家，他们通常会通过增加一条线、二等分一个角或画一个圆等方法来解决数学问题。在这个系统中，神经网络学会了如何进行辅助构造，并且以一种类似人类的方式进行。Trinh 博士将这比作在难以打开的瓶盖上缠绕橡皮筋，以增强手部的抓握力。

“这是一个非常有趣的概念验证，”前谷歌员工、xAI 联合创始人 Christian Szegedy 评论说。但他也指出，这个系统“还存在许多未解之谜”，并且它“不容易被推广到其他数学领域或其他学科”。

Trinh 博士表示，他计划将这一系统应用到数学的其他领域乃至更广泛的领域。他希望进一步探索所有类型推理背后的“共同基本原理”。

法国高等师范学院的认知神经科学家Stanislas Dehaene，在基础几何知识领域有着深入的研究兴趣。他对 AlphaGeometry 的性能表现赞不绝口。然而，他提到这个系统在解决问题时，并没有实际“看到”问题的本质——它仅仅是处理了图像的逻辑和数字编码（这些图纸实际上是为了方便人类读者）。Dehaene 博士指出：“系统所操作的圆、线条和三角形，并没有被赋予任何空间感知。”研究人员也认同，引入视觉元素可能会大有裨益。Luong 博士表示，他们计划在一年内利用谷歌的 Gemini——一个能够同时处理文本和图像的“多模态”系统——来实现这一点。

灵魂的解答

去年 12 月，Luong 博士回到了他在越南胡志明市的母校，向他的前导师及国际数学奥林匹克 (I.M.O.) 教练 Le Ba Khanh Trinh 展示了 AlphaGeometry。Lê 博士曾在 1979 年的奥林匹克竞赛中荣获金牌，并因其在几何问题上的优雅解答获得特别奖。他对 AlphaGeometry 的一个证明进行了分析，发现虽然证明引人注目，但却让人感到有些遗憾。Luong 博士回忆说，Lê 博士认为这种解答过于机械化，缺乏他所追求的解决方案中的灵魂与美感。

此前，Trinh 博士还邀请了麻省理工学院的数学博士生、I.M.O.教练和奥林匹克金牌得主 Evan Chen 对 AlphaGeometry 的一些工作进行审核。Chen 先生证实了其计算结果的正确性，并表示他对系统是如何找到这些解答的非常感兴趣。

“我很想知道这台机器是怎样找出这些解法的，”他说道。“不过，说到底，我也很好奇人类是怎样找出解答的。”