新AI，可以求解复杂的几何问题！

AlphaGeometry，这是DeepMind的研究人员最新开发的人工智能系统，它能以接近国际数学奥林匹克的人类金牌得主的水平，解决国际奥数中的几何问题。这是以前的人工智能难以做到的，标志着人工智能性能的一项重大突破。研究人员在《自然》杂志的一篇论文中，详细介绍了这一人工智能系统。

充满挑战的领域

对定理进行证明是一种非凡的解决问题的技能，它彰显了对逻辑推理的掌握，以及在无限的可能性中搜索目标的能力。自20世纪50年代以来，追求更好的定理证明能力便成了人工智能研究的焦点。

数学奥林匹克竞赛是世界上最著名的定理证明竞赛，其悠久的历史可以追溯到1959年。现在，这项由世界上最优秀的中学生参与的现代竞技，不仅展示了年轻人的才能，而且也成为先进的人工智能系统在数学和推理方面的试验场。

然而，目前的机器学习方法并不适用于大多数数学研究领域，因为将人类证明转换为可被机器验证的格式的成本很高。几何领域的问题尤为严重，因为它面临独特的翻译挑战，导致训练数据严重稀缺。

神经符号系统

AlphaGeometry是一个神经符号系统，它将神经语言模型的预测能力，与以规则为基准的符号推演引擎巧妙地结合了起来，这二者可以相互配合，寻找复杂的几何定理的证明。

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

因此在AlphaGeometry中，有一个系统可以提供快速的、直观的想法，另一个系统提供更深思熟虑的、理性的解决方案。这可能正是它强大的原因。

大规模的合成数据

我们知道，几何依赖于对空间、距离、形状和相对位置的理解，是艺术、建筑、工程和许多领域的基础。人们用纸和笔来学习和研究几何，利用现有的知识来发现新的、更复杂的几何性质和几何关系。

为了能大规模地模拟这一知识构建过程，DeepMind的研究团队通过综合大量的有着不同复杂程度的定理和证明，生成了大量的合成数据，可以在没有任何人工示范的情况下利用这些数据，从头开始训练AlphaGeometry。

由AlphaGeometry生成的合成数据的可视化表示。

具体来说，系统首先会生成10亿个几何对象的随机图，并详尽地推导出每个图中的点和线之间的所有关系。然后，AlphaGeometry会找到每个图中包含的所有证明，再往回运转，找出需要哪些额外的结构来获得这些证明。这一过程被称为“符号推演与回溯”。

这个庞大的数据池经过过滤，筛除了相似的示例，最终得到了一个由1亿个不同难度的示例组成的训练数据集，其中有900万个特征添加了构造。

应对奥数几何问题

国际奥林匹克几何题是基于图形的，在解决这些图形之前需要添加新的几何结构，比如点、线或圆。有了这么多的示例，AlphaGeometry的语言模型就能够在面对奥数几何问题时，为新的构造给出很好的建议。

在一组有30道几何题的数学奥林匹克竞赛测试中，AlphaGeometry在标准的奥林匹克时限内解决了25个问题。相比之下，此前的最先进系统解决了10个这样的几何问题，而人类金牌得主平均解决25.9个问题。

从2000年到2022年的30个奥林匹克几何问题的基准测试集中，AlphaGeometry在比赛时限内解决了25个问题，接近人类金牌得主的水平。之前最先进的方法，被称为“吴消元法”，解决了10个问题。（图/DeepMind）

AlphaGeometry提供的每道奥数题的解，都经过了计算机的检查和验证，并且还被拿来与之前的人工智能方法以及人类在奥数上的表现进行了比较。可以说，AlphaGeometry在解决奥数几何问题的能力上，接近人类的顶级表现。

期待新的可能性

解决奥林匹克级别的几何问题，是在通往更先进和更通用的人工智能系统的道路上发展深度数学推理的一个重要里程碑。通过AlphaGeometry，研究人员展示了人工智能不断增长的逻辑推理能力，以及发现和验证新知识的能力。

现在，他们正在开源AlphaGeometry代码和模型，并希望与合成数据生成和训练中的其他工具和方法一起，帮助在数学、科学和人工智能领域开辟新的可能性。