陶哲轩点评谷歌AlphaProof：AI在数学竞赛中展现「超凡智慧」

IMO 2024 中六个问题的每一个问题满分为 7 分，总分最高 42 分。DeepMind 的系统最终得分为 28 分，意味着解决的 4 个问题都获得了满分 —— 相当于银牌类别的最高分。

DeepMind 文章连接：https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

常用 AI 辅助证明的数学家陶哲轩近期正处在出差的忙碌中，对问题求解引擎 AlphaProof 和 AlphaGeometry2 还未完全消化。但他在自己的博客上对 DeepMind 的 AI 系统参加 IMO 竞赛这件事表达了自己的看法。

陶哲轩谈到，这是一项非常伟大的工作， 再次改变了我们对哪些基准挑战可以通过 AI 辅助或完全自主的方法实现的期望。 

例如，IMO 级别的几何问题现在对于专用的 AI 工具来说已基本解决。现在看来，通过强化学习过程可以找到形式化证明的 IMO 问题至少在某种程度上可以被 AI 攻克。虽然目前每个问题需要相当大的计算量，并且在形式化方面需要人类的帮助。

在陶哲轩看来，这种方法还有一些「buff 加成」，它能使形式化数学更容易自动化，这反过来可能会促进包含形式化成分的数学研究方法。如果更公开地共享由此产生的形式证明数据库，它可能是一个有用的资源。 

这种方法（更多地基于强化学习而非大型语言模型，有点类似 AlphaGo 的精神，且强调整体方法）非常聪明，事后来看很有道理。正如「AI 效应」所言，一旦解释清楚，它不会给人一种展示人类智能的感觉；但它仍然是我们 AI 辅助问题解决工具集能力的扩展。

「AI 效应」是指当人工智能技术取得进展或解决问题时，人们往往会认为这些成就并不是真正的人工智能或者不具备真正的智能。换句话说，一旦某项技术被理解或普及，它就不再被认为是智能的。这种现象表明，人们对 “智能” 的定义和期望会随着技术的进步而不断提高。 

他在最新博客中表示，DeepMind 的这些新工具无法与最近赢得 AIMO 进步奖的 NuminaMath 模型直接比较。NuminaMath 模型完全自动化且资源效率高出数个数量级，并且采用了完全不同的方法（使用大型语言模型生成 Python 代码，以蛮力解决区域竞赛级别的数值答案问题）。这个模型也是完全开源的。这也是非常不错的工作，展示了尝试使用 AI 来辅助或自动化数学问题解决过程的不同部分的多维挑战。

其实 DeepMind 在数学推理方面有着不懈的努力。在今年年初，它的人工智能算法就已经在数学奥林匹克竞赛（IMO）上取得了重大成绩突破。论文《Solving olympiad geometry without human demonstrations》向世人介绍了 AlphaGeometry，还登上了国际权威期刊《自然》杂志。专家表示，这是人工智能朝着具有人类推理能力方向迈进的重要一步。

论文链接：https://www.nature.com/articles/s41586-023-06747-5

未来 DeepMind 还将带给我们怎样的惊喜，我们拭目以待。