

数学界迎来AlphaGo时刻：谷歌AI用19秒答完一道IMO几何题

汉斯出版社

2024-08-05

导读：关注汉斯出版社公众号即可获取最新论文咨讯！

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

在2024年国际数学奥林匹克竞赛（IMO，International Mathematical Olympiad）的六道题目中，该公司的人工智能系统成功解决了其中的四道，获得了相当于银牌的成绩。这标志着人工智能系统首次在这项全球顶级少年数学家竞赛中达到了奖牌级别的表现。

DeepMind 开发了两个专门的人工智能系统 AlphaProof 和 AlphaGeometry 2，两者协作拿到了这一成绩。AlphaProof 解决了两道代数题和一道数论题，其中包括本次比赛中最难的一道题目。而 AlphaGeometry 2 则成功解决了一道几何题，仅仅耗时 19 秒。未能完成的两道题属于组合数学的范畴。这两个人工智能系统的总成绩获得了 42 分中的 28 分，仅差 1 分就达到了金牌的门槛。

据 DeepMind 介绍，AlphaProof 是一个基于强化学习的系统，它通过生成和验证数百万个证明来自我训练，逐步解决越来越困难的问题。该系统使用形式化语言 Lean 来证明数学陈述。训练数据不足是常见的问题之一，为解决该问题，研究团队设计了一个额外的网络，试图将现有的百万个用自然语言写成的问题翻译成 Lean 语言，而不包含人工编写的答案。

AlphaGeometry 2 是谷歌之前几何解题人工智能模型的升级版本，现在由基于 Gemini 的语言模型驱动。它可以解决与物体运动以及涉及角度、比率和距离的方程式有关的问题。由于它比其前身接受了更多合成数据的训练，因此能够解决更具挑战性的几何问题。

值得注意的是，人工智能系统解题的过程与人类参赛者有所不同。谷歌首先将 IMO 问题翻译成形式化的数学语言，然后交由人工智能模型处理。而在正式比赛中，人类参赛者需要在两个 4.5 小时的环节中直接面对数学陈述。

尽管取得了令人瞩目的成就，但这项技术仍存在一些局限性。菲尔兹奖得主、著名数学家蒂莫西·高尔斯爵士（Timothy Gowers）指出了几个关键的限制因素。首先，人工智能系统需要比人类参赛者更长的时间来解题，有些问题花费了 60 小时以上，而且人工智能系统的处理速度也比人类大脑快得多。如果给予人类参赛者同样的时间，他们的分数可能会更高。其次，数学题需要人工将其翻译成形式化语言 Lean，然后人工智能模型才能开始工作。

虽然人工智能执行了最重要的数学推理，但这个“自动形式化”步骤仍需由人类完成。此外，目前尚不清楚这种技术是否能扩展到其他数学领域，特别是那些训练数据较少的领域。

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

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