水平接近人类金牌选手，人工智能（AI）学会做国际数学奥林匹克竞赛难题了。
这个名为 AlphaGeometry 的 AI 模型由来自 Google DeepMind 和纽约大学的联合团队研发，是一个能解国际数学奥林匹克竞赛级别几何题的 AI 系统，于近日登上了顶级科学期刊 Nature。
据介绍，AlphaGeometry 通过自主合成数百万个定理和证明，解决了 30 个最新奥林匹克级别（优等高中生参加的数学定理证明大赛）问题中的 25 个，接近国际数学奥林匹克竞赛金牌选手的平均表现，远超之前最好的自动化定理证明系统。
这一突破标志着 AI 在数学问题解决方面取得了显著的进展——无需人类演示即可自主应对复杂的几何学挑战。
该研究证明了 AI 能以接近人类最高水平破解复杂逻辑挑战的潜力——这正是 AI 研究的一个主要目标。
值得一提的是，AlphaGeometry 能生成人类可阅读的证明，甚至发现了 2004 年国际数学奥林匹克竞赛定理的一个新版本。
相关研究论文以“Solving olympiad geometry without human demonstrations”为题，1月17日发表在 Nature 上。
AI 搞定奥数题，很难吗？
自 20 世纪 50 年代以来，追求更好的定理证明能力一直是 AI 研究的焦点。数学奥林匹克竞赛是世界上最著名的定理证明竞赛，其历史可以追溯到 1959 年，在发现卓越人才方面有着重要作用。
国际数学奥林匹克竞赛的题目通常涉及深度的数学理论和抽象的数学概念，需要独立思考、创造性解决问题和运用直觉。这些问题往往要求高度的逻辑推理和创造性的思维，这是人类数学家所具备的，但超越了传统的机器学习方法的应用范围。
此外，与其他领域相比，人类解决数学问题的过程不容易转化为大规模的可用于训练的数据集。几何学具有特有的翻译困难，在通用数学语言中的证明示例也很少。并且几何语言具有非常精准的定义，无法表达许多使用几何范围之外的人类证明，比如复数。
图｜IMO2000P6的人类证明和 AlphaGeometry 证明的并排比较。这是一个较难的问题（人类平均得分 = 1.05/7），问题陈述中包含大量对象。左图，人类解决方案使用复数。通过精心选择的坐标系，问题会大大简化，并且通过代数运算自然可以得出解决方案。右图，AlphaGeometry 解决方案涉及两个辅助构造和100多个推导步骤，其中许多低级步骤对于人类来说极其乏味。在这种情况下，基于搜索的解决方案的可读性和直观性要差得多。更具结构性的组织，即高级的证明大纲，可以大大提高AlphaGeometry 解决方案的可读性。在AlphaGeometry中构建许多高级推导规则，有助于减少低级推导并简化证明步骤。（来源：该论文）
缺乏足够的样本数据，特别是包含人类专业数学家的解答过程，使得机器学习模型难以学习和理解解题方法。因此，目前的几何方法仍主要依赖于符号方法和人工设计的硬编码搜索启发式。
无需人类，自主解决复杂问题
在该研究中，AlphaGeometry 的关键创新点在于，其能够综合数百万条复杂程度各异的定理和证明，利用从头训练的神经语言模型进行自主训练。这意味着 AlphaGeometry 能够独立学习和解决各类复杂问题，而无需依赖人类输入。
神经语言模型在引导符号演绎引擎（能够搜索难题中的大量分支点）方面具有独特的优势。神经模型的引入使得 AlphaGeometry 在处理具有挑战性的问题时能够做出更为精准的推理。这种综合运用符号演绎引擎和神经语言模型的方法是该研究的重要创新之一。
图｜AlphaGeometry 概述以及它如何解决简单问题和IMO2015问题3。顶行显示 AlphaGeometry 如何解决简单问题。a）简单的例子及其图表。b）模型通过运行符号推演引擎来启动证明搜索。引擎从定理前提中详尽地推导出新的陈述，直到定理被证明或新的陈述被穷举为止。c）由于符号引擎未能找到证明，语言模型构造一个辅助点，在符号引擎重试之前增长证明状态。循环继续直到找到解决方案。d）对于简单的例子，循环在第一个辅助结构“D作为BC的中点”之后终止。该证明包括另外两个步骤，这两个步骤都利用了中点属性：“BD = DC”和“B、D、C 共线”。底行显示了 AlphaGeometry 如何解决 IMO 2015 Problem 3 (IMO 2015 P3)。e）IMO 2015 P3 问题陈述和图表。f IMO 2015 P3的解有3个辅助点。（来源：该论文）
尽管 AlphaGeometry 在解决奥林匹克级别的几何问题上取得了显著的成功，但也存在一些局限性。
据论文描述，AlphaGeometry 主要专注于解决奥林匹克级别的几何问题，应用范围相对狭窄。这限制了该方法在其他数学领域或实际问题中的推广。未来的研究需要探讨如何扩展该方法以涵盖更广泛的数学领域。
而且，研究团队采用了大规模的人工合成数据来训练 AlphaGeometry，这虽然为模型提供了广泛的学习材料，但合成数据仍然可能无法完全覆盖真实数学问题的多样性和复杂性。因此，模型在真实场景中的性能可能会受到数据不足的影响。
此外，虽然 AlphaGeometry 能够生成人类可读的证明，但在处理极其复杂的推理时，其生成的结果可能变得难以理解。这使得人们在一些情况下难以追踪和解释模型的推理过程。
解决数学问题，AI 大有可为
近年来，使用 AI 技术来理解和证明数学定理，是科学家们重点关注的研究方向之一。
例如，AI 可以被用来开发自动定理证明系统，这些系统可以独立地推导和证明数学定理。这种方法旨在减轻人工证明的负担，并提供更高效的证明方法。
此外，AI 也可以被用来构建数学知识图谱，有助于将数学概念之间的关系建模成图结构。这种图谱可以用于改进定理的推理和证明，使得系统能够更好地理解数学领域的知识体系。
对于创造性思维的开发，AI 也有一席之地。一些研究采用生成式模型，比如生成对抗网络（GANs），来生成符合数学结构和规范的新定理。这种方法有助于拓展数学领域的创造性思维，引入新的数学概念和结论。
当然，要使得 AI 在数学领域展现出如人类顶尖数学家一般的水平，还有很长的路要走。
尽管如此，AlphaGeometry 展现出了 AI 在数学方面的应用潜力，这一成果不仅为数学领域带来了创新，也为 AI 在其他领域的应用带来了新的可能。
论文链接：
本文来自微信公众号：学术头条 （ID：SciTouTiao），作者：学术头条