谷歌推几何AI系统AlphaGeometry，实力达奥林匹克金牌得主

计划重点:

⭐️ AI 系统超越了当前几何问题的最新方法，推动了数学领域的 AI 推理

⭐️ AlphaGeometry 在标准预设时间限制内解决了25个奥赛级几何问题

⭐️通过结合语言神经模型和规则推理引擎，AlphaGeometry实现了逻辑推理的新里程碑

Google DeepMind 发布了一个名为AlphaGeometry 的人工智能系统，它可以解决复杂的几何问题，其水平接近人类奥林匹克金牌得主——这是人工智能性能的突破。在对30道奥数几何题的基准测试中，AlphaGeometry 在标准奥数时限内解决了25道。相比之下，之前最先进的系统解决了其中10个几何问题，而人类金牌得主平均解决了25.9个问题。

由于缺乏推理技能和训练数据，人工智能系统经常难以解决几何和数学中的复杂问题。AlphaGeometry 的系统将神经语言模型的预测能力与规则约束推演引擎相结合，协同工作以找到解决方案。通过开发一种方法来生成大量的合成训练数据（1亿个独特的示例），我们可以在没有任何人类演示的情况下训练 AlphaGeometry，从而避开数据瓶颈。

AlphaGeometry 采用神经符号方法

AlphaGeometry 是一个神经符号系统，由神经语言模型和符号推演引擎组成，它们共同努力寻找复杂几何定理的证明。类似于“思考，快和慢”的理念，一个系统提供快速、“直观”的想法，而另一个系统则提供更加深思熟虑、理性的决策。

由于语言模型擅长识别数据中的一般模式和关系，因此它们可以快速预测潜在有用的结构，但通常缺乏严格推理或解释其决策的能力。另一方面，符号演绎引擎基于形式逻辑并使用明确的规则来得出结论。它们是理性且可解释的，但它们可能“缓慢”且不灵活——尤其是在独自处理大型、复杂的问题时。

AlphaGeometry 的语言模型引导其符号推导引擎寻找几何问题的可能解决方案。奥林匹克几何问题基于图表，需要添加新的几何结构才能解决，例如点、线或圆。AlphaGeometry 的语言模型可以从无数种可能性中预测添加哪些新结构最有用。这些线索有助于填补空白，并允许符号引擎对图表进行进一步推论并接近解决方案。

生成1亿个综合数据示例

几何依赖于对空间、距离、形状和相对位置的理解，是艺术、建筑、工程和许多其他领域的基础。人类可以使用笔和纸来学习几何，检查图表并使用现有知识来发现新的、更复杂的几何属性和关系。研究人员的合成数据生成方法大规模模拟了这种知识构建过程，使我们能够从头开始训练 AlphaGeometry，而无需任何人类演示。

使用高度并行计算，系统首先生成十亿个几何对象的随机图，并详尽地推导出每个图中点和线之间的所有关系。AlphaGeometry 找到了每个图表中包含的所有证明，然后向后工作以找出需要哪些附加构造（如果有）来得出这些证明。我们把这个过程称为“符号推演与回溯”。

这个庞大的数据池被过滤以排除类似的示例，从而产生了包含1亿个不同难度的独特示例的最终训练数据集，其中900万个具有添加的结构。有了这么多关于这些结构如何产生证明的例子，AlphaGeometry 的语言模型能够在遇到奥林匹克几何问题时为新结构提出很好的建议。

开创性地利用人工智能进行数学推理

AlphaGeometry 提供的每一道奥数题的解法都经过计算机检查和验证。研究人员还将其结果与之前的人工智能方法以及人类在奥林匹克竞赛中的表现进行了比较。此外，数学教练、前奥林匹克金牌得主 Evan Chen 为我们评估了 AlphaGeometry 的一系列解决方案。

过去针对基于证明的竞争问题的人工智能解决方案有时是偶然的（输出有时是正确的，需要人工检查）。AlphaGeometry 没有这个弱点:它的解决方案具有机器可验证的结构。尽管如此，它的输出仍然是人类可读的。人们可以想象一个通过强力坐标系解决几何问题的计算机程序:想想一页又一页繁琐的代数计算。AlphaGeometry 不是那样的。它像学生一样使用带有角度和相似三角形的经典几何规则。”

由于每个奥林匹克竞赛都有六个问题，其中只有两个通常集中在几何上，因此 AlphaGeometry 只能应用于给定奥林匹克竞赛中的三分之一问题。尽管如此，仅其几何能力就使其成为世界上第一个能够在2000年和2015年通过 IMO 铜牌门槛的人工智能模型。

在几何方面，我们的系统接近 IMO 金牌得主的标准，但研究人员着眼于更大的奖项:推进下一代人工智能系统的推理。鉴于利用大规模合成数据从头开始训练人工智能系统的更广泛潜力，这种方法可能会影响未来人工智能系统如何发现数学及其他领域的新知识。

AlphaGeometry 建立在 Google DeepMind 和 Google Research 的工作基础上，开创了人工智能数学推理的先河——从探索纯数学之美到使用语言模型解决数学和科学问题。研究人员最近推出了FunSearch，它首次使用大型语言模型在数学科学的开放问题中取得了发现。

模型代码:https://github.com/google-deepmind/alphageometry

论文网址:https://www.nature.com/articles/s41586-023-06747-5