谷歌数学AI登Nature：IMO金牌几何水平，定理证明超越吴文俊法
AlphaGo系列数学模型
梦晨 发自 凹非寺
量子位 | 公众号 QbitAI
谷歌DeepMind再发Nature，Alpha系列AI重磅回归，数学水平突飞猛进。
AlphaGeometry，无需人类演示达到IMO金牌选手的几何水平。
有当年AlphaZero无需人类知识学围棋《Mastering the game of Go without human knowledge》的感觉了。
具体来说，30道IMO难度的几何定理证明题，AlphaGeometry做对25道，人类金牌选手平均25.9道，之前SOTA方法（1978年的吴文俊法）做对10道。
IMO金牌得主陈谊廷（Evan Chen）负责评估AI生成的答案，他评价到：
AlphaGeometry的输出令人印象深刻，既可验证又干净。过去的人工智能解决方案偶然性很大，输出有时是正确的，需要人工检查。
AlphaGeometry没有这个弱点，它的解决方案具有机器可验证的结构，并且是人类可读的……它像学生一样使用带有角度和相似三角形的经典几何规则。
除成绩亮眼之外，这项研究中还有三个重点引起业界关注：
- 无需人类演示，也就是只用了AI合成数据训练，延续了AlphaZero自学围棋的方式。
- 大模型结合其他AI方法，与AlphaGo和OpenAI Q*传闻相似。
- 与许多先前方法不同，AlphaGeometry可以生成人类可读的证明过程，且模型和代码都开源。
团队认为，AlphaGeometry提供了一个实现高级推理能力、发现新知识的潜在框架。
这可能有助于推动人工智能的定理证明——被视为构建AGI的关键一步。
另外，量子位在与作者团队交流过程中，打听到了是否真的会让AlphaGeometry去参加一届IMO竞赛，就像当年AlphaGo挑战人类围棋冠军一样。
他们表示正在努力提高系统的能力，还需要让AI能解决几何之外更广泛的数学问题。
AI证明几何也画辅助线
此前AI系统不能很好解决几何问题，卡就卡在缺乏优质训练数据。
人类学习几何可以借助纸和笔，在图像上使用现有知识来发现新的、更复杂的几何属性和关系。
谷歌团队为此用生成了10亿个随机几何对象图，以及其中点和线间的所有关系，最终筛选出1亿不同难度的独特定理和证明，AlphaGeometry在这些数据上完全从头训练。
系统由两个模块组成，相互配合寻找复杂的几何证明。
- 语言模型，预测可用来解决问题的几何结构（也就是添加辅助线）。
- 符号推理引擎，使用逻辑规则推导出结论。
一作Trieu Trinh介绍，AlphaGeometry的运作过程类似人脑分为快与慢两种类型。
也就是诺贝尔经济学奖得主丹尼尔·卡尼曼的畅销书《思考快与慢》中普及的“系统1、系统2”概念。
系统1提供快速、直观的想法，系统2提供更加深思熟虑、理性的决策。
一方面，语言模型擅长识别数据中的模式和关系，可以快速预测潜在有用的辅助结构，但通常缺乏严格推理或解释其决策的能力。
另一方面，符号推理引擎基于形式逻辑并使用明确的规则来得出结论。它们是理性且可解释的，但它们缓慢且不灵活，尤其是在独自处理大型、复杂的问题时。
例如在解决一道IMO 2015年的竞赛题时，蓝色部分为AlphaGeometry的语言模型添加的辅助结构，绿色部分是最终证明的精简版，共有109个步骤。
在做题过程中，AlphaGeometry还发现了2004年IMO竞赛题中一个未使用的前提条件，并因此发现了更广义的定理版本。
不需要O是BC的中点这个条件，就能证明P、B、C共线。
另外研究还发现，对于人类得分最低的3个问题，AlphaGeometry也需要非常长的证明过程和添加非常多的辅助结构才能解决。
但在相对简单的问题上，人类平均得分和AI生成的证明长度之间没有显著相关性 (p = −0.06)。
One More Thing
对于AlphaGeometry与AlphaGo的联系和区别，在与团队交流过程中，谷歌科学家Quoc Le介绍到：
他们都是在一个非常复杂的决策空间中搜索，但AlphaGo的方法更传统（注：神经网络负责模式识别），AlphaGeometry中的神经网络负责建议下一步要采取的行动，指导搜索算法在决策空间中向正确的方向移动。
虽然这次成果随Alpha系列命名，第一单位也是Google DeepMind，但其实作者主要是前谷歌大脑成员。
Quoc Le大神不用过多介绍，一作Trieu Trinh与通讯作者Thang Luong都在谷歌工作了六七年，Thang Luong自己高中时也是IMO选手。
两位华人作者中，何河是纽约大学助理教授。吴宇怀此前参与了谷歌数学大模型Minerva研究，现在已经离开谷歌加入马斯克团队，成为xAI的联合创始人之一。
论文地址：
https://www.nature.com/articles/s41586-023-06747-5
参考链接：
[1]https://www.nature.com/articles/d4186-024-00141-5
[2]https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry
- 不做Sora背后：百度的多模态路线是什么？2024-11-16
- 60%以上低空经济企业上钉钉，钉钉&生态伙伴发布低空行业解决方案2024-11-14
- Claude三巨头回应一切！Opus3.5仍可能发布，5小时视频10万人围观2024-11-12
- 开源版SearchGPT来了，两张3090就可复现，超越Perplexity付费版2024-11-12
相关阅读
谷歌佩奇支持的Kitty Hawk中止Flyer飞车计划 将专注打造Heaviside
据国外媒体报道，谷歌联合创始人拉里·佩奇支持的初创公司Kitty Hawk日前宣布，将中止Flyer飞车计划，专注打造新款飞行汽车Heaviside。
