计算机距离自动化数学推理还有多远?
计算机距离自动化数学推理还有多远?
作者:斯蒂芬·奥恩斯 (Stephen Ornes) 2020年8月27日
文章来自于:Quanta Magazine: 查看原文
人工智能工具正在塑造下一代定理证明器,以及数学与机器之间的关系。
引言
据报道,在20世纪70年代,已故数学家保罗·科恩(Paul Cohen)——唯一一位因在数理逻辑方面的工作而获得菲尔兹奖的人——做出了一个影响深远的预测,至今仍在激动和刺激着数学家们:即“在某个未指明的未来时间,数学家将被计算机取代。”科恩因其在集合论中的大胆方法而闻名,他预测所有的数学都可以自动化,包括证明的编写。
证明是一个逐步的逻辑论证,用于验证一个猜想或数学命题的真实性。(一旦被证明,猜想就变成了定理。)它既确立了一个陈述的有效性,也解释了它为什么是真的。然而,证明是奇怪的。它是抽象的,与物质经验脱节。“它们是想象中的、非物质世界与生物进化而来的生物之间的一种疯狂的联系,”卡内基梅隆大学的认知科学家西蒙·德迪奥(Simon DeDeo)说,他通过分析证明的结构来研究数学的确定性。“我们并非为做这件事而进化。”
计算机对于大型计算很有用,但证明需要不同的东西。猜想源于归纳推理——一种关于有趣问题的直觉——而证明通常遵循演绎的、逐步的逻辑。它们往往需要复杂的创造性思维,以及填补空白的更费力的工作,而机器无法实现这种结合。
计算机化的定理证明器可以分为两类。自动定理证明器(Automated theorem provers, ATPs)通常使用强力方法来处理大型计算。交互式定理证明器(Interactive theorem provers, ITPs)则充当证明助手,可以验证论证的准确性并检查现有证明中的错误。但这两种策略,即使结合起来(正如新型定理证明器的情况),也并不等同于自动化推理。
此外,这些工具并未受到张开双臂的欢迎,大多数数学家不使用或不欢迎它们。“对于数学家来说,它们非常有争议,”德迪奥说。“他们中的大多数人不喜欢这个想法。”
该领域一个艰巨的开放挑战是:证明的制作究竟能在多大程度上实现自动化?一个系统能否生成一个有趣的猜想并以人们能理解的方式证明它?来自世界各地实验室的一系列最新进展提出了人工智能工具可能回答这个问题的方法。布拉格捷克信息学、机器人学和控制论研究所的约瑟夫·乌尔班(Josef Urban)正在探索各种使用机器学习来提高现有证明器效率和性能的方法。今年7月,他的团队报告了一组由机器生成和验证的原创猜想和证明。而在6月,由克里斯蒂安·塞格迪(Christian Szegedy)领导的谷歌研究小组发布了利用自然语言处理优势使计算机证明在结构和解释上更像人类的最新成果。
一些数学家将定理证明器视为训练本科生编写证明的潜在颠覆性工具。另一些人则表示,让计算机编写证明对于推进数学来说既不必要,也可能是不可能的。但是,一个能够预测有用猜想并证明新定理的系统将实现一些新的东西——某种机器版本的理解,塞格迪说。而这暗示了自动化推理本身的可能性。
有用的机器
数学家、逻辑学家和哲学家长期以来一直在争论创造证明的哪一部分是根本上属于人类的,关于机械化数学的辩论至今仍在继续,尤其是在连接计算机科学和纯粹数学的深谷中。
对于计算机科学家来说,定理证明器没有争议。它们提供了一种严格的方法来验证程序是否有效,而关于直觉和创造力的争论远不如找到解决问题的有效方法重要。例如,在麻省理工学院,计算机科学家亚当·奇利帕拉(Adam Chlipala)设计了定理证明工具,用于生成密码算法——传统上由人类编写——以保护互联网交易。他的团队的代码已经被用于谷歌Chrome浏览器上的大部分通信。
约翰霍普金斯大学的艾米莉·里尔在教学中使用定理证明器,并在自己的研究中使用证明助手。“使用证明助手改变了我对编写证明的思考方式,”她说。 ——威尔·柯克/约翰霍普金斯大学
“你可以用一个工具编写任何类型的数学论证,并将你的论证连接起来,创建安全性的证明,”奇利帕拉说。
在数学领域,定理证明器帮助产生了复杂的、计算量大的证明,否则这些证明可能会占用数学家数百年的生命。描述最佳堆叠球体(或者历史上是橙子或炮弹)方式的开普勒猜想提供了一个有说服力的例子。1998年,托马斯·黑尔斯(Thomas Hales)和他的学生萨姆·弗格森(Sam Ferguson)一起,使用各种计算机化的数学技术完成了一个证明。结果是如此繁琐——结果占用了3GB——以至于12位数学家花了数年时间分析它,然后才宣布他们有99%的把握认为它是正确的。
开普勒猜想并不是唯一一个由机器解决的著名问题。四色定理指出,任何二维地图只需要四种颜色就可以保证没有两个相邻区域共享同一种颜色,该定理于1977年由数学家使用一个计算机程序解决,该程序穷举了所有五色地图,证明它们都可以简化为四色。而在2016年,三位数学家使用计算机程序证明了一个长期存在的开放挑战,称为布尔毕达哥拉斯三元组问题,但该证明的初始版本大小为200TB。使用高速互联网连接,一个人需要三个多星期才能下载完它。
复杂的情感
这些例子常常被誉为成功,但它们也加剧了争论。证明四色定理的计算机代码(该定理在40多年前就已解决)是人类无法自行检查的。“从那时起,数学家们就一直在争论这到底算不算一个证明,”哥伦比亚大学的数学家迈克尔·哈里斯(Michael Harris)说。
许多数学家,如哥伦比亚大学的迈克尔·哈里斯,不同意计算机化定理证明器是必要的——或者它们将使人类数学家过时的观点。 ——贝阿特丽斯·安托林 (Béatrice Antolin)
另一个抱怨是,如果数学家想使用定理证明器,他们必须首先学习编程,然后弄清楚如何用计算机友好的语言表达他们的问题——这些活动分散了做数学的精力。“等我把我的问题重新组织成能适应这种技术的形式时,我自己就已经解决了这个问题,”哈里斯说。
许多人只是觉得在他们的工作中不需要定理求解器。“他们有一套系统,那就是铅笔和纸,而且行之有效,”伦敦帝国理工学院的数学家凯文·巴泽德(Kevin Buzzard)说,他三年前将工作重心从纯粹数学转向定理证明器和形式化证明。“计算机为我们做了惊人的计算,但它们从未独立解决过一个难题,”他说。“在此之前,数学家是不会买账的。”
但巴泽德和其他人认为也许他们应该接受。首先,“计算机证明可能并不像我们想象的那么陌生,”德迪奥说。最近,他与现就职于斯坦福大学的计算机科学家斯科特·维泰里(Scott Viteri)一起,逆向工程分析了一些著名的经典证明(包括欧几里得《几何原本》中的一个)和数十个使用名为Coq的定理证明器编写的机器生成证明,以寻找共同点。他们发现机器证明的网络结构与人类证明的结构惊人地相似。他说,这种共同的特性可能有助于研究人员找到一种方法,让证明助手在某种意义上能够解释自己。
“机器证明可能并不像看起来那么神秘,”德迪奥说。
其他人则表示,定理证明器可以成为有用的教学工具,无论是在计算机科学还是数学领域。在约翰霍普金斯大学,数学家艾米莉·里尔(Emily Riehl)开发了学生使用定理证明器编写证明的课程。“它迫使你非常有条理、清晰地思考,”她说。“第一次写证明的学生可能不知道自己需要什么,也难以理解逻辑结构。”
里尔还表示,她也越来越多地在自己的工作中使用定理证明器。“它不一定是需要一直使用的东西,也永远不会取代在纸上涂写,”她说,“但使用证明助手改变了我对编写证明的思考方式。”
定理证明器也提供了一种保持该领域诚实性的方法。1999年,俄裔美国数学家弗拉基米尔·沃埃沃德斯基(Vladimir Voevodsky)发现了他一个证明中的错误。从那时起直到2017年去世,他一直是使用计算机检查证明的积极倡导者。黑尔斯说,他和弗格森在用计算机检查他们最初的证明时发现了数百个错误。即使是欧几里得《几何原本》中的第一个命题也不是完美的。如果机器能帮助数学家避免这类错误,为什么不利用它呢?(实践上的反对意见,无论合理与否,正是哈里斯提出的那个:如果数学家必须花费时间将数学形式化以便计算机理解,那这些时间就没有花在做新的数学上。)
但是,剑桥大学的数学家、菲尔兹奖得主蒂莫西·高尔斯(Timothy Gowers)想走得更远:他设想未来定理证明器将取代主要期刊的人类审稿人。“我可以看到这成为标准做法,即如果你想让你的论文被接受,你必须让它通过自动检查器,”他说。
与计算机对话
但在计算机能够普遍检查甚至设计证明之前,研究人员首先必须清除一个重大的障碍:人类语言和计算机语言之间的沟通障碍。
今天的定理证明器并非为方便数学家而设计。第一类,ATPs,通常用于检查一个陈述是否正确,常常通过测试可能的情况。例如,要求一个ATP验证一个人可以从迈阿密开车到西雅图,它可能会搜索所有通过道路连接迈阿密的城市,并最终找到一个有道路通往西雅图的城市。
并非所有数学家都讨厌定理证明器。剑桥大学的蒂莫西·高尔斯认为它们有一天可能会取代数学期刊的人类审稿人。 阿贝尔奖
使用ATP,程序员可以编写所有的规则,或称公理,然后询问某个特定的猜想是否遵循这些规则。然后计算机完成所有工作。“你只需输入你想证明的猜想,然后希望你能得到答案,”计算机科学家丹尼尔·黄(Daniel Huang)说,他最近离开加州大学伯克利分校去一家初创公司工作。
但问题在于:ATP不做的是解释它的工作。所有的计算都在机器内部进行,对人类的眼睛来说,它看起来就像一长串0和1。黄说,扫描证明并理解其推理过程是不可能的,因为它看起来像一堆随机数据。“没有人能看着那个证明然后说,‘我懂了’,”他说。
第二类,ITPs,拥有包含多达数万个定理和证明的庞大数据集,它们可以扫描这些数据集来验证一个证明是否准确。与在某种黑箱中操作并只吐出一个答案的ATP不同,ITP需要人类的交互甚至一路上的指导,所以它们并非那么难以接近。“人类可以坐下来理解证明层面的技术是什么,”黄说。(这些是德迪奥和维泰里研究的那种机器证明。)
ITPs近年来变得越来越流行。2017年,解决布尔毕达哥拉斯三元组问题的三人组使用了Coq(一个ITP)来创建和验证他们证明的形式化版本;2005年,微软剑桥研究院的乔治·冈希尔(Georges Gonthier)使用Coq形式化了四色定理。黑尔斯也在开普勒猜想的形式化证明中使用了名为HOL Light和Isabelle的ITP。(“HOL”代表“高阶逻辑”。)
当今该领域的前沿努力旨在将学习与推理相结合。它们通常将ATP与ITP结合起来,并集成机器学习工具以提高两者的效率。他们设想ATP/ITP程序能够像人类一样进行演绎推理——甚至交流数学思想——或者至少以类似的方式。
推理的极限
约瑟夫·乌尔班认为,证明所需的演绎推理和归纳推理的结合可以通过这种组合方法实现。他的团队已经构建了由机器学习工具引导的定理证明器,这使得计算机能够通过经验自主学习。在过去几年中,他们探索了使用神经网络——帮助机器通过粗略模拟我们大脑神经元活动来处理信息的计算层。今年7月,他的团队报告了由一个在定理证明数据上训练的神经网络生成的新猜想。
乌尔班的部分灵感来自于安德烈·卡帕西(Andrej Karpathy),几年前他训练了一个神经网络来生成看起来像数学但实则无意义的内容,这些内容对非专家来说看起来是合法的。然而,乌尔班不想要无意义的内容——他和他的团队反而设计了自己的工具,在对数百万个定理进行训练后寻找新的证明。然后他们使用该网络生成新的猜想,并使用名为E的ATP检查这些猜想的有效性。
该网络提出了超过50,000个新公式,尽管数万个是重复的。“看来我们目前还不能证明更有趣的猜想,”乌尔班说。
谷歌研究的塞格迪将自动化计算机证明中的推理挑战视为一个更大领域的子集:自然语言处理,这涉及对词语和句子使用模式的识别。(模式识别也是塞格迪之前在谷歌负责的计算机视觉项目背后的驱动思想。)像其他团队一样,他的团队希望定理证明器能够找到并解释有用的证明。
受到像AlphaZero这样的人工智能工具(DeepMind的程序,可以在国际象棋、围棋和日本将棋中击败人类)快速发展的启发,塞格迪的团队希望利用语言识别的最新进展来编写证明。他说,语言模型可以展示出惊人可靠的数学推理能力。
他在谷歌研究的团队最近描述了一种使用语言模型——通常使用神经网络——来生成新证明的方法。在训练模型识别已知为真的定理中的一种树状结构后,他们进行了一种自由形式的实验,简单地要求网络在没有任何进一步指导的情况下生成并证明一个定理。在数千个生成的猜想中,大约13%既可证明又是新的(意味着它们没有重复数据库中的其他定理)。他说,这个实验表明神经网络可以自学某种对证明样貌的理解。
“神经网络能够发展出一种人工的直觉风格,”塞格迪说。
当然,目前尚不清楚这些努力是否会实现科恩40多年前的预言。高尔斯曾表示,他认为到2099年计算机将能够超越数学家的推理能力。他预测,起初,数学家将享受一个某种意义上的黄金时代,“数学家做所有有趣的部分,计算机做所有枯燥的部分。但我认为这只会持续很短的时间。”
毕竟,如果机器继续改进,并且它们能够访问大量数据,它们也应该会变得非常擅长做有趣的部分。“它们将学会自己提出问题/提示,”高尔斯说。
哈里斯不同意。他不认为计算机证明器是必要的,也不认为它们将不可避免地“使人类数学家过时”。他说,即使计算机科学家能够编写出某种合成直觉,它仍然无法与人类的直觉相媲美。“即使计算机能理解,它们的理解方式也与人类不同。”
本文在Spektrum.de上转载了德文版。