这项工作代表了 AI 在数学推理上的威力突破，是开发通用 AI 体系方面的重要里程碑。
这一次，人工智能算法在数学奥林匹克比赛（IMO）上取得了重大成绩突破。
在今天发表的国际权威期刊《自然》杂志最新一期上，论文《Solving olympiad geometry without human demonstrations》向世人介绍了 AlphaGeometry，专家表示，这是人工智能朝着具有人类推理威力方向迈进的重要一步。
论文链接：https://www.nature.com/articles/s41586-023-06747-5
DeepMind 也在论文发表的第一时间将代码和模型开源，GitHub：https://github.com/google-deepmind/alphageometry
这是一种人工智能体系，来自 Google DeepMind 研究者之手，它可能以接近人类奥赛金牌得主的水平办理复杂的多少成绩。
在对 30 道奥数多少题的基准测试中，AlphaGeometry 在标准奥数时限内办理了 25 道。相比之下，之前最先进的体系办理了其中 10 个多少成绩，而人类金牌得主平均办理了 25.9 个成绩。
定理说明对于鉴于学习的 AI 模型来说困难程度很高，因为在大多数数学领域中，翻译成机器可验证言语的人类说明的训练数据都很少。DeepMind 提出了一种使用分解数据进行定理说明的替代格式，鉴于该办理方案的通用的指导框架 AlphaGeometry 具有对很多领域的适用性。
研究介绍
AlphaGeometry 将言语模型与「标记引擎」相结合，借助标记和逻辑规矩进行数学推论。在这其中，言语模型擅长识别、预测流程的后续步骤，但缺乏数学推理所需的严谨性；另一方面，标记引擎纯粹鉴于形式逻辑和严格的规矩，这使得它可能引导言语模型走向理性决策。
在 AlphaGeometry 的研究上，DeepMind 从跨越 2000 年到 2022 年之间的 30 个奥林匹克多少成绩（IMO-AG-30）的基准测试集中进行了测试，结果表明，AlphaGeometry 在比赛时间限制下可能办理 25 个成绩。而之前最先进的格式（Wu’s method）只能办理 10 个。
众所周知，由于缺乏推理技能和训练数据，AI 体系经常难以办理多少和数学方面的复杂成绩。AlphaGeometry 体系将神经言语模型的预测威力与规矩约束推理引擎相结合，两者协同工作以找到了新的办理方案。
此外，为了办理数据难题，该研究生成了大量的分解训练数据，即 1 亿个示例，其中许多定理的说明步骤超过 200 步，比数学奥林匹克比赛定理的平均说明长度长 4 倍。
AlphaGeometry 展示了 AI 不断增长的逻辑推理威力以及发现和验证新知识的威力。办理奥林匹克级别的多少成绩是 AI 在迈向更先进和通用人工智能体系道路上的一个重要里程碑。
菲尔兹奖得主、IMO 金牌获得者 Ngô Bảo Châu（吴宝珠）表示：「现在我完全明白了，为什么 AI 研究者们会首先尝试办理国际数学奥林匹克 (IMO) 的多少题目，因为找到它们的办理方案有点像下棋，我们在每一步都有相对较少的合理走法。但我仍然对他们可能实现这一点感到震惊。这是一项令人印象深刻的成就。」
吴宝珠，2010 年菲尔兹奖得主，现任芝加哥大学教授。
AlphaGeometry 是一个神经标记体系，由神经言语模型和标记推演引擎组成，它们共同寻找复杂多少定理的说明。一个体系提供快速、直观的想法，而另一种则提供更加深思熟虑、理性的决策。
由于言语模型擅长识别数据中的一般模式和关系，因此它们可以快速预测潜在有用的结构，但通常缺乏严格推理或做出解释。另一方面，标记推演引擎鉴于形式逻辑并使用明确的规矩来得出结论，两者相互配合，共同构成了 AlphaGeometry。
AlphaGeometry 的言语模型引导其标记推演引擎寻找多少成绩的可能办理方案。一般的奥林匹克多少成绩鉴于图表，需要添加新的多少结构才能办理，例如点、线或圆。AlphaGeometry 的言语模型可以从无数种可能性中预测添加哪些新结构最有用。这些线索有助于填补空白，并允许标记引擎对图表进行进一步推论并接近办理方案。
举例来说，下图（上）为 AlphaGeometry 解答简单题的过程，题目为「设 ABC 为 AB = AC 的任意三角形。说明∠ABC = ∠BCA。」
AlphaGeometry 说明过程是这样的：AlphaGeometry 通过运行标记推演引擎（symbolic deduction engine）启动说明搜索。这个引擎会从定理的前提出发，详尽地推导出新的陈述，直到定理得到说明或者新的陈述被耗尽。假如标记引擎未能找到说明，言语模型会构造一个辅助点，在标记引擎重新开始之前增加可说明的条件。这个循环一直持续到找到办理方案为止。对于简单的例子，循环在第一个辅助结构「 BC 的中点添加 D 点」之后终止。
下图（下）为 AlphaGeometry 办理 IMO 的解题思路。「说明三角形 FKM 和 KQH 的外接圆 (O1) 和 (O2) 彼此相切……」，这么复杂的成绩，AlphaGeometry 同样也能说明，说明过程还给出了辅助点等。出于说明目的，说明过程被大大缩短和编辑。
生成 1 亿数学推理训练数据
人类可以在纸上进行勾画来学习多少、检查图表并使用现有知识来发现新的、更复杂的多少属性和关系。该研究生成分解数据的格式大规模模拟了这种知识构建过程。其中生成分解数据的格式如图 3 所示。
使用高度并行计算，体系首先生成 5 亿个多少对象的随机图，并详尽地导出每个图中点和线之间的所有关系。AlphaGeometry 找到每个图中包含的所有说明，然后逆向推导，找出需要哪些额外的结构（如果有的话）来获得这些说明。这一过程为「标记推演与回溯」。
由 AlphaGeometry 生成的分解数据的可视化表示
之后，这个巨大的数据池被过滤以排除类似的示例，从而产生了 1 亿个训练数据集。
开创性的人工智能推理威力
AlphaGeometry 提供的每一道奥数题的解法都经过计算机检查和验证。研究人员还将其结果与之前的人工智能格式以及人类在奥林匹克比赛中的表现进行了比较。此外，数学教练、前奥赛金牌得主 Evan Chen（陈谊廷）为我们评估了 AlphaGeometry 的一系列办理方案。
陈谊廷，MIT 数学在读博士，曾获得 IMO 2014 年金牌。
Evan Chen 表示：「AlphaGeometry 的输出令人印象深刻，因为它既可验证又干净。过去针对鉴于说明的竞争成绩的人工智能办理方案有时是碰巧的（输出有时是正确的，需要人工检查），而 AlphaGeometry 没有这个弱点：它的办理方案具有机器可验证的结构。另一方面，它的输出仍然是人类可读的。人们可以想象一个通过强力坐标系办理多少成绩的计算机程序：想想一页又一页繁琐的代数计算，AlphaGeometry 不是这样做的，它像人类学生一样使用带有角度和相似三角形的经典多少规矩。」
最近一段时间，金融科技公司 XTX Markets 设立了人工智能奥林匹克数学奖（AI-MO Prize），旨在鼓励可能进行数学推理的人工智能模型的开发。由于每个奥林匹克比赛都有六个成绩，其中只有两个通常集中在多少上，因此 AlphaGeometry 只能应用于给定奥林匹克比赛中的三分之一成绩。
尽管如此，AlphaGeometry 仅靠自己的多少解题威力就成为了世界上第一个可能在 2000 年和 2015 年通过 IMO 铜牌门槛的人工智能模型。
DeepMind 已在着手推进下一代人工智能体系的推理。研究人员认为，鉴于利用大规模分解数据从头开始训练人工智能体系的广泛潜力，这种格式可能会影响未来人工智能体系发现数学及其他领域新知识的方向。
AlphaGeometry 开创了人工智能数学推理的先河 —— 从探索纯数学之美到使用言语模型办理数学和科学成绩。人们希望这种技术可能继续提升，进而办理更高级、抽象的数学成绩。
而在数学之外，AlphaGeometry 的影响或许还可以覆盖到包含多少成绩的更多领域，如计算机视觉、建筑，甚至理论物理学等。
参考内容：
https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/