Josef Urban谈机器学习和自动推理

路加福音Muehlhauser:在Urban & Vyskocil (2013)而其他的文章，你写的是关于数学形式化和自动定理证明的艺术状态。在我问关于机器学习的问题之前，您能不能快速总结一下，在这个阶段，当涉及到自动定理证明时，我们能做什么和不能做什么?

约瑟夫城市最著名的结果是罗宾斯猜想的证明是由Bill McCune的系统金宝博官方EQP．自动定理证明(ATP)今天可以用于解决一些开放方程代数问题，例如拟群和环路理论．这种公开问题的证据可能是数千次推断，并且与数学家产生的证据完全不同。解决ATP的这些问题通常不是“按钮”的问题。它可能需要特定的问题重构（通常仅涉及几个公理），适合于ATP，对ATP搜索的合适参数的探索，有时还指导LEMMAS（“提示”）的最终证明尝试，这对于解决更简单的相关问题是有用的．

ATP今天也被用于证明大型正式库中的小引理，这些库由交互式定理证明程序(ITPs)开发，如Mizar、Isabelle和HOL Light。这被称为“大理论”ATP。在过去的十年里,我们已经发现,即使大数学库(成千上万的定义和定理)使用在这些itp,通常可以从这些库和自动选择相关的先前知识发现证明小前题自动无需任何人工预处理。这样的证明通常比方程代数问题的长证明要短得多，但即使这样，对于使用ITPs来正式证明更高级的定理的人来说，已经有很大的帮助。

一个说明性的例子是留下的污点(“开普勒的正式证明”)项目的负责人汤姆·黑尔斯(Tom Hales)在1998年证明了开普勒猜想。证明是如此复杂，以至于确保其正确性的唯一方法是使用ITP进行正式验证。汤姆·黑尔斯最近写了一本300页的书大多数概念、引理和证明都有一个计算机可理解的“Flyspeck”对应物，并在HOL Light中声明和验证。黑尔斯估计这花费了大约20人年的时间。最近,我们有显示在14000个小的Flyspeck引理中，大约47%的证明可以通过大理论ATP方法自动找到。这意味着唯一需要的心理努力就是在HOL Light中正式地陈述这些引理。同样，需要注意的是，从库中已经存在的其他引理中证明引理必须非常容易。另一方面，这意味着一旦我们有了如此大规模的正式陈述的日常数学语料库，就有可能将该语料库与大理论ATP方法一起使用来解决许多简单的正式陈述的数学问题。

另一个有趣的最新发展是ATP方法，它有效地结合了“推理”和“计算”。这对ATP系统来说是一个长期的挑战，特别是在软件和硬件验证时。金宝博官方最近的SMT(可满足模理论)系统如金宝博官方Z3集成一些决策程序，典型的关于线性和非线性算法，位向量等。我不是这方面的专家，但我的印象是，这种系统的日益强大使对复杂的硬件和软件系统的全面正式验证越来越现实。金宝博官方

路加福音：当您看到它时，限制ATP算法的成功和范围最重要的因素是什么？

约瑟夫:(1)他们的推理能力低下，特别是在大型和先进的理论中;(2)缺乏计算机对当前人类水平(数学)知识的理解。

造成(1)的主要原因是，迄今为止，一般(“通用”)推理算法经常使用过多的蛮力，没有太多的智能指导，具体子问题的具体方法，以及自我完善的方法。即使是在被认为相当简单的数学问题上，这种蛮力算法也经常爆发。(2)是一个主要的障碍，因为即使ATP算法的强度已经可以用于普通数学中的简单的查询回答应用，系统仍然不能理解使用人类水平的数学语言和概念提出的问题。金宝博官方(1)和(2)是相连的:人类的数学散文可以是任意高级的，仅仅为了解析和填补论证的空白，就需要发现长长的推理链。

改进方法之一是对数学家的思维方式进行更好的(最好是自动化的)分析。换句话说，通过挖掘和理解他们知道什么，他们如何使用和产生它，以及他们如何提高他们的知识和推理方法。如果这是正确的，那么至少可以正确解析(可能是“注释”)格式的大型数学知识语料库应该是有用的，然后进一步分析，也许可以用于构建各种自我改进的ATP算法。在某种程度上，这是在过去十年开始的，尽管手动(“理论驱动”)工程的ATP算法仍然在很大程度上盛行。不幸的是，大型“atp可解析”(或注释)语料库在今天仍然非常罕见，而且制作成本很高，这恰恰是因为(2)，即人类水平和计算机水平的理解和推理之间的差距。不用说，双注释的人机数学语料库也应该(与适当的ATP一起)有助于“引导”解决(2)，即，学习越来越多的计算机理解人类水平的数学文本。由于数学是唯一具有深度正式语义学的领域，对这种语料库的研究可能最终还会使我们更好地理解自然语言和为其他科学提供强大的人工智能。

