数学领域的“AlphaGo”：DeepMind最新AI模型，打破奥数天花板

导读

今日，DeepMind再有新动作，这一次聚焦到奥林匹克竞赛领域。

DeepMind与纽约大学计算机科学系联手在《自然》（Nature）杂志上发布一项研究成果，研究团队研发了一款名为AlphaGeometry的人工智能（AI）系统。该AI模型成功解答了国际数学奥林匹克竞赛级别的几何问题，表现超越了以往最佳的自动化定理证明系统。

与以往不同的是，AlphaGeometry通过在不同复杂级别综合数百万个定理和证明，成功摆脱了对人类演示的依赖。

2016年，DeepMin的推出的AlphaGo打遍围棋界无敌手，这一次，AI能否再次在数学领域超越人类呢？

周    晨 | 撰文

很多人认为，数学或许是验证人类逻辑思维能力的一个可靠参照模板。

在数学领域，证明数学定理一直是人类自动推理能力阈值的一大证明，而奥林匹克数学竞赛，则无疑是对于逻辑极限能力的挑战。

在过去，人类的高水平逻辑推理能力被认为是AI难以取代的，因为将人类逻辑证明的思路转化为机器可验证格式的成本一直很高。奥数水平的数学定理证明对逻辑推理和解题能力要求极高，而目前基于机器学习的AI系统在这方面仍然面临挑战，因为缺乏人类示范作为训练数据，特别是在几何学定理方面，机器学习的AI难以掌握这个领域。 

1月18日，DeepMind联合纽约大学计算机科学系提出了一种名为AlphaGeometry的创新AI模型方法，使得AI模型能够在无需人类示范的情况下学习和解决复杂问题。

AlphaGeometry能够通过综合复杂程度各异的数百万条定理和证明，利用一个神经语言模型完成自我训练。这种方法结合符号演绎引擎（能搜索难题中的大量分支点），能让AI模型在无需人类直接输入的情况下学习并解开复杂问题。

AlphaGeometry合成数据生成流程

可以说，该模型通过在不同复杂性级别上综合数百万个定理和证明，成功地摆脱了对人类演示的依赖。 

为了测试该模型的有效性，研究团队用国际数学奥林匹克竞赛（优等高中生参加的数学定理证明大赛）2000-2020年的30个问题测试了该系统。AlphaGeometry解出了其中25题，接近国际数学奥林匹克竞赛金牌选手的平均表现，而之前最优秀的方法只解出了10题。

AlphaGeometry将几何定理证明器的当前状态从低于人类水平提升到接近金牌水平。

值得一提的是，AlphaGeometry能生成人类可阅读的“证明步骤”，在人类专家的评估下，AlphaGeometry成功解决了IMO 2000和2015的所有几何问题，并且还发现了一个经过推广的IMO定理，这意味着，或许在不久的将来，该模型能够在数学领域刮起一阵让人为之震惊的风暴。

AlphaGeometry的概览，以及它是如何解决一个简单问题和IMO 2015问题3的

虽然目前AlphaGeometry仅限于几何学，但研究团队表示，这种方法或许也能在其他数学领域取得成功。

可以说，这项研究的成果标志着AI领域在解决复杂逻辑挑战方面迈出了重要一步，同时，也意味着未来AI数学研究将迎来全新的可能性。

参考资料

Solving olympiad geometry without human Demonstrations.Nature.

Deep Science预印本