数学界迎来AlphaGo时刻：谷歌AI用19秒答完一道IMO几何题，差1分即可摘金

　　近日，谷歌 DeepMind 宣布其人工智能系统在数学解题能力上取得了突破性进展。

　　在 2024 年国际数学奥林匹克竞赛（IMO，International Mathematical Olympiad）的六道题目中，该公司的人工智能系统成功解决了其中的四道，获得了相当于银牌的成绩。

　　这标志着人工智能系统首次在这项全球顶级少年数学家竞赛中达到了奖牌级别的表现。

　　DeepMind开发了两个专门的人工智能系统 AlphaProof 和 AlphaGeometry 2，两者协作拿到了这一成绩。

　　（来源：DeepMind）

　　AlphaProof 解决了两道代数题和一道数论题，其中包括本次比赛中最难的一道题目。而 AlphaGeometry 2 则成功解决了一道几何题，仅仅耗时 19 秒。未能完成的两道题属于组合数学的范畴。

　　这两个人工智能系统的总成绩获得了 42 分中的 28 分，仅差 1 分就达到了金牌的门槛。

　　图丨AI 系统相较于所有人类选手的表现（来源：DeepMind）

　　IMO 作为自 1959 年以来每年举办的重大数学赛事，一直吸引着全球精英学生参与。

　　比赛涵盖代数、组合数学、几何和数论等领域，题目难度极高。近年来，IMO 问题的解决能力已成为评估人工智能系统数学推理能力的重要基准。

　　据 DeepMind介绍，AlphaProof 是一个基于强化学习的系统，它通过生成和验证数百万个证明来自我训练，逐步解决越来越困难的问题。该系统使用形式化语言 Lean 来证明数学陈述。

　　训练数据不足是常见的问题之一，为解决该问题，研究团队设计了一个额外的网络，试图将现有的百万个用自然语言写成的问题翻译成 Lean 语言，而不包含人工编写的答案。

　　图丨AlphaProof强化学习训练循环：形式化网络将大约一百万个非形式化数学问题翻译成形式化数学语言。然后，求解器网络搜索问题的证明或反证，通过AlphaZero算法逐步训练自身以解决更具挑战性的问题（来源：DeepMind）

　　AlphaGeometry 2 是谷歌之前几何解题人工智能模型的升级版本，现在由基于 Gemini 的语言模型驱动。它可以解决与物体运动以及涉及角度、比率和距离的方程式有关的问题。

　　由于它比其前身接受了更多合成数据的训练，因此能够解决更具挑战性的几何问题。

　　在尝试本次 IMO 之前，AlphaGeometry 2 能够解决过去 25 年 IMO 几何问题的 83%，远高于其前身 53% 的成功率。

　　在今年的比赛中，该系统在接收到几何题的形式化版本后仅用 19 秒就找到了解决方法。

　　值得注意的是，人工智能系统解题的过程与人类参赛者有所不同。谷歌首先将 IMO 问题翻译成形式化的数学语言，然后交由人工智能模型处理。

　　而在正式比赛中，人类参赛者需要在两个 4.5 小时的环节中直接面对数学陈述。

　　图丨AI 系统用 19 秒解决的几何题：要求证明∠KIL与∠XPY之和等于180°（来源：DeepMind）

　　尽管取得了令人瞩目的成就，但这项技术仍存在一些局限性。菲尔兹奖得主、著名数学家蒂莫西·高尔斯爵士（Timothy Gowers）指出了几个关键的限制因素。

　　首先，人工智能系统需要比人类参赛者更长的时间来解题，有些问题花费了 60 小时以上，而且人工智能系统的处理速度也比人类大脑快得多。如果给予人类参赛者同样的时间，他们的分数可能会更高。

　　其次，数学题需要人工将其翻译成形式化语言 Lean，然后人工智能模型才能开始工作。

　　虽然人工智能执行了最重要的数学推理，但这个“自动形式化”步骤仍需由人类完成。

　　此外，目前尚不清楚这种技术是否能扩展到其他数学领域，特别是那些训练数据较少的领域。

　　值得注意的是，人工智能系统未能解决两道组合数学问题，这表明它在某些数学领域还有待进步。

　　尽管存在这些限制，但专家们认为这项技术仍有巨大的潜力。高尔斯推测，这样的人工智能系统可能成为有价值的研究工具，能够帮助数学家回答广泛的问题，只要这些问题不太困难。这将极大地推动数学研究的发展。

　　剑桥大学专门研究数学和人工智能的研究员凯蒂·柯林斯（Katie Collins）指出，能够解决复杂数学问题的人工智能系统可能为“人类+人工智能”的协作模式开辟新的道路，帮助数学家解决和发明新类型的问题。

　　这反过来也可能帮助我们更好地理解人类是如何解决数学问题的。

　　谷歌DeepMind 研究副总裁普什米特·科利表示，这是机器学习和人工智能领域的重大进展，迄今为止，还没有哪个系统能以这样的成功率和通用性来解决问题。

　　此外，作为 IMO工作的一部分，DeepMind 还试验了一种基于谷歌 Gemini 和 DeepMind 最新研究的自然语言推理系统，以实现高级问题解决技能。

　　有了该系统后，不仅不用把问题翻译为形式语言，而且它还能够和其他人工智能系统结合使用。DeepMind 还在今年的IMO问题上测试了这种方法，结果显示出巨大的潜力。

　　“我们的团队正在继续探索多种用于推进数学推理的人工智能方法，并计划很快发布有关 AlphaProof的更多技术细节。”DeepMind 在博客中写道。

　　可以预见的是，随着技术的不断进步，我们将会看到更多令人兴奋的人类+人工智能协作，推动数学和人工智能领域的共同发展。

　　参考资料：

　　https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

　　https://arstechnica.com/information-technology/2024/07/google-ai-earns-silver-medal-equivalent-at-international-mathematical-olympiad/

　　https://www.technologyreview.com/2024/07/25/1095315/google-deepminds-ai-systems-can-now-solve-complex-math-problems/

　　运营/排版：何晨龙