AlphaGeometry

一个系统，两个部分

AlphaGeometry 是 Google DeepMind 于 2024 年 1 月 17 日公布的一个几何解题 AI 系统，同时配有一篇发表于《自然》（Nature）的论文^[1]。它属于通常所说的「神经符号」（neuro-symbolic）路线：不依赖单一的神经网络，而是把一个神经语言模型和一个符号推演引擎（symbolic deduction engine）配成一对^[1]。两部分各做各的事：语言模型负责证明中看起来像「猜」的那部分——下一步该试什么、该添什么；推演引擎则按形式规则一步步推导，让每一步都被检验，而不只是被预测。这样分工的用意在于，神经部分提供灵活性，符号部分提供确定性。

从零训练，用合成题目

系统是从零开始训练的，没有使用人类演示^[1]。训练数据是 1 亿个难度不一的独特合成样例，其中 900 万个带有额外添加的构造^[1]。也就是说，这些例子由程序生成，而不是从人们写下的证明里收集而来；几何题常常需要添一条原图中没有的辅助线或辅助圆，这部分样例就包含这类添加的构造。

在一个奥赛基准上的成绩

为了衡量进展，团队把 2000 年至 2022 年各届奥赛的几何题汇编成一个包含 30 道题的基准（benchmark），名为 IMO-AG-30^[1]。在这个基准上，AlphaGeometry 在竞赛时限内解出了 30 道题中的 25 道^[1]。此前最好的方法吴氏方法（Wu's method）解出 10 道^[1]。作为参照，人类金牌选手的平均成绩是 25.9 道^[1]。DeepMind 表示，AlphaGeometry 是首个能够达到 2000 年和 2015 年国际数学奥林匹克（IMO）铜牌门槛的 AI 模型^[1]。

开源的代码与模型

系统的代码和模型都已开源^[1]。论文作者包括 Trieu Trinh、Yuhuai Wu、Quoc Le、He He 和 Thang Luong^[1]。

AlphaGeometry 2

改进后的版本 AlphaGeometry 2 在 2024 年国际数学奥林匹克上，收到几何题的机器形式化表述后，19 秒内就解出了该题^[2]。在过去 25 年的历史 IMO 几何题上，它能解决 83%，而前一代是 53%^[2]。

意义

几何证明对机器是一道硬题：给出最终答案只是开始，中间每一步都要有理由。因此解题系统既需要找到有希望的下法，也需要保证找到的东西确实成立。AlphaGeometry 把这两件事接了起来——提议来自语言模型，检验交给推演引擎——在一组精选的奥赛题上把机器带到了接近人类金牌选手的位置^[1]。团队把代码和模型开源，使其他研究者可以复用并检查这套方法^[1]；后来的 AlphaGeometry 2 沿着同一条路线，把可解的历史奥赛几何题比例又提高了一大截^[2]。