计算机离数学推理自动化还有多远？

20世纪70年代，已故数学家保罗·科恩(Paul Cohen)是唯一位因在数理逻辑方面的工作而获得菲尔兹奖(Fields Medal)的人。据报道，他做出了一个令数学家们继续兴奋和恼火的全面预测--“在未指明的未来某个时候，数学家将被计算机取代。”科恩以其大胆的集合论方法而闻名，他预言所有的数学都可以自动化，包括写证明。

证明是一种循序渐进的逻辑论证，用来验证猜想或数学命题的真实性。(一旦被证明，猜想就变成了定理。)。它既确立了陈述的有效性，又解释了为什么它是真实的。然而，证据是奇怪的。它是抽象的，不受物质经验的束缚。卡内基梅隆大学(Carnegie Mellon University)的认知科学家西蒙·迪奥(Simon Deo)说，“它们是想象中的非物理世界和生物进化生物之间的疯狂联系。”他通过分析证据的结构来研究数学确定性。“我们进化不是为了做这件事。”

计算机对于大型计算很有用，但是证明需要一些不同的东西。猜想源于归纳推理--关于一个有趣问题的一种直觉--证明通常遵循演绎、循序渐进的逻辑。它们往往需要复杂的创造性思维，以及更费力的填补空白的工作，而机器无法实现这种结合。

计算机化的定理证明器可以分为两类。自动定理证明器，或称ATP，通常使用暴力方法来处理大型计算。交互式定理证明器，或ITP，充当证明助手，可以验证论点的准确性，并检查现有证明是否有错误。但是，这两种策略即使组合在一起(就像较新的定理证明器那样)，也不能构成自动推理。

此外，这些工具还没有得到广泛的欢迎，大多数数学家既不使用也不欢迎它们。“它们对数学家来说是非常有争议的，”德迪奥说。“他们中的大多数人都不喜欢这个想法。”

该领域的一个令人敬畏的公开挑战是，实际上可以在多大程度上自动进行证明：系统能否生成有趣的猜想，并以人们理解的方式进行证明？来自世界各地实验室的一系列最新进展表明，人工智能工具可能会回答这个问题。布拉格捷克信息、机器人和控制学研究所的Josef Urban正在探索各种方法，利用机器学习来提高现有证明人的效率和表现。今年7月，他的团队报告了一组由机器生成和验证的原始猜想和证明。今年6月，由克里斯蒂安·塞格迪(Christian Szegedy)领导的谷歌研究小组(Google Research)公布了利用自然语言处理的优势，使计算机校样在结构和解释上看起来更人性化的最新结果。

一些数学家将定理证明者视为一种潜在的改变游戏规则的工具，用来训练本科生撰写证明。其他人说，让计算机来编写证明对于提高数学来说是不必要的，而且很可能是不可能的。但是，Szegedy说，一个可以预测有用的猜测并证明新定理的系统将实现一些新的东西-某种机器版本的理解。这表明了自动推理本身的可能性。

数学家、逻辑学家和哲学家长期以来一直在争论，创建证明的哪一部分基本上是人类的，关于机械化数学的争论至今仍在继续，特别是在连接计算机科学和纯数学的深谷中。

对于计算机科学家来说，定理证明者是没有争议的。他们提供了一种严格的方法来验证程序是否有效，而关于直觉和创造力的争论没有找到有效的方法来解决问题那么重要。例如，在麻省理工学院(Massachusetts Institute Of Technology)，计算机科学家亚当·奇利帕拉(Adam Chlipala)设计了定理证明工具，这些工具可以生成密码算法-传统上由人类编写-来保护互联网交易。他的团队的代码已经用于谷歌Chrome浏览器上的大部分通信。

Chlipala说：“你可以接受任何类型的数学论点，并用一个工具对其进行编码，然后将你的论点连接在一起，创建安全性的证据。”

在数学中，定理证明者帮助产生了复杂的、计算量大的证明，否则这些证明将占据数学家数百年的生命。开普勒猜想描述了堆积球体(或历史上的橙子或炮弹)的最佳方式，提供了一个生动的例子。1998年，托马斯·黑尔斯(Thomas Hales)和他的学生萨姆·弗格森(Sam Ferguson)使用各种计算机化的数学技术完成了一个证明。结果是如此繁琐-结果占用了3G的空间-12位数学家分析了几年后才宣布他们99%确定它是正确的。

