什么是自动推理？
自动推理是计算机科学的一个领域，试图为系统或程序会做什么或永远不会做什么提供保证。这种保证基于数学证明。人们通过使用定理和推论等逻辑策略来解决数学、科学和计算中的许多逻辑问题。自动推理使用计算机来应对复杂的挑战，这些计算机使用相同的工具。自动推理工具尝试使用已知的数学技术来回答有关程序（或逻辑公式）的问题。这些工具可以帮助您检查语句或表达式是否为真。
自动推理可以解决哪些问题？
科学家和软件开发人员使用自动推理来证明两件事。首先，他们证明系统设计或实现遵从其规范。其次，他们证明系统按预期的方式运作。
自动推理通过以数学定理或已知真理支持的形式逻辑产生证据来给出此证明。自动推理使用基于数学、逻辑的算法验证方法为所有可能的行为提供安全性或正确性证据。
自动推理还可证明用于配置网络、允许网络访问或授予权限或保持数据私密性和安全性的系统按预期运作。
使用自动推理时，您首先向系统提出问题陈述。然后，自动推理系统使用问题陈述计算和验证假设。该软件会持续执行此操作，直到用尽所有选项为止。
自动推理的示例问题
为了更全面地理解自动推理，可以考虑问题陈述猫生活在陆地上吗？以及以下断言：
- 猫是哺乳动物
- 哺乳动物生活在陆地上
自动推理系统评估问题陈述是否正确。 具体而言，该系统使用逻辑推演。在此案例中，猫是哺乳动物，哺乳动物生活在陆地上。因此，系统将证实猫生活在陆地上。
自动推理的局限性
自动推理不进行预测或概括。例如，我们可以使用自动推理来提出类似于如下的论点：
- 猫有毛发
- 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），后者侧重于训练计算机理解书面或口头演讲。相反，自动推理使用逻辑模型和证据来推理系统或程序的可能行为，包括它可以或永远不会达到的状态。
自动推理和深度学习有什么区别？
自动推理证明程序或系统的属性。自动推理使用程序或系统本身，以及形式逻辑中系统的模型或规范。
深度学习在将统计模型应用于大型数据集的基础上进行预测。
深度学习是一种先进的机器学习技术，可以模拟人类大脑的运作方式。它使用不同的神经网络模型，这些模型由用于提取、比较和分析相关信息的多层神经元组成。数据科学家将深度学习用于复杂的应用，例如处理自动驾驶汽车中的摄像头和传感器数据。
自动推理是机器学习吗？
自动推理和机器学习并非等同。简而言之，机器学习可以做出预测和推理。自动推理则提供证据。
机器学习是人工智能的一个子集，它训练计算机使用大型数据样本做出决策。例如，数据科学家使用机器学习训练银行软件来识别欺诈活动。他们使用大量的财务数据样本，确保软件根据先前学习的结果轻松识别异常模式。
自动推理可让模型根据数学真相和证据推断出结果，而不是用数据训练模型。
AWS 如何使用自动推理来改进服务产品？
AWS 使用自动推理来改进多个服务产品。下面提供了一些示例：
- 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 上使用安全性。
