共计 1281 个字符，预计需要花费 4 分钟才能阅读完成。
周四，谷歌 DeepMind 宣布，名为 AlphaProof 和 AlphaGeometry 2 的 AI 系统解决了今年国际数学奥林匹克竞赛（IMO）的六道题目中的四道，获得了相当于银牌的成绩。这是 AI 首次在享有盛誉的数学竞赛中达到这一水平的表现。
据谷歌称，AlphaProof 使用强化学习来证明 Lean 形式语言中的数学陈述。该系统通过生成和验证数百万个证明来自我训练，逐步解决更困难的问题。同时，AlphaGeometry 2 是谷歌先前几何解决 AI 模型的升级版本，现在由基于 Gemini 的语言模型驱动，该模型在更多数据上进行了训练。
著名数学家 Sir Timothy Gowers 和 Dr. Joseph Myers 根据 IMO 官方规则对 AI 模型的解决方案进行了评分。谷歌报告称，其综合系统获得了 42 分中的 28 分，仅略低于 29 分的金牌门槛。这包括在比赛中最难的问题上获得满分，据谷歌称，今年只有五名人类选手解决了这个问题。
自 1959 年以来每年举办的 IMO，将精英预科数学家与代数、组合学、几何和数论中的极其困难问题相对抗。IMO 问题的表现已成为评估 AI 系统数学推理能力的一个公认基准。
据谷歌称，AlphaProof 解决了两道代数问题和一道数论问题，而 AlphaGeometry 2 则解决了几何问题。该 AI 模型未能解决两道组合学问题。谷歌声称其系统在几分钟内解决了一道问题，而其他问题则耗时长达三天。
谷歌表示，首先将 IMO 问题翻译成其 AI 模型处理的形式数学语言。这一步骤与官方竞赛不同，在官方竞赛里，人类选手直接在两个 4.5 小时的时段内处理问题陈述。
据谷歌报告，在今年的竞赛之前，AlphaGeometry 2 可以解决过去 25 年 IMO 历史几何问题的 83%，而其前身成功率仅为 53%。该公司声称，新系统在接收到形式化版本后 19 秒内解决了今年的几何问题。
尽管谷歌宣称，Sir Timothy Gowers 在 X 上发布的帖子中对谷歌 DeepMind 模型提出了更为细致的观点。尽管承认这一成就“远超自动定理证明器之前的水平”，Gowers 指出了几个关键的限制条件。
“主要的限制是程序需要比人类竞争者更长的时间——对于某些问题超过 60 小时——当然，处理速度远超普通人类大脑，”Gowers 写道。“如果允许人类竞争者每道问题有那样的时间，他们无疑会得分更高。”
Gowers 还指出，在 AI 模型开始工作之前，人类手动将问题翻译成形式语言 Lean。他强调，尽管 AI 进行了核心的数学推理，但这一“自动化形式化”步骤是由人类完成的。
关于对数学研究的更广泛影响，Gowers 表示不确定。“我们是否即将使数学家变得多余？很难说。我猜我们还需要一两次突破，”他写道。他指出，系统的长时间处理表明它并未“解决数学问题”，但承认“当它运行时，显然有一些有趣的事情正在发生。”
尽管存在这些局限性，Gowers 推测这样的 AI 系统可能成为有价值的研究工具。“因此，我们可能接近拥有一个程序，使数学家能够得到广泛问题的答案，只要这些问题不是太困难——那些在几个小时内可以解决的问题。这将作为一个研究工具非常有用，即使它本身不能解决开放问题。”
