自动推理（九）

不同的证明助手提供不同的功能，通过自动推理任务、支持的逻辑、对象类型、数学库的大小以及输入和输出的可读性的能力来衡量。一个不太琐碎但也不太复杂的“规范”证明可以用作系统比较的基线，如 (Wiedijk 2006) 中所做的那样，其中十七个推理系统的作者的任务是建立 \sqrt{} 的非理性。 2. 所讨论的系统肯定比这更强大，其中一些已被用来协助更高级的证明的形式化，例如 Erdös-Selberg 的素数证明定理（Isabelle 中约 30,000 行）、四色定理的形式化（Coq 中 60,000 行）和 Jordan 曲线定理（HOL Light 中 75,000 行）。交互式定理证明的一个里程碑是在 2012 年，经过六年的努力并使用 Coq 证明助手，George Gonthier 和他的团队完成了 Feit-Thompson 定理（也称为奇阶定理，有限单群分类的一个重要步骤。其他最近的成功包括凯勒猜想的解决（Brakensiek et al. 2022）、度量空间的形式化（Maggesi 2018）以及有限域的形式化和分类（Chan 和 Norrish 2019）。

尽管如此，自动推理对数学实践的影响很小，对此有很多原因。原因之一是自动定理证明器的功能不足以解决数学家通常处理的问题；他们目前的能力充其量只是本科一年级数学的水平，距离前沿的数学研究还很远。虽然当前的系统确实无法在这个难度级别上完全证明自己的问题，但我们应该记住，我们的目标是构建推理系统，以便“最终机器将成为数学研究的辅助工具，而不是替代品” （王1960）。考虑到这一点，虽然自动推理社区继续努力应对构建日益强大的定理证明器的巨大挑战，但数学家现在可以利用当前系统提供的一些好处，包括帮助完成证明差距或形式化和检查所提出的证明的正确性。事实上，后者可能是一个可以帮助解决数学界当前面临的一些实际问题的应用程序。想想 Daniel Goldston 和 Cem Yildrim 宣布的孪生素数猜想的证明，尽管专家们最初同意该证明是正确的，但不久之后就发现了一个无法克服的错误。或者，考虑一下黑尔斯对开普勒猜想的证明，该猜想断言欧几里得 3 空间中的全等球堆积的密度不大于面心立方堆积的密度。黑尔斯的证明由大约 300 页的文本和大量的计算机计算组成。经过四年的努力，《数学年鉴》指派的负责验证该证明的 12 人小组仍然对其正确性抱有真正的怀疑。托马斯·黑尔斯（Thomas Hales）就是其中之一，他亲自将他的证明形式化，并由自动证明助理对其进行检查，目的是让其他人相信其正确性（Hales 2005b，在其他互联网资源中）。诚然，他的任务很繁重，但结果对于数学和自动推理社区来说可能非常重要。当 Hales 宣布完成 Flyspeck 项目（Hales 2014，其他互联网资源；Hales 2015）时，所有的目光都集中在 Hales 和他的正式证明上，他使用 Isabelle 和 HOL Light 自动证明助手构建了该猜想的正式证明：“在事实上，我做这个项目的动机远比简单地希望消除少数裁判心中残留的疑虑要复杂得多。事实上，我认为形式方法是数学长期发展的基础。” （黑尔斯，2006）。

Church 1936a、1936b 和 Turing 1936 暗示存在最短证明非常大的定理，以及 (Appel & Haken 1977) 中的四色定理的证明、(Gorenstein 1982) 中的简单群分类以及 (Gorenstein 1982) 中的简单群分类的证明（Hales 2005a）中的开普勒猜想很可能只是未来的样本。正如（Bundy 2011）所说：“随着需要越来越多证明的重要定理的出现，数学面临着两难境地：要么必须忽略这些定理，要么必须使用计算机来协助证明。”