开普勒猜想并不是唯一一个被机器解决的著名问题。四色定理说，你只需要四个色调就可以给任何二维地图上色，这样相邻的两个区域就不会共享一种颜色。1977年，数学家们使用一个计算机程序解决了这个问题，该程序在五色地图中翻来覆去，表明它们都可以减少到四个。2016年，三位数学家使用计算机程序证明了一个名为布尔毕达哥拉斯三重问题(Boolean Pythagorean Triples Problem)的长期悬而未决的挑战，但最初的证明版本是200TB。有了高速互联网连接，一个人可以在三周多一点的时间内下载它。

这些例子经常被吹捧为成功，但它们也增加了争论。证明四色定理的计算机代码是在40多年前确定的，人类不可能自己检查。哥伦比亚大学数学家迈克尔·哈里斯(Michael Harris)说：“从那以后，数学家们就一直在争论这是否是证据。”

另一个抱怨是，如果数学家想要使用定理证明器，他们必须首先学习编码，然后弄清楚如何用计算机友好的语言来表达他们的问题-这些活动有损于做数学的行为。哈里斯说：“当我把我的问题重新设计成一种适合这项技术的形式时，我自己就已经解决了这个问题。”

许多人在他们的工作中就是看不到需要定理解算器。伦敦帝国理工学院(Imperial College London)数学家凯文·巴扎德(Kevin Buzzard)说，“他们有一个系统，就是纸和笔，而且很管用。”三年前，他的工作从纯数学转向专注于定理证明者和形式证明。他说：“计算机为我们做了令人惊叹的计算，但它们从来没有自己解决过一个难题。”“在他们这么做之前，数学家是不会相信这些东西的。”

但巴扎德和其他人认为或许他们应该这么做。首先，“电脑校样可能并不像我们想象的那么陌生，”DeDeo说。最近，他与现就职于斯坦福大学的计算机科学家斯科特·维特里(Scott Viteri)一起，对几个著名的正则证明(包括一个来自欧几里德元素的证明)和几十个机器生成的证明进行了逆向工程设计，这些证明是用一种名为Coq的定理证明器编写的，目的是寻找共性。他们发现，机器打样的网络结构与人做的打样结构惊人地相似。他说，这种共同的特征可能会帮助研究人员找到一种方法，让证据助手在某种意义上解释自己。

其他人说，定理证明者在计算机科学和数学中都可以成为有用的教学工具。在约翰霍普金斯大学，数学家艾米丽·里尔(Emily Riehl)开发了一些课程，让学生使用定理证明器写出证明。“它迫使你非常有条理，思维清晰，”她说。“第一次写校样的学生可能很难知道他们需要什么，也很难理解逻辑结构。”

里尔还说，她在自己的工作中越来越多地使用定理证明者。“这不一定是你必须一直使用的东西，也永远不会取代在一张纸上乱涂乱画，”她说，“但使用校样助手改变了我写校样的方式。”

定理证明者还提供了一种保持字段诚实的方法。1999年，俄裔美国数学家弗拉基米尔·沃沃茨基(Vladimir Voevodsky)在他的一个证明中发现了一个错误。从那时起到2017年去世，他一直是使用电脑检查证据的直言不讳的支持者。黑尔斯说，他和弗格森在用电脑检查原始证明时发现了数百个错误。甚至欧几里得元素中的第一个命题也不是完美的。如果机器可以帮助数学家避免这样的错误，为什么不利用它呢？(实际的反对意见，无论是否合理，都是哈里斯提出的：如果数学家必须花时间形式化数学才能被计算机理解，那么他们就不会花时间做新的数学。)。

但是，剑桥大学数学家、菲尔兹奖牌获得者蒂莫西·高尔斯(Timothy Gowers)想要走得更远：他展望了未来，定理证明者将取代主要期刊上的人类裁判。他说：“我可以看到，如果你想要你的论文被接受，你必须让它通过自动检查器，这将成为一种标准做法。”

但在计算机可以普遍检查甚至设计证据之前，研究人员首先必须清除一个重大障碍：人类语言和计算机语言之间的沟通障碍。

今天的定理证明者并不是设计成对数学家友好的。第一种类型的ATP通常用于检查语句是否正确，通常是通过测试可能的情况。例如，要求ATP验证一个人是否可以从迈阿密开车到西雅图，它可能会搜索所有由通往迈阿密的道路连接的城市，最终找到一个有道路通往西雅图的城市。

有了ATP，程序员可以在所有规则或公理中编码，然后询问特定的猜测是否遵循这些规则。然后，计算机完成所有的工作。计算机科学家丹尼尔·黄(Daniel Huang)最近离开加州大学伯克利分校(University of California，Berkeley)，前往一家初创公司工作。他说，“你只需输入你想要证明的猜想，就能得到答案。”

