AlphaGeometry：敢挑战奥数金牌选手的AI解题家

原文作者：Davide Castelvecchi

如今，算法解几何题的水平已经接近世界上数学最好的中学生。

一个人工智能（AI）系统能严格证明几何表述是否正确，这类表述是指关于三角形或多边形这类二维形状的陈述，其表现甚至堪比国际数学奥林匹克竞赛（IMO）的选手——国际数学奥赛是面向中小学生的数学比赛。该系统名为AlphaGeometry，相关研究1月17日发表于《自然》[1]。

研究团队让AlphaGeometry做了30道IMO的几何题，AlphaGeometry解出了其中25题——至少在几何方面达到了接近奥数金牌选手的水平。帝国理工学院的数学家Kevin Buzzard表示，几何只是IMO选手必须掌握的一个分支，想在IMO其他分支的问题上达到同等水准没这么容易，比如数论。但Buzzard依然表示，“能解出25道奥数题，而且能给出人类可读的证明，这已经很厉害了。”

语言障碍

研究人员曾用大语言模型解过各种数学题——大语言模型是一种AI程序，其学习方式是使用大型文本集进行训练，时下最热门的对话机器人用的就是这种技术。虽然结果令人鼓舞但一直缺乏意义。

比如，Minerva是谷歌（Google）针对数学领域开发的一款用于科研目的的对话机器人，其训练素材为前沿数学论文和中小学基础数学题的人类作答。虽然Minerva给出的数值答案通常是对的，但它给出的解题思路往往有错误，需要人工检查。该论文共同作者、谷歌DeepMind的计算机科学家Trieu Trinh说：“如果一个系统是用自然语言训练的，它输出必然也是自然语言，而这是我们无法信任的。”

所以，Trinh和合作者没有使用自然语言，而是开发了一种写几何证明的语言，拥有类似于计算机编程语言的严格语法。这样一来，它的答案不仅能被人类读懂，还能让计算机检查。

该团队聚焦欧几里德几何，目标是给一个陈述写一段数学证明。他们在这些定制语言中嵌入了几十条基本几何规律，例如“如果一条直线与第二条直线相交，那么这条直线也会与第二条线的平行线相交”。

他们随后又写了一个程序，能自动生成1亿个“证明”。本质上，这些证明是简单但逻辑严密步骤的随机序列，比如“有A和B两个点，构建正方形ABCD”。

这些机器生成的证明被用来训练AlphaGeometry。这表示AlphaGeometry能通过猜测下一步方式来解题，就和对话机器人生成文本的方式一样。但这也意味着其输出是机器可读的，并且很容易检查对错。对于每个问题，AlphaGeometry都会多次尝试得出一个答案。由于AlphaGeometry会自动剔除错误的答案，所以它能可靠地生成正确的结果，包括对IMO的几何题。

技术结合

AlphaGeometry将语言模型的brute-force统计猜测与符号推理相结合，这可能是它厉害的原因所在，德国巴登-符腾堡双元制应用技术大学计算机科学家Stephan Schulz说，整个方法都有很有潜力。

Buzzard表示，用合成数据训练AlphaGeometry还能避免将经典大语言模型用于数学的一个潜在隐患：作弊。他表示，对于一个用网上无数个文本训练出来的神经网络来说，“你很难保证模型从没见过这个问题。”

用自动生成的证据训练AlphaGeometry还有一个目的，研究共同作者、纽约大学的计算机科学家He He说，“我们想在不使用人类数据的情况下构建这个系统，这样它将来就可以拥有超越人类的能力。”

当然，这对数学家的工作暂时还不构成威胁。“我能想象几年后，机器学习领域各种技术解数学题水平或许能比肩最拔尖的大学生，”Buzzard说，“但目前没有证据表明，机器具有自动开展现代数学研究的水平。”