《自然》17日发表的一项计算科学研究，描述了一个能解国际数学奥林匹克竞赛级别几何题的人工智能（AI）系统。其表现超过了之前最好的自动化定理证明系统。该研究证明了AI已接近人类破解复杂逻辑问题的最高水平。

　　奥林匹克竞赛中的数学定理证明需要高水平的逻辑推理和解题能力。然而，当前基于机器学习的AI系统在证明数学定理方面还有困难。机器学习通过向计算机提供参考数据，让计算机学习如何执行特定任务。但由于作为训练数据的人类示范很少，所以定理证明，尤其是几何学定理很难被证明。

　　谷歌“深度思维”团队此次描述了一种不需要人类示范的定理证明方法。基于这一方法的AI系统名为“阿尔法几何”（G0）。它综合了复杂程度各异的数百万条定理和证明，并利用一个神经语言模型完成自我训练。这种方法结合符号演绎引擎（能搜索难题中的大量分支点），能让G0在无需人类直接输入的情况下学习并解开复杂问题。

　　团队用国际数学奥林匹克竞赛2000年至2020年间的30个问题测试了该系统。G0解出了其中25题，接近国际数学奥林匹克竞赛金牌选手的平均表现。而之前最优秀的方法只解出了10题。值得一提的是，G0能生成人类可阅读的证明，甚至发现了2004年国际数学奥林匹克竞赛定理的一个新版本。

　　研究人员指出，G0目前仅限于证明几何学定理，但这种方法或许能应用于其他数学领域。

【总编辑圈点】

　　让AI做一个定理证明，其实比让AI来玩围棋、国际象棋等更具挑战性。想要证明一个特定猜想的真假，需要使用高级别的逻辑推理能力。这比其他识别、分类任务要难得多。棋类的走法总会被预测出来，即使算法没有给出最佳方案，结果也能“殊途同归”。但在定理证明中，只要算法有一次走入死胡同，那就宣告本次解答失败，性能再好的系统也没办法。这就是为什么人们一直把数学定理证明视为构建智能机器的关键能力，也是为什么这项成果意义重大的原因。