2024年1月17日，DeepMind团队在《自然》期刊上发表了一篇名为《无需人类示例即可解决奥数几何问题》（Solving olympiad geometry without human demonstrations）的文章。
该篇文章介绍了DeepMind团队最新的人工智能系统AlphaGeometry。正如论文标题所说的，AlphaGeometry可以自行求解国际奥数难度的平面几何问题。据论文中所说，在对30道奥数几何题的基准测试中，AlphaGeometry在标准奥数时限内解决了25道。相比之下，之前最先进的系统解决了其中10个几何问题。与之对应的，人类金牌得主平均解决了25.9个问题，银牌得主平均解决了22.9个问题，而铜牌得主平均解决了19.3个问题。
一个男孩在写满数学公式的黑板前。视觉中国|图
这是继2016年3月和2017年5月，同样由DeepMind团队研发的AlphaGo，在围棋上接连战胜李世石和柯洁之后，人工智能系统再一次在纯智力竞赛领域，达到人类最顶点选手的水平。也是继2022年ChatGPT引发的新一轮大型语言模型类人工智能系统热潮以来，人工智能系统在求解数学问题领域取得的最惊人的成功。
平面几何的特殊性
与2023年加州理工、英伟达、MIT等机构的学者共同撰写的论文中声称的，面向所有数学问题的人工智能系统Leandojo不同，这次DeepMind发布的人工智能系统，是专门为了解决数学中的平面几何问题而特化的。这一点，从AlphaGeometry的名字，阿尔法几何就能看出来。这是因为，在所有的数学分支当中，平面几何是极为特殊的。
现代数学的一大特征就是公理化。所谓公理化数学，首先要约定几条“不可辩驳”的公理，或者说公设。然后由此作为基础，通过逻辑和数学的推理过程，来推演引理、定理和推论，从而推演出整个数学体系。只要承认公理，那么所有的推导结果必然自动为真。在过去的一百余年时间里，数学家们逐步完成了各个数学分支的公理化。例如，概率论的公理化就是在二十世纪三十年代由苏联数学家柯尔莫哥洛夫完成的。
平面几何的公理化则发生在两千多年前的古希腊。早在公元前300多年，欧几里得就在《几何原本》中给出了平面几何的五条公理，并以此为基础，严格证明了数十条平面几何的定理。正因为此，平面几何也被称为欧几里得几何。
极早地完成公理化，使得欧几里得几何在古希腊时期就获得了巨大的进展。而当一个数学分支的理论框架搭建完毕，能够被解决的问题都被解决之后，对于数学家们来说，这个分支也就失去了继续被研究的价值。因此，过早地发展成熟，也使得欧几里得几何成为了第一个“死掉”的数学分支。
但是，就像死掉的拉丁语因为不再变化，而成为生物学中物种命名的唯一指定语言一样，死掉的欧几里得几何，也在数学的其他方面，发挥了深远而长久的作用。
因为欧几里得几何直观易懂的五条公理体系，和清晰简明的命题推理过程，使得欧几里得几何成为了学习数学公理和证明方式的最佳模板。正因为此，欧几里得几何一直都是义务教育阶段初中数学课程当中非常重要的一部分。
另外一方面，同样因为欧几里得几何清晰的推理过程，以及相关的内容在很早就有了非常透彻的研究，这也就使得欧几里得几何成为了数学家们的一块极佳的“试验田”。在数学史上，很多数学理论、工具和观念的新发展，都会先在欧几里得几何上进行实验和推演。
代数化、坐标化、符号化与机械化
在历史上，欧几里得几何第一次完全的“改头换面”来自于笛卡尔。通过引入坐标系以及线段的运算概念，笛卡尔将平面上的点对应于一个有序的实数对，而直线、圆之类的几何图形，则可以由一个特定的代数关系式来表示。在他的著作《几何》中，笛卡尔向世人证明，几何问题可以归结成代数问题。更进一步地，可以通过代数运算来发现、证明几何性质。由此，笛卡尔成功地将当时完全分开的代数和几何学整合，创立了后来被叫做解析几何的数学分支。
一百多年前，希尔伯特发起的“形式主义纲领”，同样始于欧几里得几何。
希尔伯特想要建立的形式化的数学公理体系应该满足三个条件。即：完备性：可以发现所有数学真命题；自洽性：数学内部不存在矛盾；可决定性：能够判断每一个数学命题的真伪。
按照形式主义的要求，首先应当有一个只有有限个符号的符号表，用这些符号来代替讨论数学问题的自然语言。用这些符号，就可以像用字母拼写单词一样地去“拼写”出有意义的命题公式，即：“合式公式”。在指定了相应的命题作为公理之后，数学中逻辑推理的过程就可以用符号推演代替语言，形式地表达为符号串构成的“单词”间的对比。由此，数学推理的过程就完全变成了“形式化”的符号操作了。
在希尔伯特这样的形式主义数学家看来，所有已经发现和尚未发现的数学定理，都可以写成这样或长或短的一串符号。
虽然后来哥德尔不完备定理证明了，对于整个数学体系而言，希尔伯特的这一宏伟图景是无法实现的。但是仅限于欧几里得几何这一数学分支的话，希尔伯特的形式化公理体系是完全成立的。这是因为欧几里得几何公理体系不包含初等数论，这一哥德尔不完备定理的成立条件，因而欧几里得几何公理体系是完备的。
被希尔伯特形式化之后的欧几里得几何，则被称为希尔伯特几何。
上世纪七十年代，吴文俊用这种代数化和符号化的方法，将欧几里得几何与计算机科学相结合，开创了机器几何定理证明的方向，推动了数学机械化自动证明的发展。这套被数学界称为“吴方法”的机械化自动证明，用复杂的形式、符号计算推演来代替抽象的数学推理，从而用计算机来辅助数学家去发现自然结构、获取数学真理。
基于吴方法的自动几何定理证明，首先需要将几何问题代数化，将命题中给定的几何条件和几何结论翻译成多项式方程，然后用特定的计算机算法去计算这些多项式，最终判定几何命题是否成立。
因为欧几里得几何是完备的，所有欧几里得几何中的命题，都可以用符号化的形式语言，在有限的步骤内证明或者证伪。因此，理论上来说，吴文俊发明的吴方法，完全可以证明所有欧几里得几何的定理。
这里所谓的“理论上”，就像是理论上来说，围棋按照规则只有有限多种下法，因此可以通过穷尽所有的步骤，来找到必胜策略一样。在实际操作中，因为算力和时间的限制，吴方法也只能解决某些几何问题。
尽管如此，在近几年的人工智能热潮之前，吴方法，及其相关改进版本，仍然是机器证明欧几里得几何命题最为行之有效的方法。本文开头提到的，用来和AlphaGeometry比较的，“解决了其中10个几何问题”的“之前最先进的系统”，就是吴方法。
AlphaGeometry做了什么
AlphaGeometry相较于“之前最先进的系统”的巨大提升，代表了DeepMind之前包括AlphaGo在内的技术积累，与当下大型语言模型结合之后，在欧几里得几何这个特定的数学分支下，所展现出的惊人效果。
AlphaGeometry是个神经符号系统，主要包括一个神经语言模型（大语言模型）和一个符号演绎引擎。
在这两部分当中，大型语言模型擅长识别数据中的一般模式和关系，因此它们可以快速预测可能有用的结构。但通常情况下，大型语言模型缺乏严格推理或解释的能力。这也是之前包括ChatGPT和GPT-4等大型语言模型在数学能力方面表现难如人意的原因。
在AlphaGeometry这里，大型语言模型的这一弱点被另外一部分，即符号演绎引擎所解决。符号演绎引擎基于形式逻辑，并使用明确的规则来得出结论。这两部分协同工作，类似于卡尼曼 《思考，快和慢》一书中提到的系统1和系统2的概念，系统1提供快速、“直观”的想法，而系统2则提供“更深思熟虑、更理性的决策”的想法。
在大型语言模型的训练上，DeepMind为AlphaGeometry搭建了包含1.51亿参数的模型。在“命题、结论、证明”上进行了预训练，合成了5亿个几何证明，其中有900万个带辅助线的题目。
通过这种训练，DeepMind成功地让AlphaGeometry的大型语言模型学会了几何证明中最为重要的技巧：添加和使用辅助线。
AlphaGeometry能够对每一个几何图形，穷举该图形能够得到的命题。并且能够反过来回溯每个命题所包含的几何图形的集合。在解题过程中，AlphaGeometry会搜寻题目条件中的几何图形所能够得到的命题，以及包含题目所要证明的结论命题的几何图形的集合。通过比对这两个集合中集合对象的差异，找到辅助线的位置。
这是数学的未来吗
在惊异于AlphaGeometry的出色表现之余，我们不由得会想要知道，AlphaGeometry的这种模式，是数学发展的未来么？或者说，在可以预见的时间内，人工智能能否独立进行数学研究，并且做出有价值的结果？
虽然AlphaGeometry体现了现阶段大型语言模型“足够好的数据就意味着足够好的智能”，这一用大量参数、大样本集解决问题的暴力美学的特征。但是，AlphaGeometry本身极度依赖欧几里得几何本身的特点。而正如前文所说，欧几里得几何，在数学当中是极为特殊的一个分支。AlphaGeometry的这一做法能否推广到其他数学分支，还是一个未知数。
而且，正如杨立昆等人多次提到的，现阶段大型语言模型对于数据的利用率相当低下。单纯为了求解几何问题，AlphaGeometry的参数和训练集，就来到了如此量级。因此，即使AlphaGeometry的做法能够以某种方式扩展到一般的数学问题上，面对各种类型的数学问题，这样的人工智能系统需要的参数和训练集数量，在现阶段的实际操作层面也很可能是无法实现的。
尽管如此，AlphaGeometry所展示的，人工智能不断增长的逻辑推理能力以及发现和验证新知识的能力，仍然足够让人印象深刻。
正如AlphaGeometry的作者之一在社交媒体上所说的：“目前组合数学的形式化还处于初期，为不同领域构建强大的符号引擎需要深入的领域专业知识。我们考虑将该框架应用于更广泛的范围，作为未来的工作，并期待进一步的创新来应对这些挑战。”
就文章所展示的内容来看，AlphaGeometry的思路很直接，但是其中各种细节上的技术难点，和解决这些难点的做法，都非常得不平凡。这充分体现了作者们极强的能力和毅力。因此，现在就对AlphaGeometry下一个定论显然还为时尚早，但是完成AlphaGeometry这项工作所呈现出的一切，让我们有理由期待作者未来的工作。
南方周末特约撰稿 左力
责编 朱力远
