AlphaGeometry 解出奥赛几何题

背景

国际数学奥林匹克（International Mathematical Olympiad，IMO）是最广为人知的面向大学前学生的数学竞赛。它的题目设计成原则上用初等工具就能解出，但要找到那条论证路径很难，每届只有一部分选手能拿到奖牌。几何一直是自动推理最喜欢瞄准的领域：一道几何题通常给出一个图形和一个待证结论，而解答是一串逻辑步骤，其中常常要添一条辅助线或一个辅助圆，剩下的部分才顺下来。严格的逻辑加上一步创造性，正是这种混合使几何成为检验机器推理的好场地。

发生了什么

2024 年 1 月 17 日，Google DeepMind 公布 AlphaGeometry，并在《自然》（Nature）上发表了描述该系统的论文 ^[1]。配合公布的文章由 Trieu Trinh 和 Thang Luong 撰写 ^[1]。DeepMind 给出的说法很具体：这是第一个能够通过 2000 年和 2015 年国际数学奥林匹克铜牌分数线的 AI 模型 ^[1]。

它是怎么做的

AlphaGeometry 把一个语言模型与一个符号推演（symbolic deduction）引擎配成一对 ^[1]。两个部件干的是不同的活，整个设计就建立在这个分工上。语言模型在大量文本和其他数据上训练过，擅长提出看似合理的下一步，但它本身不证明任何东西：它的输出是建议，不是保证。符号推演引擎则相反，它对已经掌握的命题套用形式规则，推出必然成立的新命题，但它只能处理手上已有的东西，也没有「哪一步值得试」的判断力。两者合起来，语言模型提供候选步骤，推演引擎负责检验并继续往下推，于是最终得到的是证明而不是猜测 ^[1]。

结果

DeepMind 使用的基准由 30 道奥赛几何题组成，题目取自 2000 年至 2022 年间的奥林匹克竞赛 ^[1]。AlphaGeometry 在规定时间内解出了其中的 25 道 ^[1]。最自然的参照是人：人类金牌得主平均解出同样这些题目中的 25.9 道 ^[1]。

这两个数字挨得很近。需要把这一比较说清楚：它说明了什么，没说明什么。AlphaGeometry 的 25 道低于人类平均的 25.9 道，也就是说，在这套题上它没有超过最强的人类解题者。这个结果真正确立的是：在一类范围很窄、定义清楚的问题上，一个机器系统达到了与专业选手大致相同的区间，其中符号引擎负责检验，学习出来的模型负责提供想法 ^[1]。

为什么重要

这个结果的意义与其说在分数，不如说在它示范了一种搭建系统的方式。神经模型灵活，但在长链条的精确推理上不可靠；符号引擎精确，但僵硬。AlphaGeometry 的贡献是让两者互相补上对方的短板，而且是在一个正确性可以被机械检验的领域里做到的 ^[1]。这也是 DeepMind 用奥赛奖牌分数线、而不是用一个通用基准来表述结果的原因：奖牌线是外界熟悉的难度标尺，在 2000 年和 2015 年的条件下通过它，让这个公布有了一个不需要了解模型内部也能理解的判据 ^[1]。

也要看清它的范围。基准是几何，30 道题；比较对象只有一个人手平均值，即人类金牌得主平均解出的题数 ^[1]。几何是奥赛数学中图形与形式推演结合得最自然的部分；竞赛的其他领域，以及竞赛形式之外的问题，都不在这些数字覆盖之内。25 与 25.9 之间不到一道题的差距也小到应当读作「处在同一区间」，而不是排名 ^[1]。这次公布确立的是：语言模型与符号推演引擎的组合可以被推进到奥赛级几何，而且结果可以用一种参加过这类竞赛的人自己能判断的形式——奖牌分数线——说出来 ^[1]。