国际数学奥林匹克竞赛（IMO）或许是难度最高的高中数学竞赛，几乎集结了所有的数学天才。最近，一个名为“AlphaGeometry”的人工智能（AI）程序强势加入了IMO赛道，它在几何证明题上的表现已逼近人类金牌选手。
在这篇来自《环球科学》2024年5月新刊中，我们将跟随玛农·比肖夫的讲述，了解人工智能是如何步步逼近人类奥数天才的。
《环球科学》2024年5月新刊销售中
点击图片进入购买页面
撰文｜玛农·比肖夫（Manon Bischoff）
翻译｜陶兆巍
国际数学奥林匹克竞赛（IMO）可能是世界上最著名的高中数学竞赛。每年，世界各地的学生都会竞争他们梦寐以求的IMO奖牌。但可能很快，人工智能（AI）也将加入这场激烈的竞争。今年1月，由谷歌DeepMind公司和美国纽约大学的郑黄朝（Trieu H. Trinh）领导的团队在《自然》（Nature）杂志上发布了一个新的人工智能（AI）程序，名为“AlphaGeometry”，其中“geometry”意为几何。
正如其名，AlphaGeometry很擅长解决复杂的几何证明题，其表现基本上达到了人类IMO金牌得主的水平——过去IMO考试中出现过的30道几何题中，AlphaGeometry解决了25道，它甚至还为2004年的一道题目找到了一个此前的参赛选手都未曾发现且更为通用的解法。
IMO的考试共设有6道题目，分两天进行，每一天参赛选手都需要在四个半小时之内解答三道数学题。有些问题非常困难，甚至连专家都无法解决，但它们的解法却往往简洁而优雅，很需要参赛选手的巧思，这也让AI领域的研究人员对IMO的题目特别感兴趣。
将数学证明“翻译”为计算机可以理解的编程语言并不容易。这样的翻译过程往往需要花费大量人力，导致目前绝大多数数学领域都很难应用依赖大数据的机器学习方法。而在几何领域，翻译遇到的困难尤其严重。此前科学家曾特别针对几何问题开发过一些形式化编程语言，但它们几乎都无法使用其他领域的数学工具。这意味着，一旦在解题过程中用到了一些像“复数法”之类的技巧，就没办法使用这种几何专用的编程语言。
针对这个问题，郑黄朝和他的同事采取了一种与此前研究不同的策略——他们构建了一个完全由机器生成的数据集，它并不需要将人类证明翻译为形式化语言，因此无需消耗大量人力，便能为AI提供几乎不限量的学习数据。
图片来源：pexels
推理与“无中生有”