上述言论还反驳了不使用自动定理证明器的另一个论点：数学家喜欢证明定理，那么为什么要让机器夺走乐趣呢？当然，答案是，数学家可以通过让机器完成更乏味和卑微的任务来获得更多乐趣：“对于优秀的人来说，像奴隶一样在计算劳动中浪费时间是不值得的，因为计算劳动可以安全地被降级。”如果使用机器，对其他人来说”（G. W. Leibniz，《关于人类理解的新论文》）。如果仍然不相信，请考虑一下必须手动检查黑尔斯证明中使用的 23,000 个不等式的令人清醒的前景！

数学界对自动推理接受度不高的另一个原因是，这些程序不可信，因为它们可能包含错误（软件缺陷），因此可能会产生错误的结果。正式验证自动推理程序将有助于改善这一问题，特别是在证明检查器的情况下。证明程序正确并不是一件容易的事，但是在高级数学中证明定理是正确的：Gonthier证明了正确的四种颜色定理证明的程序中使用的程序是正确的，但是他花了更大的努力来形式化所有图形论，这是证明的一部分。具有讽刺意味的是，事实证明，至少在这种情况下，当然还有其他人，“实际上，验证程序的正确性比验证笔和纸数学的正确性更容易”（Wiedijk 2006）（Wiedijk 2006） 。对于定理抛弃和模型发现者，一种补充策略是验证程序的结果，而不是程序本身。释义（Slaney 1994）：对于数学家来说，只要它输出的证明（或模型）是正确的。因此，无论是由机器还是人类产生的结果，责任是在验证结果中，并由独立各方检查（当然可以很好地使用自动检查器）应提高对证明有效性的信心。

经常认为自动证明太长且详细。可以在更基本的步骤中表达的证明原则上非常有益，因为这允许数学家请求证明助手以更简单的步骤来证明其步骤是合理的。但是，证明助手也应允许相反的情况，即使用高级概念，语言和符号数学家习惯于抽象的细节和目前的结果及其理由。在（Denney 2006）中利用证明的层次结构是朝这个方向迈出的一步，但需要更多的工作。在预期的粒度水平上，在证明过程中，将证明助理工作提供了更多的见解机会。这是一个重要的考虑因素，因为数学家同样有兴趣从证据中获得理解，就像建立事实一样，对此进行了更大的兴趣。

（Bundy 2011）暗示了一个僵局，该僵局阻止了数学社区对定理掠夺的广泛采用：一方面，数学家需要使用证明助手来建立一个大型的数学成果库。但是，另一方面，他们不想使用掠夺者，因为没有这样的先前证明的库可以建立的结果。为了打破僵局，提出了许多应用程序，以帮助数学家搜索先前证明的定理是特别有望的。实际上，在证明一些线性代数的某些基本定理（Aransay andDivansón2017）和概率理论（Avigad，Hölzl和Serafin和Serafin 2017）的证明中，深思熟虑的库结果可以导致简明的非平凡数学问题证明。在其历史上，数学积累了大量定理，数学结果的数量继续显着增长。 2010年，Zentralblatt Math涵盖了约120,000个新出版物（Wegner 2011）。显然，除非可以协助使用可以以智能的方式搜索以前证明的感兴趣的结果，否则任何人都无法熟悉所有这些数学知识，除非能够协助使用自动化的定理工具，否则要应对自己不断增长的专业领域将变得越来越困难。解决这个问题的另一种方法是，数学家可以在Polymath和Mathoverflow等计算社会系统中启用彼此的知识。将自动推理工具集成到这样的社会系统中，将通过支持“精确正式扣除和数学实践中更非正式的松散互动的结合”（Martin＆Pease 2013，在其他互联网资源中）来提高其集体智能的有效性。

由于行业的真正紧迫需求，在纯数学和应用数学中自动推理的某些应用更需要选择。在进行了一些基本真实分析的形式化以验证基于硬件的浮点三角函数之后，（Harrison 2006，Harrison 2000）提到了进一步的需要形式化更多纯粹的数学数学的需求，即他的功率 - 使他的正式化扩展到Power to for Power to for Power Series系列三角函数和基本定理关于二芬太汀的近似。哈里森（Harrison）感到惊讶的是，“如此广泛的数学发展仅用于验证浮点切线功能是否满足某些错误的限制”，并且从这一说法中，人们希望还有其他工业应用需要更广泛的形式化。

