人工智能在数学上能够走多远？IMO银牌是个里程碑 | jonathan zhou

人工智能学家 · 公众号 · AI · 2024-09-03 20:45

正文

来源：风云之声

近日， DeepMind 的AlphaProof/AlphaGeo在国际数学奥林匹克竞赛(IMO)中取得了前所未有的成绩，解出了六道问题中的四道，获得银牌。这是个什么成绩呢？本届竞赛共有来自108个国家的609位选手参加，其中54人获得金牌，121人获得银牌，145人获得铜牌。因此，AlphaProof/AlphaGeo的成绩可以说仅次于54位人类选手。这一成就无疑将与"深蓝"击败卡斯帕罗夫和"AlphaGo"击败李世石一样，成为人工智能挑战人类智力巅峰的又一里程碑，同时也将引发新一轮关于机器智力边界的讨论。

冷战背景下，一些社会主义阵营国家认为数学是科学和技术发展的基础，也意识到了早期发现和培养数学天才的重要性。他们提出了一个颠覆性的数学教育理念——将前沿科学研究转化为不需要专业知识背景的抽象基础数学问题，用这些问题在更小年龄段选拔科研人才。在这种思路下，分子结构、线性规划等复杂的科学问题被简化为如鸡兔同笼、牛吃草等基础数学题。与传统注重知识点的教育模式相比，奥数更考验包括归纳和推理能力在内的"流动智力"。奥数解题过程更接近科研工作的本质——将具体问题抽象化，或将抽象问题具体化，然后在不同抽象层级间穿梭。这种教育理念在选拔数学人才方面取得了卓越成功——许多IMO参赛者后来成为杰出数学家，其中16名奖牌得主更是获得了数学界最高荣誉菲尔兹奖。

奥数题目注重通用逻辑能力的特点，使其成为衡量人工智能逻辑能力的理想工具。与大多数针对特定知识点和基本逻辑判断的人工智能基准测试不同，奥数可以通过多重逻辑推理和难以穷举的考核方式来评估人工智能的能力。这意味着最有效的解题方法不是简单的"背题"式预训练，而是运用通用推理方法——这也是人类在奥数中取得优异成绩和进行科研工作所需的核心能力。

因此，AlphaProof/AlphaGeo在国际奥数比赛中获得银牌，标志着人工智能系统在通用推理能力上已经接近最优秀的人类。与"深蓝"和"AlphaGo"击败人类顶尖选手不同，奥数涵盖的领域更加广泛，对创造性思维和解决前所未见问题的能力要求更高，同时对论证的严谨性要求极为苛刻。这些特点让我们看到了人工智能在科研工作中取代人类的巨大潜力。

人工智能是如何在国际奥数比赛上取得突破的？答案是三大创新：神经/符号双系统架构，人造数据训练方法，探索式举一反三。

第一个创新，是神经/符号双系统架构，它巧妙地结合了神经网络和符号系统的优点。神经网络基于深度学习模型，具有强大的归纳能力，可从海量数据中发现隐藏规律。虽然它可能产生"幻觉"，但这种"创造力"对突破常规思维很有价值。与之互补的符号系统则擅长严谨的逻辑推理，能在逻辑框架内做出准确判断。DeepMind将这两个系统融合，创造出一种独特的问题解决方法。目前，数学界最受关注的机器命题证明系统是Lean语言，这也是IMO主办者提供给人工智能的题目格式。首先，它将题目转换为机器可读的Lean命题，让符号系统进行逻辑推导，得出更多命题。如果这还不足以解决问题，神经网络就会介入，运用"扩散性思维"（基于蒙特卡洛树搜索）寻找可能正确的中间命题，搭建已知条件和待证明结论之间的桥梁。经过大量训练，神经网络在寻找关键推理步骤方面变得越来越高效。

第二个创新，是采用"人造数据"方法创建训练集。符号引擎生成了数十亿级的奥数题，这些题目虽然缺乏实际比赛题目的巧妙性，但正确性有保证。通过隐藏中间步骤，这些题目需要神经网络和符号系统协作来解决。训练过程重点关注需要神经系统参与的蒙特卡洛树搜索步骤，提升了模型预判关键推理环节的能力。虽然这些人造题目与实际比赛题目有所不同——后者更注重巧妙和独特的解法，而非通用方法——但由于数据量庞大，许多经典证明方法也被随机生成，在丰富了模型的知识库的同时也验证了模型和人类推理的互通之处。

第三个创新，是搜索和验证个例的人工智能模块。DeepMind与多位数学家在《自然》杂志上发表的研究阐述了深度学习模型在前沿数学中的潜在应用，其中搜索和验证个例的方法在AlphaProof中得到验证。数学家的工作过程与模型相似，包含"扩散式探索"和严谨论证两个部分。对于一个命题，数学家首先创造个例，然后严格验证命题在个例中的正确性。如果发现不正确，他们需要凭直觉改进命题，排除错误个例，再继续验证。"创造个例"和"验证个例"由符号引擎完成，而改进命题则由扩散式神经网络负责。如果引擎能创造足够多的个例，神经网络就能从这些数据中的规律判断出更可能正确的命题。DeepMind介绍了这种拟人工作方式在拓扑学和抽象代数上取得的突破，这些成果得益于深度学习能够发现不明显的、非线性的、需要大量计算的规律。

IMO题目总共有六道，覆盖几何、代数、排列组合等领域。我们来具体看看，人工智能在每道题目上的表现，从中就可以清晰地看到各种创新的效果以及局限。