在软件和硬件验证中，(1)可能是主要的问题，尽管，例如，大型代码库的语义注释也是主要的工作。解决(1)仍然是任意困难的，但似乎“代码”一般没有“数学”那么多样化，它可能通过较少的手工编程技术走得很远。

路加福音:有多少人类的数学知识已经形式化，以至于自动定理证明可以使用它?形式化数学的发展速度是多少?

约瑟夫我们的一个指标是创建于1999年的100个定理列表和由Freek Wiedijk跟踪的正式金宝博官方系统．目前，这100个定理中有88%已在至少一个证明助手中被证明，87%仅在HOL Light中被证明。很多本科课程可能已经涵盖了很好的程度:实/复杂微积分的基础知识、测度理论、代数和线性代数、一般拓扑、集合论、范畴论、组合学和图论、逻辑等。但我认为博士级别的覆盖范围还很遥远。

最近有一些高级数学形式化Feit-Thompson定理在Coq中的形式证明，前面已经提到过污点项目由HOL Light完成，开阳中一半以上的连续格的纲目的形式化，以及许多更小更有趣的项目。一些在系统中形式化的定理和理论的概述页是MML查询金宝博官方(开阳)正式证明档案(伊莎贝尔)公鸡contrib， 和100定理项目在Hol光线。

形式数学的发展速度不是很高，但作者的数量也相当低。我粗略估计每年大约有1万到2万顶级引理，其中有100到300个更重要的定理。但是在不同的系统之间，它们的不同的库之间，有时甚至在一个库中都存在大量的重复和重复。金宝博官方人们正在尝试各种形式化方法，有时更喜欢从头开始设计自己的形式化，而不是试图重用别人的工作。这与代码库非常相似。使库尽可能可重用是一项艰巨的工作。

严格地说，目前只有Mizar、Isabelle和HOL Light可以使用大型理论ATP系统，这些系统真正尝试一次性使用整个图书馆来证明新的猜想。金宝博官方Coq的逻辑与最强的ATP系统所用的逻辑更不同，迄今为止，它们之间还没有足够完整的大理论联系。金宝博官方但是在Coq(以及其他交互式验证程序)中也有很多小规模的可编程的自动化验证程序。

路加福音:拥有形式化数学知识的大型数据库的前景自然会引出这样一个问题:“我们是否可以使用机器学习算法来改进自动定理证明?”机器学习在自动定理证明方面的现状如何?

约瑟夫今天，大多数机器学习应用都处于大理论ATP的背景下。在证明一个新猜想时，有最发达的学习方法的任务是从一个大的库中选择最相关的定理和定义。这是重要的原因有两个:(i) ATP今天通常可以很远时足够正确的公理,不冗余,相当接近猜想,和(2)不相关的公理添加到ATP搜索空间往往迅速减少的机会找到证据在合理的时间内。这个选择问题被称为“前提选择”和人们已经尝试了许多学习和非学习算法，并以各种方式结合在一起．从2003年开始尝试的最古老的方法是朴素贝叶斯，但最近我们也尝试了核方法，各种版本的距离加权k-最近邻，随机森林，和一些基本的集成方法。

一个主要问题是选择良好的数学对象，如公式和学习算法的证据。在一个大型的不同库中，只需使用一组符号作为公式功能已经有用。这一直通过纯粹句法N-GRAM类似物（术语和子项及其部分，以各种方式标准化）来扩展这一点，以更具语义，但仍然是完全句法的功能，如添加类型信息和类型层次结构，以强烈语义特征如大型多样化模型中配方的有效性。特征预处理方法，如TF-IDF和潜在语义分析有帮助很多，并且很可能仍然可以完成。