尽管不是最初预期的速度，但自动推理是在数学中找到应用程序。其中，对证明的正式验证具有特殊意义，因为它不仅提供了一种可行的机制来检查人类独自一人的证据，而且还具有重新定义证明所需的东西的潜力这样接受。随着自动推理助手的使用变得更加普遍，人们可以按照一定的有条理的顺序设想他们的使用：首先，自动推理工具用于理论探索和发现。然后，在确定了一些目标问题之后，从业人员与自动助手互动地工作以找到证据并确定事实。最后，在提交出版之前，使用自动证明检查器来检查所有最终证明的正确性，并通过在正式数学的存储库中创建新条目，并将其提供给其余数学社区。在使用自动证明助手成为数学家生活中的日常事务确实是时间问题。自动推理社区的巨大挑战是要早日实现。

除了正式验证或认证外，证明的另一个重要方面是其提供的解释；也就是说，它给出的原因是为什么给定的语句实际上是正确的。不用说，这是洞察力的重要来源，对于许多数学家而言，它可能是证明最有价值的方面涉及的对象；此外，证明中使用的方法具有适用于证明其他数学结果的潜力。因此，当涉及到数学界使用的定理掠夺者时，也许应该较少强调掠夺者作为认证者，即作为证明检查员，并更加重视作为证明求解者，即作为助理帮助助手数学家完成证明并解释这样做的步骤。假设供奉献者足够强大，可以在数学家的研究领域成功攻击证据，那么如果供者也使用相同的符号，方法和方法，则非常理想，但公认的挑战是极具挑战性的数学家本人。可以肯定地敢打赌，数学家会更容易接受这种面向人类的定理称者，因为供者会以数学家的方式工作。最初，越来越多的数学家可能只是出于好奇心而探讨这样的谚语。也就是说，只是要看看供者将如何证明先前确定的结果。这对于数学学生来说肯定会引起人们的兴趣，因为他们可能需要查看给定的问题（例如，他们的教科书）是如何解决的，并且通过检查证据，想学习如何自己做。

如今，几乎所有自动化定理掠夺者都将以类似于机器而不是人类（例如解决方案驱动的连接方法）的方式来构建其证据。在建立事实后，有些系统可以以更适合人类的形式显示更高级别的步骤，并通过将面向机器的步骤转换为人类可读格式来做到这一点。该方法具有优点，但有一个重要的限制：在翻译分解之前，可以继续要求解释有多深？另一种方法可以试图解决情况的方向：为什么不构建直接证明定理数学家实际做到的系统呢？这确实是一个非常艰巨的任务，但问题并不是什么新鲜事物，并且已经由少数研究人员以各种形式采用，可以追溯到自动定理的早期证明，包括Bledsoe 1977（调查非分辨率方法） ，Boyer and Moore 1979（递归术语重写的归纳），Bundy等。 1991年（自动归纳定理证明），Clarke和Zhao 1994（定理掠夺与符号代数系统的整合），Portoraro，1994年（对建立符号逻辑证明的学生的自动建议），Portoraro 1998（战略证明象征性逻辑的教师DO和象征性逻辑的方式）教会它），佩莱蒂尔（Pelletier）1998（谓词微积分中的建筑证明IT），Beeson 2001（使用数学方法进行证明生成），Buchberger等。 2016年（计算机辅助的天然数学）等。最近，Ganesalingam and Gowers 2017描述了一个定理供奉献者，该定理宣传者解决并介绍了公制空间理论中基本问题的证据，在该理论中，该程序的方法很难与数学家可能证明和写作。为了说明，下面是该计划的证明，即公制空间的两个开放子集的交集本身是开放的，并且它是由该程序解决和编写的，因此给出了：

