AlphaGeometry 如何结合逻辑证明与创造性作图

2024 年 1 月，Google DeepMind 发布了 AlphaGeometry，这套系统能够解决国际数学奥林匹克竞赛，也就是 IMO 的几何题。这是面向高中生的最高级别国际数学竞赛，100 多个国家各自通过复杂的层层选拔，派出 6 名青少年参赛。在包含 30 道几何题的测试集上，AlphaGeometry 解出了 25 道，超过了银牌选手对应的表现。

对我来说，最令人惊讶的是 AI 登场之前的成果。基于逻辑和方程求解的方法，就已经能处理相当多的这类问题。但它们最终撞上了一堵墙：有些题目，单靠这些逻辑机制无法解决。DeepMind 团队没有让 AI 包办一切，而是把这些机制与一个通过学习获得能力的组件结合起来。我想讲清楚这两部分，先从不用 AI 的系统能做到什么说起。

我们的任务是造一个能解 IMO 几何题的机器人，而且额外加一条限制：不准使用 AI。几何里有个很实用的秘密，只要掌握几个关键事实，就能走得出人意料地远。两条直线相交，对顶角相等；一条截线穿过两条平行线，Z 字形内部的内错角相等。只要接连应用这两个事实，就已经能证明图中一个并不显然的结论。

现在想象一下，如果起点是 10 条、50 条，甚至 100 条事实呢？这些事实以不同方式组合，可以证明的定理就会不断增多。2000 年 10 月发表的一篇论文，正是采用了这种方法，建立了一个包含 75 条几何规则的数据库。有些规则很基础，就像刚刚用过的那些；另一些则更复杂。反复应用这些规则，研究者就能解出一些非常难的几何题。

计算机还需要一种表示几何题的方法。一种选择是给所有元素设定坐标，写出具体方程，但这样很麻烦。另一种选择是 Lean 这样的定理证明语言。Lean 在代数、不等式等领域很强大，不过这里介绍的方法采用了更专门的语言，专为欧氏几何设计。就本次介绍所及，我还不知道它除了研究论文中的描述之外，是否有正式名称。

以“两边相等的三角形有两个相等的角”为例。在这套几何语言里，我们声明 A、B、C 三个点，给出 AB = AC，并把目标设定为角 ABC 等于角 BCA。研究者把这种方法称为演绎数据库，简称 DD。数据库提供起始事实，再通过演绎产生更多结论。

在包含 30 道 IMO 几何题的测试集上，DD 解出了 7 道。可以从两个角度看这个结果：30 道题答对 7 道，远称不上出色的奥数成绩；但这些题非常难，单靠反复应用几何规则，哪怕解出一道，也足以令人惊叹。在断定只有 AI 才能进一步提升之前，我们应该先解决一个基本局限：DD 不会解方程。

泰勒斯定理是个简单例子：圆的直径所对的圆周角是直角。证明时，把圆周上的第三个点与圆心连接起来。这样得到的三条半径长度相等，所以两个较小的三角形都是等腰三角形。它们各自相等的底角可以分别记作 α 和 β。大三角形内角和是 180°，于是得到 2α + 2β = 180°。

把这个方程除以 2，得到 α + β = 90°。这两个角加起来就是 B 点处的角，证明就完成了。对配备线性代数能力的计算机来说，最后这一步代数变换很简单，但演绎数据库恰恰缺少这项能力。DeepMind 的研究者加入了一个叫作代数推理的模块，简称 AR，用来求解线性方程组。

现在我们有了两个模块：DD 应用一组写死的几何规则，AR 求解由此产生的方程。系统让它们交替运行：先运行 DD，直到演绎无法再取得进展；再运行 AR，直到它也停滞，然后回到 DD。如此反复，直到证明目标命题，或者时间耗尽。这套组合程序叫作 DD + AR。

