AlphaGeometry:不靠人类证明解奥赛几何

快速答案

AlphaGeometry 来自 Google DeepMind 与纽约大学,在 30 道近年 IMO 级几何题上解出 25 道,而此前最强的自动方法只解出 10 道,人类金牌选手平均能解 25.9 道。它做到这点没有用过任何一条人类写的证明:整个系统完全靠 1 亿条合成定理及其机器生成的证明训练出来。

几何证明为什么难倒 AI

奥赛几何对机器来说位置很尴尬。推导本身是严格的,但取胜的关键往往是一步「辅助构造」——在原图之外画一个新点、新线或新圆。这一步创造性动作能让纯推导永远啃不动的题瞬间瓦解,而可能的构造空间几乎是无穷大的。

两种常规思路在这里都会失手。符号证明器能机械地推出所有正确结论,却没有判断该试哪个构造的「品味」,于是搜索爆炸;在文本上训练的语言模型很流畅,却会编出根本不成立的步骤。更隐蔽也更棘手的障碍是数据:几乎不存在大规模、机器可校验格式的人类几何证明语料,所以「模仿专家」这套老办法根本没有可模仿的对象。

一个神经符号循环

AlphaGeometry 把任务拆给两个互补的部件。符号演绎引擎会穷尽地推出当前图形能导出的一切结论——又快,又绝不出错。当推导卡住时,一个 Transformer 语言模型提出一条辅助构造加进图里,引擎再在扩展后的图上重跑。循环往复,直到目标被证明或预算耗尽。

这种分工才是要害。语言模型从不需要给出正确证明,它只需要提示「该往哪看」。它促成的每一步仍由符号引擎校验,所以一个糟糕的建议只是浪费搜索时间,绝不会引入无效证明。神经直觉负责挑构造,符号逻辑负责担保正确。

用合成定理训练

既然人类证明数据几乎不存在,作者就自己造。他们随机采样几何前提,让符号引擎推出全部结论,再把定理连同证明它的推导步骤读出来——得到约 1 亿条无需人工标注的样本。一个关键技巧把辅助构造找了回来:当某条证明依赖一个不在原始前提里的点时,就把这个点挪进证明,变成模型必须学会提出的构造。这正是一个只靠机器数据训练的系统,如何学会几何学家所倚重的那一步真正创造性动作。

关键结果

在 2000–2022 年间 30 道奥赛级几何题的测试集上,AlphaGeometry 解出 25 道。此前最强的自动几何方法(吴方法)解出 10 道,一个无引导的强符号基线解出 18 道;人类 IMO 金牌选手平均能解 25.9 道。在一位前 IMO 奖牌得主的评估下,它的输出被判定为有效、人类可读的证明,而不是不透明的坐标硬算——其中一题它给出的解法比官方答案更一般。要害在于:提升明确来自那个提构造的语言模型,单靠符号引擎只能停在 18 道。

局限与存疑

AlphaGeometry 很窄。它只处理能用其形式语言表达的欧氏平面几何,不碰组合、数论和不等式,而这些恰好占了 IMO 试卷的大部分。题目必须先被人工翻译成它的形式表示,所以它并不是端到端读竞赛 PDF。有些证明比优雅的人类写法更长、更机械,而符号引擎的覆盖范围划定了什么能被证明的上限——一旦某个事实落在它的规则集之外,再多神经引导也没用。

真正的悬念是通用性。这套配方——合成可校验的数据,让模型提出创造性的跳跃,再用符号引擎逐步检查——之所以诱人,正因为它同时绕开了幻觉和数据荒。它能否迁移到没有几何这种干净、完全可判定推导的领域,尚未被证明,而这才是值得盯住的地方,而非那个几何分数本身。

常见问题

AlphaGeometry 是怎么解几何题的?

它在两者间交替:符号演绎引擎推出当前图形的全部结论,语言模型在推导卡住时提出一条新的辅助构造。引擎校验每一步,所以模型只需要好的直觉,不需要保证正确。

AlphaGeometry 用人类证明训练过吗?

没有。它从零开始,在约 1 亿条合成定理和机器生成的证明上训练,不用任何人类示例。辅助构造也是从这些合成证明本身里反推出来的。

AlphaGeometry 和人类比有多强?

在 30 道奥赛几何题上它解出 25 道,人类 IMO 金牌选手平均 25.9 道,此前最佳自动方法只有 10 道——所以在这一小块上它接近但尚未超过金牌水平。

AlphaGeometry 做不到什么?

它只限于用其形式语言表述的欧氏平面几何,不解组合、数论或不等式题,而且需要题目被预先翻译成它的形式输入,不能直接读原始竞赛题面。

AlphaGeometry 的启示不是「AI 会做几何」,而是合成数据加一个校验器,能教会模型搜索引擎猜不出的那一步创造性跳跃。完整结果见 Nature。