1.19‍‍‍‍
知识分子
The Intellectual
图源：Freepik
撰文丨张天祁
责编 | 李珊珊
●                  ●                   ●
谷歌DeepMind旗下的AI在数学上取得了突破，1月17日Google DeepMind参与的研究团队在Nature上发文，宣布旗下AI系统在无需人类提示的情况下，攻克了国际数学奥林匹克（IMO）题目。这个名叫AlphaGeometry的模型，在30道IMO几何题中做出了25道。
人类金牌选手平均能够在30道IMO几何题目中做出25.9道，可以说AlphaGeometry在几何证明上已经和IMO的金牌得主相当，而且AlphaGeometry是在和人类选手同样长的时间内完成题目。相比之下，过去最先进的方法只能解决10个题目。
在去年《知识分子》的专访中，卡耐基梅隆大学数学系教授罗博深（ChatGPT冲击下，中国教育的优势会荡然无存吗？）曾表达过GPT-4给他带来的惊喜。在他看来GPT-4像是一个聪明的学生，单论逻辑推理的水平，已经可以比肩可以做奥数题目的初中生。
今年AlphaGeometry的成就，相比去年的GPT-4又是一次飞跃。IMO的含金量不用多说，现在AlphaGeometry能够解决的问题已经是这个级别了：
AlphaGeometry的开发者，刚刚于纽约大学计算机科学系毕业的Trieu H. Trinh博士表示。“我们的成果不仅仅是一点点改进。这是在结果上的一大飞跃，一个真正的突破。”
AI如何做出IMO难题
计算机证明几何定理此前主要有两种路线。第一类是计算机代数方法，它利用符号推理系统，将几何条件翻译成其点坐标的多项式方程后进行计算。这类方法最出名的是中国科学家吴文俊在70年代开创的“吴方法”。在AlphaGeometry成功前，基于吴方法的求解器在IMO测试中获得了最好的成绩。
第二类是搜索方法，我们最熟悉的就是基于神经语言模型的GPT-4了。这类方法的问题是普遍需要人类的从旁帮助，需要人类提出一些关键推导规则。GPT-4在IMO测试中的表现非常糟糕，正确率为0%。而且还出现了各种语法语义上的错误，胡编乱造，几乎不能理解几何知识。
语言模型擅长快速识别数据中的常规模式和关系，能够迅速预测可能有用的结构，但它们通常缺乏严谨的推理能力和解释决策的能力。而符号推理系统则基于正规逻辑，使用明确的规则来得出结论。这些引擎是理性的、可解释的，但可能显得“慢”且不够灵活——尤其是独自处理大型、复杂问题时。
AlphaGeometry的强大之处在于，创造性地利用一种创新的“神经符号”系统，结合了这两种方式的优点。开发者把这种独特的组合比作丹尼尔·卡尼曼《思考，快与慢》中提出的决策理论，一个系统快速提供“直觉”式的想法（神经语言模型），而另一个则负责更谨慎、理性的决策（符号推理系统）。
比如证明一道简单的几何题：已知等腰三角形ABC中，AB和AC的边长相等，求证：∠ABC=∠BCA。
面对这样一个问题，AlphaGeometry首先会运用符号推理系统，根据题目所给的图形和定理前提进行推理，直到定理被证明或者推不下去。如果推不下去，神经语言模型会构造一个辅助点，让符号推理系统重新推理，重复这个循环直到完成证明。在这道题里，神经语言模型找到了BC的中点D，沿着这个解决方案，AlphaGeometry证明了结论。
这种方法，其实和普通人做一道几何题的思路非常相近。无论是老师还是学生，解决一道几何难题都会借助辅助线来帮助证明。在AlphaGeometry中，善于寻找结构的神经语言模型就是在负责提出各种辅助线。
对于更难的题目，这种思路也能适用，比如2015年IMO第三题需要找到三个辅助点，在神经语言模型（下图蓝色字体）和符号推理系统的交替输出下，经过109个逻辑步骤，这个题目也得到了顺利解决。
AlphaGeometry的解法人类和机器都能读懂。AlphaGeometry对每一道IMO几何实体的解答，都经过计算机检查和验证。
数学教练、前IMO金牌得主Evan Chen也表示“AlphaGeometry 的输出成果令人印象深刻，因为它既能被验证又十分清晰。”在他的印象里，AI解题和简洁与美感无关，是穷尽坐标系统暴力解题的计算机程序，充斥着繁复的代数计算。但AlphaGeometry的计算更像人，“它像学生一样，使用角和相似三角形之类经典几何规则“。
无需人类示范，合成一亿数据
对于机器学习领域来说，定理证明一直是一个难题。在大多数数学领域中，把人类的证明语言翻译成机器能验证的语言非常难，几何的证明语言尤其困难。没有关于定理证明的数据，大模型自然也就没有什么学习成果。因此，过去做几何证明还是主要依赖符号推理系统，即使大模型有着长足的发展，也运用不到几何的证明中去。
AlphaGeometry的优势在于，它绕过了翻译这一步，直接利用算法生成的数据训练神经语言模型，这些生成数据不包括人类编写的示例。其中很多证明的步骤有200多个，要知道IMO题目的平均证明步骤才50个左右。通过这个过程发现的合成定理不受人类审美偏见（例如对称性）的约束，内容更为广泛。
生成数据的步骤比较复杂。AlphaGeometry团队会抽样一组定理的前提条件，作为符号推理系统的输入内容，生成详尽的推导结果。也就是说，团队会生成一组随机的几何图，再推导出其中所有的点线关系。完成后再进行回溯，找出需要哪些额外的结构（如果有的话）才能得出这些证明。
在高度并行的环境下，AlphaGeometry团队随机生成了10亿组几何图形，去除重复的数据后，产生了超过 1 亿个不同难度的、独特的定理和证明，其中900万个含有新增的构造，可以理解为发挥辅助线作用的部分。
有了这些数据，神经语言模型就可以“自学”几何，从而在解题需要找辅助点的时候提供思路，即使面对IMO级别的题目也可以提出足够好的解题建议。
这也回避了大语言模型经常面对的测试成果抄袭指控。AlphaGeometry的数据都是自己生成的，在生成的数据中，也没有和IMO中定理重复的部分。取得IMO测试的好成绩，绝对没有上网抄答案的嫌疑。
对于AlphaGeometry的亮眼成绩，也有人泼冷水，爱丁堡大学的数学和科学历史学家 Michael Barany 就表示，他不知道这是不是一个有意义的的数学里程碑。“奥林匹克的考题与绝大多数数学家所从事的创造性数学大相径庭。”他说。
史上最年轻的IMO金牌得主、加州大学洛杉矶分校数学家陶哲轩则认为，AlphaGeometry 的研究成果“相当出色”，并表示这项工作取得了“意料之外的显著成就”。他表示，虽然将 AI 系统专门调整以解决奥林匹克数学题目，可能不会直接增强其深入研究的能力，但在这个过程中获得的经验可能比最终结果更加宝贵。
不过AlphaGeometry团队最在意的不是数学，而是AI逻辑推理能力的进展。在Nature论文的开篇，团队就提到，证明奥林匹克级别的数学题“是人类水平自动推理的重要里程碑”。
AlphaGeometry系统已经有金牌得主的实力，但团队却表示他们的目标是一个更大的奖项：推动下一代人工智能系统的推理能力。“考虑到利用大规模合成数据，从头开始训练AI系统的更广泛潜力，这种方法可以塑造未来AI系统在数学和其他领域发现新知识的方式。”
数学之后，该团队的更进一步的目标则仍然是：通用人工智能。
在官网的介绍中，AlphaGeometry的开发者表示，“我们的长期目标仍然是建立能够跨数学领域通用的人工智能系统，开发通用人工智能系统所依赖的复杂问题解决和推理能力，同时拓展人类知识的前沿领域。”
参考文献：
1.AlphaGeometry: An Olympiad-level AI system for geometry. (2024, January 17). Google DeepMind.
2.Solving olympiad geometry without human demonstrations. (2024, January 17). Nature.
3.A.I.’s Latest Challenge: the Math Olympics. (2024, January 17). The New York Times.
4.DeepMind AI solves geometry problems at star-student level. (2024, January 17). Nature.
关注《知识分子》视频号
get更多有趣、有料的科普内容
END
继续阅读
阅读原文
关键词
数学
数据
语言模型
定理
方法