早期创造和培养数学天才的主要性已经被很多人认可，他们提出了一个颠覆性的数学教诲理念——将前沿科学研究转化为不须要专业知识背景的抽象根本数学问题，用这些问题在更小年事段选拔科研人才。在这种思路下，分子构造，线性方案等繁芜的科学问题被简化为如鸡兔同笼、牛吃草等根本数学题。与传统看重知识点的教诲模式比较，奥数更磨练包括归纳和推理能力在内的“流动智力”。奥数解题过程更靠近科研事情的实质——将详细问题抽象化，或将抽象问题详细化，然后在不同抽象层级间穿梭。这种教诲理念在选拔数学人才方面取得了卓越成功——许多IMO参赛者后来成为精彩数学家，个中16名奖牌得主更是得到了数学界最大声誉菲尔兹奖。
奥数题目看重通用逻辑能力的特点，使其成为衡量人工智能逻辑能力的空想工具。与大多数针对特定知识点和基本逻辑判断的人工智能基准测试不同，奥数可以通过多重逻辑推理和难以穷举的考察办法来评估人工智能的能力。这意味着最有效的解题方法不是大略的“背题”式预演习，而是利用通用推理方法——这也是人类在奥数中取得精良成绩和进行科研事情所需的核心能力。
AlphaProof/AlphaGeo在国际奥数比赛中得到银牌，仅次于54名金牌选手，标志着人工智能系统在通用推理能力上的进步。与“深蓝”和“AlphaGo”击败人类顶尖选手不同，奥数涵盖的领域更加广泛，对创造性思维和解决前所未见问题的能力哀求更高，同时对论证的严谨性哀求极为苛刻。这些特点让我们看到了人工智能在科研事情中取代人类的巨大潜力。
人工智能在国际奥数比赛上的打破紧张源于三大创新：神经/符号双系统架构，人造数据演习方法，探索式举一反三。
神经/符号双系统架构奥妙地结合了神经网络和符号系统的上风。神经网络基于深度学习模型，具有强大的归纳能力，可从海量数据中创造隐蔽规律。虽然它可能产生“幻觉”，但这种“创造力”对打破常规思维很有代价。与之互补的符号系统则善于严谨的逻辑推理，能在逻辑框架内做出准确判断。DeepMind将这两个别系领悟，创造出一种独特的问题办理方法。
目前，数学界最受关注的机器命题证明系统是Lean措辞，这也是IMO主理者供应给人工智能的题目格式。首先，它将题目转换为机器可读的Lean命题，让符号系统进行逻辑推导，得出更多命题。如果这还不敷以办理问题，神经网络就会参与，利用“扩散性思维”（基于蒙特卡洛树搜索）探求可能精确的中间命题，搭建已知条件和待证明结论之间的桥梁。经由大量演习，神经网络在探求关键推理步骤方面变得越来越高效。
第二个打破是采取“人造数据”方法创建演习集。符号引擎天生了数十亿级的奥数题，这些题目虽然缺少实际比赛题目的奥妙性，但精确性有担保。通过隐蔽中间步骤，这些题目须要神经网络和符号系统协作来办理。演习过程重点关注须要神经系统参与的蒙特卡洛树搜索步骤，提升了模型预判关键推理环节的能力。虽然这些人造题目与实际比赛题目有所不同——后者更看重奥妙和独特的解法，而非通用方法——但由于数据量弘大，许多经典证明方法也被随机天生，在丰富了模型的知识库的同时也验证了模型和人类推理的互通之处。
第三个打破是搜索和验证个例的人工智能模块。DeepMind与多位数学家在《自然》杂志上揭橥的研究阐述了深度学习模型在前沿数学中的潜在运用，个中搜索和验证个例的方法在AlphaProof中得到验证。数学家的事情过程与模型相似，包含“扩散式探索”和严谨论证两个部分。对付一个命题，数学家首先创造个例，然后严格验证命题在个例中的精确性。如果创造禁绝确，他们须要凭直觉改进命题，打消缺点个例，再连续验证。“创造个例”和“验证个例”由符号引擎完成，而改进命题则由扩散式神经网络卖力。如果引擎能创造足够多的个例，神经网络就能从这些数据中的规律判断出更可能精确的命题。DeepMind先容了这种拟人事情办法在拓扑学和抽象代数上取得的打破，这些成果得益于深度学习能够创造不明显的、非线性的、须要大量打算的规律。
通过剖析本次国际数学奥林匹克竞赛（IMO）各题目的解题表现，我们可以清晰地看到不同算法如何提升和补充了人工智能模型的能力。
Q4作为一道范例的几何题，展示了DeepMind今年早些时候发布的AlphaGeo算法的能力。与更为通用的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在某些方面已经超越了人类的通用推理能力。
然而，AI未能解出的Q3和Q5，都属于奥数中的“排列组合”问题。这类问题的特点是解空间极其发散，且命题相对更加开放。这导致AlphaProof在构建人造题库时难以进行更深入的搜索，从而限定了它在这类问题上的解题能力上限。这不仅展示了AI在数学推理方面的巨大进步，也揭示了它在解空间更广的领域存在的局限性，为未来AI算法的改进指明了方向。
人工智能在IMO的造诣，为我们展示了人工智能如何助力前沿数学研究。虽然这类模型从狭义上看并非“通用人工智能”——其演习集和用场局限于办理不等式、平面几何、数论等特定题目，但其开拓方法为人工智能在高等智力劳动中的运用供应了宝贵启迪。IMO模型的成功也指明了未来科研事情者与深度学习模型可以如何互助。
首先，数学家必须将前沿理论转化为打算机可读形式。近年来，包括陶哲轩在内的多位数学家呼吁用开源推理措辞Lean表达数学成果(这也是AlphaProof模型答题的形式)。目前，这个生态系统已包含超过15万项定理，为未来基于深度学习的数学研究奠定了根本。这个事情不止须要数学界把已经揭橥的论文和证明转化成机器可读/可验证模式，它还可能改变数学家的事情流程。如果确信某些相对繁琐的须要列举不同情形证明步骤可以用人工智能证明，数学家会更多选择“大力失事业”的证明办法。曾经，有一万种分类的证明方法是不会被数学家考试测验/接管的，由于审稿者也无法确认其精确性，但现在可以由人工智能完成。此外，浩瀚数学家指出，在形式化证明助手Lean中，“大略命题”和“繁琐命题”的观点与人类直觉存在显著差异。随着Lean逐渐发展成为一种普遍运用的工具，人类数学家将担当起“引导”的关键职能，其核心任务是将数学问题的研究路径转化为Lean更易理解和处理的形式。
其次，存量数据和创造人工数据的方法将变得至关主要。2018年，DeepMind在预测蛋白质构造方面取得了超越人类的打破，这得益于环球生物实验室积累的大量蛋白质折叠数据。然而，真实天下的科研数据每每稀缺。高质量数据集，尤其是具有创新性的数据集，数量有限且难以获取。合成数据可以填补这一缺口。精心设计的合成数据天生算法可以创造出包含各种抽象模式和推理路径的数据，帮助它演习出的深度学习模型培养更深层次的数学直觉和创造力。这个过程和AlphaProof/AlphaGeo研发一样，须要有对领域理解极深的人类做准备事情，并在模型能力和可扩展性上找到平衡点。由于深度学习中的规模法则目前尚未碰着瓶颈，我们有情由相信，合成无限量的演习和测试样本可以进一步提升深度学习模型的抽象能力，提高扩展性，乃至催生出更具创新性的思辨能力。
AlphaProof/AlphaGeo的打破是算力增大过程中产生“呈现能力”的有力证据。DeepMind在演习模型时利用了惊人的三百亿PetaFLOPS算力，相称于演习了GPT-4级别的大措辞模型。近期，大措辞模型的运用彷佛进入了瓶颈期，市场上涌现了认为“算力缺口”并不存在的不雅观点，认为现有算力已足以支持大措辞模型的市场需求。然而，DeepMind在IMO上的成果有力地回嘴了这种不雅观点——纵然通用大措辞模型的算力需求进入瓶颈，同等规模的算力仍旧可以在科研前沿等高代价领域做出大量超越人类顶峰的事情。更主要的是，我们尚不清楚更高数量级的算力是否能在理论物理、能源和材料科学等更多人类智力顶峰领域取得超越人类的成果。其余，如果更高数量级的算力可以在深度学习领域有和人类一样的创新能力，那未来最好的科研模型可能完成自我迭代，指数式地超越人类智能极限。
人工智能超越人类智能的征程，或许才刚刚开始。
（作者系加拿大国际数学奥林匹克竞赛集训队员，普特南竞赛环球百强选手。2014年毕业于哈佛大学运用数学系，现致力于人工智能在金融领域实践。联系办法：nirvanatear@hotmail.com。）