本周，亚马逊科学公司在其研究领域列表中增加了自动推理。我们之所以做出这样的改变，是因为自动化推理在亚马逊的影响力。例如，Amazon Web Services的客户现在可以直接访问基于自动推理的功能，如IAM access Analyzer、S3 Block Public access或VPC可达性分析器。我们还看到亚马逊开发团队将自动推理工具集成到他们的开发过程中，提高了我们产品的安全性、耐用性、可用性和质量。
本文的目的是为对该领域一无所知但又好奇了解更多的行业专业人士提供一个关于自动推理的温和介绍。理解本文所需要的只是能够阅读一些小的C和Python代码片段。在此过程中，我将提及一些专业概念，但目的只是以非正式的方式介绍它们。最后，我提供了一些我们最喜欢的公开工具、视频、书籍和文章的链接，供那些希望深入了解的人使用。
花点时间回答“f是否会返回false？”这不是一个骗人的问题：我特意用一个简单的例子来说明问题。
为了通过穷举测试来检查答案，我们可以尝试执行以下双嵌套测试循环，该循环对unsigned int类型的所有可能的值对调用f：
#包括<；斯特迪奥。h>；
不幸的是，即使在现代硬件上，这种双重嵌套循环也会运行很长时间。我编译了它，并在2.6GHz的英特尔处理器上运行了48个多小时才放弃。
为什么测试需要这么长时间？因为UntIX MAX通常为4294967295，所以要考虑的是1844 6740401196196025单独的F调用。在我的2.6GHz机器上，编译的测试循环每秒调用f大约4.3亿次。但要在这种情况下测试所有18个五分之一的病例，我们需要1360多年的时间。
当我们向行业专业人士展示上述代码时，他们几乎立即得出f可以'；只要底层编译器/解释器和硬件正确，就不能返回false。他们是怎么做到的？他们对此进行了推理。他们从上学时就记得x+y可以改写为y+x，并得出f总是返回真的结论。
自动推理工具为我们做这项工作：它试图通过使用已知的数学技术来回答有关程序（或逻辑公式）的问题。在这种情况下，该工具将使用代数来推断x+y==y+x可以替换为简单的表达式true。
即使域是无限的（例如，无界的数学整数而不是有限的整数），自动推理工具也可以非常快。不幸的是，在某些情况下，这些工具可能会回答“不知道”。我们'；我将在下面看到一个著名的例子。
自动推理的科学本质上专注于尽可能降低这些“不知道”答案的频率：工具报告的频率越低"；唐'；我不知道"；（或尝试时暂停），它们就越有用。
今天的工具能够为昨天的工具无法回答的程序和查询提供答案。明天的工具将更加强大。我们看到了这个领域的快速发展，这就是为什么在亚马逊，我们从中获得了越来越多的价值。事实上，我们看到自动推理形成了亚马逊式的良性循环，在这种循环中，更多的工具输入问题推动了工具的改进，从而鼓励更多地使用工具。
一个稍微复杂一点的例子。现在我们已经大致了解了什么是自动推理，接下来的一个小例子让我们更真实地感受到了这些工具为我们管理的那种复杂性。
空g（整数x，整数y）{
def g（x，y）：
试着回答这个问题：“g是否总是最终将控制权返回给它的调用者？”
当我们向行业专业人士展示这个程序时，他们通常会很快找到正确的答案。一些人，尤其是那些了解理论计算机科学成果的人，有时会错误地认为我们可以'；我不能回答这个问题，理由是“这是一个停顿问题的例子，已经被证明是无法解决的”。事实上，我们可以对特定程序的停止行为进行推理，包括这一个。稍后我们将进一步讨论这个问题。
以下是大多数行业专业人士在研究这个问题时使用的推理：
在y不是正的情况下，执行跳到函数g的末尾。这是一个简单的情况。
如果在循环的每次迭代中，变量x的值减小，那么最终，循环条件x>；y将失败，g的末端将到达。
只有当y始终为正时，x的值才会减小，因为只有这样，对x的更新（即x=x-y）才会减小x。但是y的正性是由条件表达式确定的，因此x始终减小。
有经验的程序员通常会担心C程序的x=x-y命令中的下溢，但随后会注意到x>；在更新到x之前为y，因此不能下溢。
如果你执行了以上三个步骤，你现在可以非常直观地看到自动推理工具在对计算机程序进行推理时代表我们执行的思维类型。这些工具必须面对许多细节（例如，堆、堆栈、字符串、指针算法、递归、并发、回调等），但也有几十年的研究论文涉及处理这些和其他主题的技术，以及各种实用工具，将这些想法付诸实施。
主要的收获是，自动推理工具通常代表我们完成上述三个步骤：第1项是关于程序控制结构的推理。第2项是关于程序中最终正确的内容的推理。第3项是关于程序中什么总是正确的推理。
请注意，AWS资源策略、VPC网络描述甚至makefiles等配置工件都可以被视为代码。这种观点允许我们使用我们用来推理C或Python代码的相同技术来回答有关配置解释的问题。正是这种见解为我们提供了IAM访问分析器或VPC可达性分析器等工具。
正如我们在上面研究f和g时所看到的，自动推理可以比穷举测试快得多。有了今天可用的工具，我们可以以毫秒为单位显示f或g的属性，而不是通过穷举测试来等待生命周期。
我们现在能抛弃我们的测试工具，转向自动推理吗？不完全是。是的，我们可以大大减少对测试的依赖，但我们不会很快完全消除它，如果有的话。考虑我们的第一个例子：
bool f（无符号整数x，无符号整数y）{
回想一下，一个有缺陷的编译器或微处理器实际上可能会导致由该源代码构造的可执行程序返回false。我们可能还需要担心语言运行时。例如，C数学库或Python垃圾收集器可能存在导致程序行为异常的错误。
关于测试，我们经常忘记的一点是，它所做的远不止是告诉我们C或Python源代码。它还测试编译器、运行时、解释器、微处理器等。测试失败可能源于堆栈中的任何工具。
相比之下，自动推理通常只适用于堆栈的一层——源代码本身，有时也适用于编译器或微处理器。我们发现，推理的价值在于，它可以让我们清楚地定义我们知道的和不知道的关于被检查层的信息。
此外，自动推理工具使用的周围环境模型（例如，编译器或调用我们的过程的过程）使我们的假设非常精确。分离计算堆栈的各个层有助于更好地利用我们的时间、精力、金钱以及今天和明天工具的功能。
不幸的是，在使用自动推理时，我们几乎总是需要对某些事情做出假设——例如，控制我们的硅芯片的物理原理。因此，测试永远不会被完全取代。我们希望进行端到端测试，尽可能地验证我们的假设。
我之前提到过，自动推理工具有时会返回“不知道”，而不是“是”或“否”。它们有时也会永远运行（或超时），因此永远不会返回答案。让我们看看著名的"；停顿问题"；程序中，我们知道工具不能返回“是”或“否”。
假设我们有一个名为terminates的自动推理API，如果一个C函数总是终止，它会返回“是”，如果该函数可以永远执行，它会返回“否”。例如，我们可以使用这里描述的工具（作者之前工作的无耻自我推广）构建这样一个API。为了了解终止工具能为我们做什么，考虑两个基本的C函数，g（来自上面），
空g（整数x，整数y）{
空g2（整数x，整数y）{
由于我们已经讨论过的原因，函数g总是将控制返回给它的调用者，因此终止（g）应该返回true。同时，terminates（g2）应该返回false，因为例如，g2（5，0）永远不会终止。
注意它'；这是递归的。什么是终止（h）的正确答案？答案不可能是"；是的；。它也不能是"；没有；。为什么？
想象一下（h）将返回"；是的；。如果你读h的代码，你会发现在这种情况下，函数不会因为h代码中的条件语句而终止，它将在（1）{}时执行无限循环。因此，在这种情况下，terminates（h）答案是错误的，因为h是递归定义的，调用terminates本身。
同样，如果终止（h）返回"；没有"；，然后h实际上会终止并将控制权返回给它的调用者，因为条件语句的if情况不满足，并且没有else分支。同样，答案是错误的。这就是为什么在这种情况下，“不知道”的答案实际上是不可避免的。
程序h是图灵1936年关于可判定性和1931年哥德尔不完全性定理的著名论文中给出的例子的变体。这些论文告诉我们，像停顿问题这样的问题是无法“解决”的，如果“解决”是指解决过程本身总是终止，回答“是”或“否”，但永远不回答“不知道”。但这并不是我们许多人心目中“已解决”的定义。对于我们中的许多人来说，一个工具有时会超时或偶尔返回“不知道”，但当它给出答案时，总是给出正确的答案就足够了。
这个问题类似于航空旅行：我们知道它不是100%安全的，因为坠机事故在过去发生过，我们确信它们在未来也会发生。但当你安全着陆时，你知道那次它起了作用。航空业的目标是尽可能减少失败，尽管原则上这是不可避免的。
把它放在自动推理的背景下：对于一些程序，比如h，我们永远无法对工具进行足够的改进，以取代"；唐'；我不知道"；答复但今天还有许多其他情况'；s工具回答"；唐'；我不知道"；，但未来的工具可能能够回答#34；是的"；或"；没有；。自动推理主题专家面临的现代科学挑战是让实用工具尽可能多地返回“是”或“否”。作为当前工作的一个例子，请查看CMU教授和亚马逊学者Marijn Heule，以及他对解决Collatz终止问题的探索。
另一件需要记住的事情是，自动推理工具经常试图解决“棘手”的问题，例如NP复杂性类中的问题。在这里，与我们在暂停问题中看到的想法相同：自动推理工具具有强大的启发式算法，通常可以解决特定情况下的棘手问题，但这些启发式算法可能（有时确实）失败，导致“不知道”答案或执行时间过长。科学的目标是改进启发式算法，以最小化这个问题。
科学文献中使用了大量名称来描述相关主题，而自动推理只是其中之一。下面是一个快速词汇表：
逻辑是一个正式的、机械的系统，用来定义什么是真的，什么是假的。例子：命题逻辑或一阶逻辑。
证明是定理逻辑中的有效论点。例如：Gonthier和#39；这是四色定理的证明。
机械定理证明器是一种半自动推理工具，用于检查通常由人写下的证明的机器可读表达式。这些工具通常需要人工指导。例子：来自亚马逊研究员约翰·哈里森的霍尔·莱特。
形式验证是将定理证明应用于计算机系统模型，以证明系统的期望属性。示例：CompCert验证了C编译器。
形式化方法是最广泛的术语，简单地说就是使用逻辑对系统模型进行形式化推理。
半自动推理工具需要用户提供提示，但仍能在逻辑上找到有效的证据。
正如你所见，在这个空间工作时，我们可以选择名字。在亚马逊，我们选择使用自动推理，因为我们认为它最能体现我们对自动化和规模的雄心。在实践中，我们的一些内部团队同时使用自动和半自动推理工具，因为我们的科学家'；在全自动推理中的启发式可能失败的情况下，我们通常可以获得半自动推理工具。对于我们面向外部的客户功能，我们目前只使用完全自动化的方法。
在这篇文章中，我介绍了自动推理的概念，使用最小的玩具程序。我还没有描述如何处理具有堆或并发性的实际程序。事实上，有各种各样的自动推理工具和技术，用于解决各种不同领域的问题，其中一些领域相当狭窄。要描述它们以及该领域的许多分支和子学科（如“SMT求解”、“高阶逻辑定理证明”、“分离逻辑”），需要数千篇博客文章和书籍。
自动推理可以追溯到计算机的早期发明者。逻辑本身（自动推理试图解决的问题）已有数千年的历史。为了使这篇文章简短，我将在这里停下来，并建议进一步阅读。请注意，首先进入这个区域很容易迷失在杂草阅读深度中，你可能会比开始时更加困惑。我鼓励你使用有限的深度优先搜索方法，只在一些细节中顺序查看各种工具和技术，然后继续，而不是只深入学习一个方面。
使用可证明安全性自动化AWS合规性验证，与AWS合规副总裁查德·伍尔夫和合规审计员Coalfire#39进行讲座；公司首席执行官汤姆·麦坎德罗
AWS自动推理技术的发展，与AWS安全副总裁埃里克·布兰德温（Eric Brandwine）一起演讲
AWS CISO和安全副总裁Steve Schmidt关于AWS中基于形式/约束的工具的开发和使用的讲座
我们今天使用的自动定理证明器中发现的一些算法可以追溯到1959年，当时王浩使用自动推理来证明《数学原理》中的定理。