证明。让x为a \ cap B的元素。然后在A中的x \中x \。因此，由于a是打开的，因此存在\ eta> 0，以便每当d（x，u）中的u \ \ lt \ eta和B开放，因此存在\ theta> 0，因此每当d（x，v）\ lt \ theta时，v \ in b中的v \。我们想找到\ delta> 0 S.T.每当D（x，y）\ lt \ delta时，y \在a \ cap b中。但是，只有y \ y \ y \ in A和y \在B中的y \中，y）\ lt \ theta。现在假设d（x，y）\ lt \ delta。然后d（x，y）\ lt \ eta如果\ delta \ le \ eta和d（x，y）\ lt \ theta如果\ delta \ le \ theta。因此，我们可以采用\ delta = \ text {min} \ {\ eta，\ theta \}，我们完成了。

令人印象深刻的是，作者承认，即使是数学中的基本问题，在建立和呈现此类证明方面的许多缺点和许多出色的挑战，并将读者转介给他们的文章以获取详细信息。正如我们已经提到的那样，建立越来越强大的掠夺者可以在数学研究的高级领域攻击问题并以人为导向的方式进行问题，这是极具挑战性的，但我们还需要补充一点，这是一个非常有价值的，有前途和有益的线条研究。数学家拥抱这种掠夺者将在研究和教育中都有明确的实际应用。也将有哲学的含义，尤其是掠夺者在陷入证明时赋予寻求帮助的额外能力的那一刻机器，反之亦然？与定理供体互动的经验将被扩展到一个新领域，成为真正的双方，更亲密和更丰富的领域，更多的是协作而不是互动：协作定理的曙光证明。

4.8人工智能

自成立以来，自动定理的领域证明在更大的人工智能领域（AI）具有重要的应用。自动扣除是AI应用程序的核心，例如逻辑编程（请参阅第4.1节逻辑编程），其中计算等同于扣除；机器人技术和解决问题（Green 1969），实现目标的步骤是从证据中提取的步骤；演绎数据库（Minker等人，2014年），其中事实知识表示为原子从句和推理规则，并且通过演绎来推断新事实；专家系统（Giarratano＆Riley 2004），其中人类在给定领域中的专业知识（例如血液感染）被捕获为IF-Then扣除规则的集合以及通过应用推论规则获得结论（例如诊断）的何处；还有许多其他人。在人工智学中，自动推理的应用必然会具有深厚的哲学含义智能代理和多机构系统（Meyer 2014），尤其是赋予未来智能系统，例如决策支持系统或机器人，具有法律和道德行为。可以为任务自动化义逻辑（Furbach等，2014），但是鉴于对义逻辑的通用系统没有达成共识，道德规范“代码设计师”需要一种方法来实验不同的道态系统（即启动）淘汰公理，并从中得出什么结论），以帮助他们确定手头特定应用程序所需的道德代码； （Benzmüller等人，2018年）讨论了一个环境。如果在这些实验中使用实际的物理机器人，则“拔出实验室”一词将是描述性的，尽管有些令人毛骨悚然。

限制证明搜索空间一直是实施自动扣除的关键考虑因素，而传统的AI搜索搜索一直是定理掠夺者不可或缺的一部分。主要思想是防止卖者追求纯正的推理道路。搜索的一个双重方面是尝试寻找先前证明的结果，该结果可能在完成当前证明中很有用。自动识别这些结果并非易事，并且随着问题域的大小以及已经建立的结果的数量增长而变得不那么容易。尤其是鉴于构建大量定理库的趋势，例如定理证明的Mizar问题（MPTP）（Urban等人，2010年，Bancerek＆Rudnicki 2003）或Isabelle/HOL Mathemathematical Mathagathematical Mathematical Library（Urban等人）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP）（MPTP（MPTP））（ Meng＆Paulson 2008），因此，为正式数学的大型图书馆中的发现，评估和选择的技术开发技术在（Kühlwein等人，2012年）中讨论的是一项重要的研究线。