另一个主要问题是用于训练的证据。有些证明对于人类来说很容易，但是对于今天的ATP来说很难，所以如果可能的话，最好找到一个ATP证明并从中学习，而不是试图从形式上正确但ATP不可行的证明中学习。这就产生了一种探索性的AI系统，它将演绎证明、发现和从证明中学习交织金宝博官方在一起。正反馈循环出现:我们发现的ATP证明(以及反例)越多，下一次学习迭代就越好，我们通常在下一次学习建议的证明发现迭代中发现的ATP证明越多。在某种意义上，一个人不能轻易地“只做归纳人工智能(学习)”或“只做演绎人工智能(ATP)”:大理论ATP的最强方法是真正交错定理证明与学习从证明。这应该不会太令人惊讶，因为人类不是通过单纯的归纳或单纯的演绎来进行科学研究的。但对我来说，拥有至少一个允许这种技术和实用实验相结合的人工智能领域似乎真的很有用。

当我们不再把atp当作黑盒来看待，而是开始审视它们的内部时，也会有类似的想法。而不是发展一个善于为猜想选择相关前提的归纳/演绎系统(金宝博官方mal是一个例子)，我们可能尝试发展一个系统，它拥有许多专门的解决问题的技术(ATP金宝博官方策略)，用于常见的问题类别，以及一些关于哪些技术用于哪些问题类别的直觉。一个例子是盲人Strategymaker大图书馆的不同的问题同时共同进化出人口的ATP策略(search-directing参数作为集)培训可以解决的问题,人口的的最终目标有相当小的组策略,共同解决尽可能多的问题。最初的专家策略(“捕食者”)会发生突变，并在它们容易的猎物(它们擅长的简单训练问题)上快速评估，如果突变在这样的训练子集上显示出希望(更快的解决方案)，它们将在更广泛的问题上进行更昂贵的评估(允许更多的时间)，可能解决一些以前无法解决的问题，并把它们变成进一步的培训目标。同样，对迄今为止尚未解决的问题进行随机突变是相当低效的，所以人们确实需要直觉来判断突变应该依赖哪些训练数据。这又产生了一个快速的“归纳”训练阶段，随后(如果成功)是一个较慢的“努力思考”阶段，在这个阶段中，新训练的策略试图解决更多的问题，使它们成为进一步的训练数据。直觉与演绎能力再次协同进化;只做其中一项并不那么有效。

从黑箱到白箱，你也可以问ATP策略和演绎技术到底是什么，以及如何引导/规划它们，而不仅仅是找到问题类的预定义搜索参数的良好组合。有几种学习方法可以超越这种参数设置，最突出和最成功的可能是“提示”方法Bob Veroff(做得也有点不同由斯蒂芬舒尔茨)，将证明搜索指向在相关问题证明中被发现有用的引理(线索)。我相信，学习这样的内在指导仍然是一个有待探索的领域，我们应该努力。人们不仅可以将搜索导向以前有用的引理，还可以基于与其他问题的类比、对问题状态的更深层次的知识等，着眼于提出全新引理和概念的方法。根据人们对什么是机器学习和什么不是机器学习的看法，人们也可以在这里联系到Douglas Lenat关于概念和引理发现系统的开创性工作，如金宝博官方自动化的数学家和Eurikeo.．