为了实现这一点，研究人员首先会用算法生成“初始几何构图”，其中包括一个图形和相关的特征信息。比如，一个三角形，它的两条高和它们的交点。然后，AlphaGeometry架构中最重要的两个模块之一——“推理引擎”（DDAR）开始发挥作用。DDAR由DD（Deductive Database，演绎数据库）和AR（Arithmetic Rules，代数法则）构成。DD中包含了一些基本的几何定理，比如“连接三角形两边中点的线段平行于第三边”等定理，同时它能自动应用这些几何定理进行推导；而AR负责其中计算的部分，它可以对边或者角之间的代数关系做代数变形。
演绎数据库与代数法则相结合得到的推理引擎可以从一个几何构图出发，得到这个构图的“推理闭包”，也就是在不添加辅助对象的情况下能证明的所有几何结论，比如“哪两个角相等”、“哪四点共圆”之类的结论。结合这些自动生成的初始构图与其推导出（推理闭包中的）结论的过程，研究人员就得到了一个由“几何定理”和“证明”构成的训练数据集。
然而，要想解决IMO级别的竞赛题，这样的推理算法还远远不够。通常情况下，IMO中出现的几何题都是证明题，包含图形、条件陈述和有待证明的结论（我们也把一个可以被证明的几何题称为一个几何定理）。这些竞赛题几乎都需要参赛选手额外添加辅助构造，才有可能做出完整的证明过程。郑黄朝的研究团队在论文中也写道：“如何生成证明中需要使用的全新的辅助构造才是关键。”
构造题目中并不存在的点或线，大概是很多人曾在中学数学课上经受过的震撼（或者说折磨）。而这些“莫名其妙”却必须出现的辅助构造，对于计算机同样是一种折磨，一般的推导算法并不能做到，但这恰好是AI算法中的大语言模型（large language model，LLM）所擅长的。事实上，大语言模型正是AlphaGeometry架构中的另一个关键模块。
大语言模型生成文本有一个基本原理：通过此前出现的词汇，预测下一个位置里特定词汇出现的概率。郑黄朝的研究团队也基于类似的方法，用 “几何定理-证明”数据集来训练AlphaGeometry。他们将推理引擎生成的几何定理和其证明转化为字符串，然后再用这些数据训练大语言模型。
整个训练过程分为两步：预训练和微调。在第一步（预训练）中，AI首先会学习由几何定理和证明构成的数据集，其中大概包含了一亿个不同的证明。事实上，这一步已经给出了足以证明定理的辅助构造，它们本来就是初始构图中的已知部分（简而言之，就是题目中已经给出辅助构造的几何题）。
在第二步（微调）中，研究人员用“回溯算法”找到了最终证明的定理实际依赖的构图，也就是删除所有和定理表述无关的辅助构造，只留下精简的定理（也就是题目没给辅助线的几何题，它们只占到数据集中的9%），这一过程可以让AI更深刻地理解如何做辅助构造。
不过，大语言模型并没有学习解决几何问题的“严格推导步骤”，这一步依然是由专门的推理引擎负责。在这个架构中，最终训练出来的大语言模型只负责去构造点、线之类的辅助对象。
图片来源：pexels
逼近数学天才
知晓关键模块如何运作后，AlphaGeometry的整体架构就更容易理解了。当AlphaGeometry得到一个问题时，推理引擎会首先推导出题目中图形的一些性质，也就是给出该构图下的推理闭包。如果这些性质并不包含我们要证明的结论，就需要AI介入了。比如，它决定为题目中的三角形ABC添加一个辅助点：BC的中点D——这样的“创造力”正是AI从过往的训练数据中学到的。这样，AI便能为推理引擎提供一个更丰富的构图，在此基础上继续推导新的性质。这两个程序可以交替运行，直到它们一同证明了所需的结论。“这个方法听起来似乎是合理的，某种意义上，它有点像数学竞赛参赛选手的训练过程，”三届IMO金牌获得者、菲尔兹奖得主彼得·舒尔茨（Peter Scholze）评价道。
为了测试AlphaGeometry的实力，研究人员从2000年以来IMO竞赛出现过的几何题中选取了30道，占总几何题数量的75%，只有那些在系统中无法表述的问题（例如几何不等式和组合几何问题）没被包含在内。最终，AlphaGeometry解决了其中的25道问题。与之相对的，大语言模型GPT-4一道题目也解不出来；而IMO选手平均能解出其中15.2道题，铜牌选手解出了19.3道，而金牌得主也没比AlphaGeometry好多少——他们平均能解决其中25.9道几何题。这也意味着，AlphaGeometry的表现已经超过了绝大多数IMO参赛者。
值得一提的是，此前由我国著名数学家吴文俊开发的“吴方法”，其实是一个“理论上更强有力的”解决几何题的算法。吴文俊在理论上证明，如果允许他的算法运行足够长的时间，它一定可以“证明任何一个结论正确的欧式几何定理”。然而，吴方法有两个根本性的问题：第一，它生成的证明并不是我们人类可以阅读的；第二，它真的太慢了——研究人员留给吴方法解决每一道问题的时间是4.5个小时，最终它只解决了30道问题中的10道。而即使把时间放宽10倍，吴方法也没能解决更多的问题。
幸运的是，AlphaGeometry生成的数学证明对于人类来说是完全可读的，而非机器语言。当研究人员开始仔细阅读AI生成的这些几何题的解题过程时，他们发现了一个非常特别的证明。这个证明并没有用到问题里的全部条件，也就是说，AlphaGeometry自己发现了一个“推广问题”（题目给出的已知条件比原题目更少）的解，相对原题则是更通用的解法。同样非常明显的是，对于那些人类IMO参赛选手很难处理、较为复杂的问题，机器给出的证明长度通常来讲也更长（简单的问题却并非如此）。看上去，AI和我们人类在这些挑战上面临着相似的困境。
目前，AlphaGeometry还不能参与IMO竞赛，因为并非所有的题目都是几何题——它们只占三分之一左右。但是郑黄朝和他的团队还是强调，这个架构其实可以广泛用于其他数学领域，比如组合学。
硅基选手如何进化
当然，想要让AI真正地在数学的其他方面展现相当的水平并非易事。研究人员不仅需要在代码层面对研究领域中的数学概念给出明确的定义，也需要考虑如何搭建相应的架构。在几何领域表现优异的AlphaGeometry，其架构包括三个部分：一个初始“构图”采样器、一个用于推理的符号引擎和一个能识别辅助构造的回溯算法。只有集齐了这些部件，大语言模型的创造力才能真正发挥作用。但仔细考虑这三个部分，每一个都不简单。
这篇论文的第二作者吴宇怀指出，在一般的数学问题中，我们可能无法像在欧式几何中那样，相对容易地进行构图采样；与此同时，推理引擎和回溯算法的构建往往需要大量的数学专业知识。AlphaGeometry用到的演绎数据库正是基于张景中院士等人多年来的研究成果；而这个“相当不平凡”的回溯算法则是郑黄朝本人的杰作，他花了整整4年的时间（几乎是他就读博士学位期间的全部时间）才将这些成果组合起来。
如今，AI领域的发展势头可谓迅猛，几乎每隔几天便有新的突破。谁又能知道未来呢？也许过不了几年，某位硅基选手会参加IMO竞赛，它可能还会带走金牌。
本文为《环球科学》2024年5月刊《几何竞赛，AI逼近人类天才》一文
《环球科学》2024年5月新刊
正在热卖

戳图片或阅读原文
立即购买
点击【在看】，及时接收我们的内容更新 
继续阅读
阅读原文
关键词
数据
数学竞赛
定理
奥数
问题