但问题是：ATP做不到的是解释它的工作原理。所有的计算都是在机器内进行的，在人眼看来，它看起来就像一长串0和1。黄说，扫描证据并遵循推理是不可能的，因为它看起来像一堆随机数据。他说：“没有人会在看到证据后说，‘我明白了。’”

第二类ITP有大量的数据集，其中包含多达数万个定理和证明，他们可以扫描这些数据来验证证明是准确的。与在一种黑匣子里操作并只吐出答案的ATP不同，ITP需要人与人互动，甚至需要一路上的指导，所以他们不会那么难以接近。“一个人可以坐下来了解什么是证明级技术，”黄说。(这些是DeDeo和Viteri研究的机器校样。)。

近年来，ITP变得越来越受欢迎。2017年，布尔毕达哥拉斯三重问题背后的三人组使用ITP的Coq创建和验证了他们的证明的正式版本；2005年，微软剑桥研究院的Georges Gonthier使用Coq将四色定理形式化。黑尔斯还使用了名为HOL Light和Isabelle的ITP来正式证明开普勒猜想。(“HOL”代表“高阶逻辑”。)。

今天，该领域最前沿的努力旨在将学习与推理结合起来。他们经常将ATP和ITP结合起来，还集成了机器学习工具来提高两者的效率。他们设想的ATP/ITP项目可以使用演绎推理-甚至交流数学思想-与人们一样，或者至少以类似的方式。

约瑟夫·厄本认为，证明所需的演绎推理和归纳推理的结合可以通过这种结合的方式来实现。他的团队已经建立了由机器学习工具指导的定理证明器，这些工具允许计算机通过经验自行学习。在过去的几年里，他们探索了神经网络的使用-通过粗略地近似我们大脑的神经元活动，帮助机器处理信息的计算层。7月份，他的团队报告了一个神经网络根据定理证明数据训练产生的新猜想。

厄本的部分灵感来自安德烈·卡帕西，他几年前训练了一个神经网络，以产生在非专家看来合法的数学外观的胡言乱语。然而，厄本并不想要胡说八道--相反，他和他的团队设计了自己的工具，在对数百万个定理进行培训后，寻找新的证明。然后，他们使用网络生成新的猜想，并使用名为E的ATP检查这些猜想的正确性。

该网络提出了5万多个新公式，尽管有数万个是重复的。厄本说：“看起来我们还没有能力证明更有趣的猜想。”

Google Research的Szegdy认为，计算机证明中自动推理的挑战是一个更大的领域的子集：自然语言处理，它涉及到单词和句子的使用中的模式识别。(模式识别也是计算机视觉背后的驱动力，这也是塞格迪之前在谷歌进行的项目的目标。)。和其他团队一样，他的团队希望定理证明者能够找到并解释有用的证据。

受到AlphaZero等人工智能工具快速发展的启发，DeepMind程序可以在国际象棋中击败人类，围棋和幕府将军的团队希望利用最近在语言识别方面的进展来编写校样。他说，语言模型可以展示令人惊讶的坚实的数学推理。

他在Google Research的团队最近描述了一种使用语言模型(通常使用神经网络)来生成新证据的方法。在训练模型识别已知为真的定理中的一种树状结构后，他们进行了一种自由形式的实验，简单地要求网络在没有任何进一步指导的情况下生成并证明一个定理。在数千个生成的猜想中，大约有13%既是可证明的，又是新的(这意味着它们没有复制数据库中的其他定理)。他说，这项实验表明，神经网络可以自学一种对证明是什么样子的理解。

“神经网络能够发展出一种人工风格的直觉，”塞格迪说。

当然，目前还不清楚这些努力是否会实现科恩40多年前的预言。高尔斯说过，他认为到2099年，计算机将能够超过数学家。一开始，他预测，数学家将享受一种黄金时代，“当数学家做所有有趣的部分，而计算机做所有无聊的部分。”但我认为这将持续很短的时间。“。

毕竟，如果机器继续改进，并且它们可以访问海量数据，它们应该也会变得非常擅长做有趣的部分。高尔斯说：“他们将学习如何按照自己的提示去做。”

哈里斯不同意这种说法。他不认为计算机证明者是必要的，也不认为它们会不可避免地“让人类数学家过时”。他说，即使计算机科学家能够编程出一种合成直觉，它仍然比不上人类。“即使计算机能理解，它们也不能以人类的方式理解。”