路加福音：在未来20年内，您期望该地区有哪些趋势？您是否期望在20年内，更大的研究数学家将使用ATP，至少以高度互动的方式（金宝博娱乐翼Lenat Eurisko) ?您是否期望学习型(而非非学习型)atp在未来占据主导地位?你认为事情会发展到这样的程度吗一些金宝博娱乐研究数学家将被有效地取代，就像一些律师助理(据说）被更好的软件所取代以便通过合法数据库进行搜索？

约瑟夫首先，人工智能预测通常会发生，但通常需要比预期更长的时间。在这些低调的领域，20年真的不算多:Flyspeck本身花了大约20人年，而开星花了40年Andrzej Trybulec富有远见的演讲到目前开元图书馆的1200篇文章。在这些领域并没有很多大型项目，它们往往是由单个研究人员的极端决心推动的。金宝博娱乐

我认为，人工智能在20年内可以取得的一个重大突破是深刻的自动化语义理解(形式化，“机器阅读”)的大多数latex编写的数学教科书。长期以来，这被三个因素所阻碍:(i)缺乏注释正式/非正式语料训练这样的语义解析,(2)缺乏足够大的存储库所需要的数学知识背景”obvious-knowledge填缝”,和(3)缺乏足够强大的large-theory ATP,可以填补缺口的原因使用大量的背景知识存储库。这种情况最近发生了很大的变化，除非我们真的很懒，我相信这种情况会经常发生。它可能不会马上变得完美，也不会在手动规范化的水平上实现，但它将通过使用更多的数据和更好的算法逐步改进，这有点类似于谷歌在英语、西班牙语和德语等语言之间的翻译。一旦它开始自动发生，它可能像滚雪球一样越滚越快，再次感谢更多的“推理数据”变得可访问和数据驱动的大理论ATP和人工智能方法的力量之间的正反馈循环。

我不认为数学家们有任何理由“害怕人工智能”(至少在现在)，恰恰相反:越来越多的人在思考目前计算机理解和数学辅助水平低的问题。冯·诺伊曼、图灵和哥德尔等数学家是我们将计算机和人工智能作为一门学科的首要原因。他们的动机之一是希尔伯特的计划和莱布尼茨式的梦想，即让机器辅助数学和科学推理。在图灵诞生后的一百年里，计算机科学和人工智能对他们的“父母”科学贡献甚少，而且进展如此缓慢，这对他们来说甚至有点遗憾。此时此刻，任何试图编写正式数学的人都在祈祷更好的自动化。没有它，正规化将仍然是一项缓慢、昂贵和微不足道的努力。因此，情况恰恰相反:为了使数学和科学的深层语义处理得以发展，自动化必须得到提高。但是一旦这种对科学的深层语义处理开始发展，这也意味着数学家更容易接触到它。法律只是一个例子;我真的很喜欢约翰·麦卡锡的未来主义笔记形式证明成为各种政策制定的有力标准。需要正式检查的复杂数学证明只是冰山一角:今天，我们正在构建和依赖越来越复杂的机器、硬件、软件、法律、政治和经济系统，它们都有漏洞，很容易被破解和破坏。金宝博官方解决这些问题并让我们能够正确地执行更复杂的设计，对于拥有数学思维的人来说是一个巨大的未来机遇和市场，他们拥有自动化工具，能够在不牺牲正确性的前提下快速取得进展。

我确实预计，在未来的20年里，atp总体上将比现在有更好的模式检测能力，它们将能够更好地积累、处理和有效地使用之前的知识，并更好地将暴力搜索与各种层次的指导相结合。特别是在更高级的数学中，高级启发式的人类启发证明/思考方法可能会开始得到发展。一种尝试自动获取它们的方法是通过计算机对latex编写的数学文本的基本理解，并学习“通过类推”和“使用对角化”等高级概念在不同上下文中的确切语义。这也与重新表述问题并将其映射到一个设置(对于当前的atp，最好是纯方程式)的能力有关，在这个设置中定理的证明变得更容易。另一个需要做的相关工作是用一种可理解的数学表示“解释回来”长长的ATP证明。

“学习”这个词本身很多。最近SAT解决方案（命题ATP）的突破称为“冲突驱动的条款学习”（CDCL），但它只是一个正确的（分辨率）引起了由公理暗示的新引理。“学习”的泛化方面非常有限。我真的不知道ATP在二十年内有多好，改善可能来自各方，而不仅仅是通过使用“学习”。主要的ATP Calculi是如此简单和强烈的力量，即某人也会提出一种全新的方法，这将大大提高ATP系统的强度。金宝博官方例如，基于实例化的ATPiProver依靠CDCL扩展的SAT溶剂在近年来已经提高了很多。

另一个趋势，我期望的是更多种类的目标决策程序（处理数字，列表，BitVectors等），特别是当软件和硬件验证有用时，以及与ATP Calculi的集成。我也希望我们将开始能够从ATP完成的成功推理模式自动检测此类有针对性算法。在某种意义上，我们需要更好的自动编制“搜索”进入“计算”（我们可以称之为“学习决策程序”）。这两者之间没有刚性区别：在ATP启发的编程语言如Prolog，两件事在很大程度上是重合的。我们知道如何在某些（例如数数）问题类中指导证明搜索越好，证明搜索越多，有效计算。

最后，我可以大胆地对大理论ATP在20年后的强度做出一个具体的、可反驳的预测:以Flyspeck为例。开阳图书馆，学习辅助的大理论ATP今天可以证明47%的重复。40%的最高级的lemmas.．20年，使用相同的硬件和资源（即，不依赖Moore Law），我们将能够自动证明80％（在图书馆的同一版本上测量）。

卢克：谢谢，Josef！