Q4是一道典型的几何题，它展示了DeepMind今年早些时候发布的AlphaGeo算法的威力。与更为通用，基于Lean引擎的AlphaProof不同，AlphaGeo专注于通过几何题引擎和辅助线解决几何问题。它通过建立一个包含一亿条复杂命题证明的庞大数据库，培养了神经网络判断辅助线效用的能力。这个理解辅助线功效的神经网络能够从数十条可行的辅助线中筛选出最具潜力的方向。这种高效筛选使AlphaGeo能在搜索树上深入探索，从而解决更具挑战性的问题。由于几何题的搜索空间最小，AlphaGeo在拿到题后19秒就证明出来了，远快于任何人类。(图为AlphaGeo的解法和辅助线)

Q2则考验了"中间命题"的广度。与几何题不同，数论问题的中间步骤搜索空间更为广阔。在Q2中，如果参赛者（无论是人类还是AI）能洞察到x = ab + 1这个巧妙的中间步骤，整个问题就会简化为仅需三行即可证明的简单命题。这意味着，AlphaProof与人类一样，需要具备发现x = ab + 1的洞察力。考虑到这个构造在已知题库中前所未见，对它的洞察力必然源于AlphaProof在生成数十亿训练样本的过程中，反复尝试类似问题后产生的涌现能力。

Q1和Q6则考验了AI反复创造和验证个例的能力。具备这种能力的AI可以基于已知命题生成大量个例，通过验证这些个例是否符合证明条件，不断探索正例和反例的边界，最终找到正确的命题。这种主动探索能力的出现，预示着AI有能力在寻找未知解时探索新颖路径，并在过程中不断调整方向。最令人惊叹的是，在这次比赛中，只有五名人类选手解出的Q6，AlphaProof却给出了满分证明。这有力地证明了AI在某些方面已经超越了人类的通用推理能力。

AlphaProof在Q1和Q6上展现了巨量算力的威力。在得到题目后，AlphaProof遇到证明困难时，采取了“临场题海战术”，人工生成大量类似的，可以解决的问题，再从这些问题的证明中训练神经网络在原题上找更深的解法。虽然使用这种战术的AlphaProof证明这两道题花了三天时间，超过了人类选手的时间限制，但这仅是因为AlphaProof的算力资源不够，有足够算力资源的情况下可以和人类一样在9小时内答完题。

然而，有两道题AI还未能解出，它们是Q3和Q5。这两道题都属于奥数中的"排列组合"问题，这类问题的特点是解空间极其发散，且命题相对更加开放。因此，组合数学更加依赖于数学家的个人灵感，在整个数学界往往属于鄙视链的下端。例如中国得过国家自然科学一等奖的中学教师陆家羲以及匈牙利传奇数学家保罗·埃尔德什，在许多正统数学家那里得到的评价都比较微妙。由于解空间发散，AlphaProof在构建人造题库时难以进行更深入的搜索，从而限制了它在这类问题上的能力。这不仅展示了AI在数学推理方面的巨大进步，也揭示了它在解空间更广的领域的局限性，为未来AI算法的改进指明了方向。

人工智能在IMO的成就，为我们展示了人工智能如何助力前沿数学研究。虽然这类模型看并非"通用人工智能"——其训练集和用途局限于解决不等式、平面几何、数论等特定题目，但其开发方法无疑为人工智能在高级智力劳动中的应用提供了宝贵启示。

IMO模型的成功，也启示了未来科研工作者与深度学习模型可以如何合作。

首先，数学家必须将前沿理论转化为计算机可读形式。近年来，包括陶哲轩在内的多位数学家呼吁用开源推理语言Lean表达数学成果(这也是AlphaProof模型答题的形式)。目前，这个生态系统已包含超过15万项定理，为未来基于深度学习的数学研究奠定了基础。这个工作不止需要数学界把已经发表的论文和证明转化成机器可读/可验证模式，它还可能改变数学家的工作流程。假如确信某些相对繁琐的需要列举不同情况证明步骤可以用人工智能证明，数学家会更多选择“大力出奇迹”的证明方式。曾经，有一万种分类的证明方法（例如四色定理）是不会被数学家尝试/接受的，因为审稿者也无法确认其正确性，但现在可以由人工智能完成。此外，众多数学家指出，在形式化证明助手Lean中，"简单命题"和"繁琐命题"的概念与人类直觉存在显著差异。很多数学家发现，一些在自然语言中条件简单的命题，在Lean语言中表述繁琐，而另一些命题则是相反。随着Lean逐渐发展成为一种普遍应用的工具，人类数学家将担当起"向导"的关键职能，其核心任务是将数学问题的研究路径转化为Lean更易理解和处理的形式。

其次，存量数据和创造人工数据的方法将变得至关重要。2018年，DeepMind在预测蛋白质结构方面取得了超越人类的突破，这得益于全球生物实验室积累的大量蛋白质折叠数据。然而，真实世界的科研数据往往稀缺。高质量数据集，尤其是具有创新性的数据集，数量有限且难以获取。合成数据可以弥补这一缺口。精心设计的合成数据生成算法可以创造出包含各种抽象模式和推理路径的数据，帮助它训练出的深度学习模型培养更深层次的数学直觉和创造力。这个过程和AlphaProof/AlphaGeo研发一样，需要有对领域理解极深的人类做准备工作，并在模型能力和可扩展性上找到平衡点。由于深度学习中的规模法则目前尚未遇到瓶颈，我们有理由相信，合成无限量的训练和测试样本可以进一步提升深度学习模型的抽象能力，提高扩展性，甚至催生出更具创新性的思辨能力。

人工智能在数学上能够走多远？IMO银牌是个里程碑 | jonathan zhou

正文

请到「今天看啥」查看全文