论文中的一个例子是，几何演绎先产生两个关系，再由代数推理求解对应的方程。基准测试展示了这种组合的价值：单独使用 DD，在 30 道题中解出 7 道；DD + AR 则解出 14 道。再加入人工编写的启发式规则，增加到 18 道，接近铜牌水平。我觉得，主要靠穷举的方法，竟然能在 IMO 几何这样困难的问题上走这么远，实在了不起。

既然不用 AI 已经能做到这些，为什么还要加入它？剩下的弱点是辅助作图。解决许多几何题，必须画出原图没有的额外线段或图形。现有图形可能包含了陈述题目所需的一切，却恰恰缺少能让证明成立的那笔辅助作图。

以三角形内角和为 180° 这个定理为例。在三角形的顶部和底部画平行线。根据内错角相等，可以把一个角标为 α，另一个标为 β，再把剩下的角称为 γ。顶部直线上的三个角满足 α + γ + β = 180°。它们也正是三角形的三个角，因此结论成立。

关键的一步是画出那些线。之后，用熟悉的事实就能完成证明。这也是几何有趣的原因之一：恰到好处的额外想法，仿佛凭空冒出来。一道 IMO 题可能需要多次这样的辅助作图。对机器来说，这意味着每一步都要面对无穷多种可能的添加方式，而纯演绎引擎并不擅长搜索这种空间。

DeepMind 团队构建了一个语言模型，只负责一件事：提出辅助作图。输入包括题目陈述和截至当前已经生成的证明步骤。虽然我用英语描述它们，系统实际接收的，是那套专用几何语言。模型输出的是一笔辅助作图，比如添加到图中的新点或新图形。

完整的 AlphaGeometry 循环，首先把题目交给语言模型，获得一个辅助作图建议。扩充后的图形进入 DD + AR，由它尽可能推导更多结论。这些推论再回到语言模型，让它提出下一笔辅助作图。如此反复，在新想法与逻辑后果之间交替，直到解出题目或时间耗尽。

可以把这对搭档想象成一个创造型大脑和一个逻辑型大脑。语言模型想出一个可能有用的补充，DD + AR 则用已知规则和方程确定它能推出什么。随后，模型再提供一个想法，逻辑引擎继续推导。学习组件指引搜索方向，符号组件完成推理。

这还留下一个大问题：语言模型的训练数据从哪里来？已经公开的 IMO 几何题及其解答，数量不足以直接训练这样的模型。AlphaGeometry 团队绕开了这个瓶颈，自己生成样本。先随机绘制点和线，再让 DD + AR 从图形中尽可能推导出所有结论。

假设这些推导证明了三角形内角和为 180°。我们就可以倒过来，把图中的部分线条擦掉。剩下的图形便定义了一道题：给定这个三角形，证明它的内角和。要解题，就得把擦去的线重新画出来，作为辅助作图。重复这个过程，就能把随机图形及其推论转化为训练题，而且每道题所需的作图步骤都是已知的。

研究者生成了数亿个合成证明样本，其中 900 万个至少需要一次辅助作图。有些生成的图形极其复杂，这里介绍的最长合成证明包含 247 个步骤，使用了两次辅助作图。这些样本提供了训练语言模型所需的数据。

性能提升的过程令人瞩目：DD 在 30 道题中解出 7 道，DD + AR 解出 14 道，加入人工编写启发式规则的版本解出 18 道。而将 DD + AR 与经过训练、包括微调的语言模型结合，成绩提高到 25 道。学习组件帮助符号引擎找到了它独自无法发现的证明。

对我来说，令人兴奋的远不止三角形。AlphaGeometry 把创造性的建议与逻辑推理结合起来。人类在科学、医学和工程中解决问题时，也常常采用这种合作方式。这套系统本身并不是为解决那些领域的问题而设计的，但它让我们看到一种机器可能采用的通用策略：想出一个有用的点子，推演它的后果，然后继续。

结尾的介绍说明，这是 3Blue1Brown 夏季客座视频系列的第二期，由 Aleph0 的创作者制作。推荐这个频道的理由是，它能用简洁而充实的内容讲清高等数学。