AI 挑战国际数学奥林匹克竞赛，AlphaGeometry 展现了它超强的解题能力。
DeepMind 和纽约大学的联合团队研发出了一款名为 AlphaGeometry 的 AI 模型，该模型具备解决国际数学奥林匹克竞赛级别几何题的能力。在最近的一期《自然》杂志上，这款 AI 系统被详细介绍，引起了广泛关注。
AlphaGeometry 的表现令人惊叹，它自主合成了数百万个定理和证明，成功解决了 30 个最新奥林匹克级别问题中的 25 个。这一成绩已经接近国际数学奥林匹克竞赛金牌选手的平均表现，远超过了之前的自动化定理证明系统。
这一突破标志着 AI 在数学问题解决方面取得了显著的进展—— 无需人类演示即可自主应对复杂的几何学挑战 。该研究证明了 AI 能以接近人类最高水平破解复杂逻辑挑战的潜力——这正是 AI 研究的一个主要目标。
值得一提的是，AlphaGeometry 能生成人类可阅读的证明， 甚至发现了 2004 年国际数学奥林匹克竞赛定理的一个新版本 。
相关研究论文以“Solving olympiad geometry without human demonstrations”为题，刚刚发表在 Nature 上。
01 AI 搞定奥数题，很难吗?
自 20 世纪 50 年代以来，追求更好的定理证明能力一直是 AI 研究的焦点。数学奥林匹克竞赛是世界上最著名的定理证明竞赛，其历史可以追溯到
1959 年，在发现卓越人才方面有着重要作用。
国际数学奥林匹克竞赛的题目通常涉及深度的数学理论和抽象的数学概念，需要独立思考、创造性解决问题和运用直觉。
这些问题往往要求高度的逻辑推理和创造性的思维，这是人类数学家所具备的 ，但超越了传统的机器学习方法的应用范围。
此外，与其他领域相比，人类解决数学问题的过程不容易转化为大规模的可用于训练的数据集。几何学具有特有的翻译困难，在通用数学语言中的证明示例也很少。并且几何语言具有非常精准的定义，无法表达许多使用几何范围之外的人类证明，比如复数。
图|IMO2000P6的人类证明和 AlphaGeometry 证明的并排比较。这是一个较难的问题(人类平均得分 =
1.05/7)，问题陈述中包含大量对象。左图，人类解决方案使用复数。通过精心选择的坐标系，问题会大大简化，并且通过代数运算自然可以得出解决方案。右图，AlphaGeometry
解决方案涉及两个辅助构造和100多个推导步骤，其中许多低级步骤对于人类来说极其乏味。在这种情况下，基于搜索的解决方案的可读性和直观性要差得多。更具结构性的组织，即高级的证明大纲，可以大大提高AlphaGeometry
解决方案的可读性。在AlphaGeometry中构建许多高级推导规则，有助于减少低级推导并简化证明步骤。(来源：该论文)
缺乏足够的样本数据，特别是包含人类专业数学家的解答过程，使得机器学习模型难以学习和理解解题方法
。因此，目前的几何方法仍主要依赖于符号方法和人工设计的硬编码搜索启发式。
02 无需人类，自主解决复杂问题
在该研究中，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 能够生成人类可读的证明，但在处理极其复杂的推理时，其生成的结果可能变得难以理解。这使得
人们在一些情况下难以追踪和解释模型的推理过程 。
03 解决数学问题，AI 大有可为
AI在数学领域的应用已经引起了广泛的关注。从自动定理证明到知识图谱构建，再到创造性思维开发，AI在解决数学问题方面展现出了巨大的潜力。这些技术的应用有望为数学领域带来更多创新和突破。
自动定理证明是AI在数学领域的一个重要应用。通过AI技术，可以自主推导和证明数学定理，从而减轻人工证明的负担并提供更高效的证明方法。这种技术的应用有望推动数学领域的发展和进步。
数学知识图谱是一种将数学概念之间的关系建模成图结构的方法。AI在构建数学知识图谱方面也具有广泛的应用前景。通过构建数学知识图谱，AI能够更好地理解数学领域的知识体系，并用于改进定理的推理和证明。这种方法有望提高定理证明的准确性和效率。
AI在创造性思维开发方面也具有广泛的应用前景。一些研究采用生成式模型，如生成对抗网络(GANs)，来生成符合数学结构和规范的新定理。这种方法有助于拓展数学领域的创造性思维，引入新的数学概念和结论。通过AI技术，我们可以更好地探索数学领域的未知领域，推动数学的发展和进步。
尽管目前AI在数学领域的应用还有很大的发展空间，但随着技术的不断进步和应用场景的不断拓展，AI在数学领域的应用前景将越来越广阔。未来，我们有望看到更多创新和突破，AI将为数学领域带来更多的可能性。
试试，新一代AI效率神器 @ 海鲸AI