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

在奥数问题面前，AI 的「智商」往往不太够用。不过，这已经是过去式了。谷歌 DeepMind 用 AI 做出了今年国际数学奥林匹克竞赛 IMO 的真题，并且距拿金牌仅一步之遥。对于 AI 来说，奥数不再是问题了。IMO 2024 中六个问题的每一个问题满分为 7 分，总分最高 42 分。DeepMind 的系统最终得分为 28 分，意味着解决的 4 个问题都获得了满分 —— 相当于银牌类别的最高分。

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

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

   

   陶哲轩谈到
3. 这是一项非常伟大的工作，再次改变了我们对 AI 辅助或完全自主方法实现基准挑战期望。
4. 例如，IMO 级的几何问题对于专用的 AI 工具来说已基本解决，形式化证明的 IMO 问题至少在某种程度上可以通过强化学习过程被 AI 攻克，尽管目前每个问题需要相当大的计算量，并在形式化方面需要人类的帮助。
5. 陶哲轩认为，这种方法还可以自动化形式化数学，从而可能促进包含形式化成分的数学研究方法。如果更公开地共享由此产生的形式证明数据库，它可能是一个有用的资源。
6. 这种方法（基于强化学习，类似于 AlphaGo 的精神，强调整体方法）非常聪明，事后看来很有道理。正如「AI 效应」所言，一旦解释清楚，它不会给人一种展示人类智能的感觉；但它仍然是我们 AI 辅助问题解决工具集能力的扩展。

   

   「AI 效应」

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

NuminaMath 模型

本月月初，陶哲轩在自己的博客中发布 AI 数学奥林匹克竞赛（AIMO 进步奖） 的初步成绩已公布的消息。其中，获得第一名的是 Numina 的团队。

NuminaMath 模型完全自动化且资源效率高出数个数量级，并且采用了完全不同的方法（使用大型语言模型生成 Python 代码，以蛮力解决区域竞赛级别的数值答案问题）。这个模型也是完全开源的。

DeepMind 的数学推理研究

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

论文链接：https://www.nature.com/articles/s41586-023-06747-5未来 DeepMind 还将带给我们怎样的惊喜，我们拭目以待。参考链接：https://mathstodon.xyz/@tao/112850716240504978

以上是陶哲轩点评谷歌AlphaProof：AI在数学竞赛中展现「超凡智慧」的详细内容。更多信息请关注PHP中文网其他相关文章！