科学家和软件开发人员使用自动推理来证明两件事。首先，他们证明系统设计或实现遵从其规范。其次，他们证明系统按预期的方式运作。

自动推理通过以数学定理或已知真理支持的形式逻辑产生证据来给出此证明。自动推理使用基于数学、逻辑的算法验证方法为所有可能的行为提供安全性或正确性证据。

自动推理还可证明用于配置网络、允许网络访问或授予权限或保持数据私密性和安全性的系统按预期运作。

使用自动推理时，您首先向系统提出问题陈述。然后，自动推理系统使用问题陈述计算和验证假设。该软件会持续执行此操作，直到用尽所有选项为止。

自动推理的示例问题

为了更全面地理解自动推理，可以考虑问题陈述 猫生活在陆地上吗？ 以及以下断言：

猫是哺乳动物

哺乳动物生活在陆地上

自动推理系统评估问题陈述是否正确。  具体而言，该系统使用逻辑推演。在此案例中，猫是哺乳动物，哺乳动物生活在陆地上。因此，系统将证实猫生活在陆地上。

自动推理的局限性

自动推理不进行预测或概括。例如，我们可以使用自动推理来提出类似于如下的论点：

Fluffy 是一只猫

因此，Fluffy 有毛发

我们不能使用自动推理来提出类似于如下的论点：

猫是哺乳动物

猫生活在陆地上

因此，所有哺乳动物都生活在陆地上

这样的应用在定理证明器中很常见，其中在执行推演性推理任务时需要人工指导。

以下是自动推理的其他一些使用案例。

科学家、工程师和数学家通过在科学应用场景中应用代数公式来解决问题并验证数学证据。在此类实践中，他们使用依赖多个变量来推断出问题可能解决方案的数学模型。

自动推理可帮助硬件工程师构建可靠的产品。借助自动推理，工程师能够发现传统测试方法所忽视的潜在缺陷。

例如，电子设计工程师使用严格的数学自动推理分析来获得确凿的证据，证明特定硬件设计符合其规范，例如系统行为或执行。

验证表明，系统的所有可能行为都满足构成规范的暂存属性。此验证还可以表明系统实现的每种可能行为都与其高级规范的某些行为一致。

软件开发人员使用自动推理来帮助确保应用程序能够抵御意外的安全问题，并确保软件按预期或设计运作。与硬件验证一样，自动推理可让开发人员根据各种策略验证软件安全措施。

例如，Amazon Web Services（AWS）的工程师通过自动推理证明每种启动配置的启动代码都是安全的。另一个示例是，这些工程师可证明在 Amazon Simple Storage Service（Amazon S3）上存储和处理的数据受到保护。在此示例中，他们依靠自动推理来执行复制、一致性、自动扩展、负载均衡和其他协调任务。

人类推理建模

计算机科学家使用自动推理技术来配置访问权限。为此，他们编写描述何时允许和拒绝用户访问资源的请求的策略。此策略可验证只有目标用户才能访问资源，这对于资源的安全性和隐私性非常重要。

例如，计算机科学家使用可满足性模块理论（SMT）公式和 SMT 求解器来证明安全特性。

接下来，我们分享几种使计算系统能够进行人工推演的自动推演方法。

经典逻辑是一种数学哲学，为自动逻辑推理程序提供基本的推理模型。这种逻辑基于如下原则：每个命题都有真或假的真值，但不能同时为两者。

它主要侧重于一阶逻辑，即允许数学家在语句中使用类似于 存在 的量词来表示像 x 这样的未知变量。例如，科学家在逻辑编程中应用经典逻辑在此语句中找到 x ： 存在 x，使得 x 生活在陆地上，并且 x 是哺乳动物 。

命题逻辑是一种逻辑系统，其中存在可能对或错的命题以及它们之间关系的构造，这种构造称为 论点 。

命题逻辑中论点的经典语句是 如果 P，则 Q 。例如，如果是星期六，则是周末。

自动推理使用一种称为 SAT 求解 的技术。该技术使用名为 SAT 求解器 的工具来搜索命题逻辑中令人满意的论点分配。这意味着使论点为真的变量。

自动推理是人工智能（AI）的一门特定学科，它将逻辑推理应用于计算机系统。

人工智能科学教导计算机在解决问题时像人类一样思考。人工智能的最新发展推动了各个子学科的发展，包括深度学习、数据分析和机器学习。

自动推理不同于其他人工智能技术，例如自然语言处理（NLP），后者侧重于训练计算机理解书面或口头演讲。相反，自动推理使用逻辑模型和证据来推理系统或程序的可能行为，包括它可以或永远不会达到的状态。

自动推理和机器学习并非等同。简而言之，机器学习可以做出预测和推理。自动推理则提供证据。

机器学习是人工智能的一个子集，它训练计算机使用大型数据样本做出决策。例如，数据科学家使用机器学习训练银行软件来识别欺诈活动。他们使用大量的财务数据样本，确保软件根据先前学习的结果轻松识别异常模式。

自动推理可让模型根据数学真相和证据推断出结果，而不是用数据训练模型。

Amazon CodeGuru Reviewer 使用自动推理和机器学习来帮助开发人员识别软件漏洞。

Amazon Inspector Classic 具有网络可访问性 功能 ，可自动分析 EC2 实例是否存在潜在的安全漏洞和配置错误。

AWS Identity and Access Management（IAM）Access Analyzer 应用自动推理来管理账户权限。

Amazon Virtual Private Cloud (Amazon VPC) Reachability Analyzer 应用自动推理来帮助您了解和可视化 AWS 网络。

有关各种 AWS 服务自动推理的更多信息，请访问 可证明的安全性 。我们使用数学推理为安全工作负载提供强大的安全保障。

立即 创建账户 ，开始在 AWS 上使用安全性。

AWS 对 Internet Explorer 的支持将于 07/31/2022 结束。受支持的浏览器包括 Chrome、Firefox、Edge 和 Safari。 了解详情 »