作者：王聪彬

自动推理（Automated Reasoning）最早可追溯到“笛卡尔构想”，其中蕴含了机器自动证明定理的人类梦想；莱布尼茨的“通用符号演算”则为实现这一梦想设定了目标；希尔伯特的“形式主义与判定问题”将自动推理提升为一个严谨的数学问题，提供了理论上的完整解决框架。

数学问题所展现出的是精准性和严谨性，自动推理通过数学和逻辑的验证方法，实现了大规模系统在安全性、效率和稳定性上的显著提升。

“对于复杂系统，可能的输入非常多甚至无限。”亚马逊云科技首席信息安全官(CISO) Chris Betz说，“我们可以用更好的自动推理技术，在几秒钟内系统地、彻底地探索这个无限空间。”

自动推理在亚马逊云科技已经得到广泛应用，通过将系统逻辑转化为数学模型，亚马逊云科技在代码优化、部署安全性和错误修复等方面实现了更高效的管理。

这种基于数学的验证方法不仅使系统更易于维护，还为持续提升系统性能和安全性创造了良性循环。在亚马逊云科技，自动推理以及提供了严密的安全保障，让服务如同自然法则般可靠且可控，为客户带来前所未有的信任体验。

自动推理在云中崭露头角

自动推理是专注于使用计算机程序来模拟人类的推理过程，从而在给定的知识和规则的基础上推导出新的结论或证明某个命题的真实性。

Chris Betz曾在re:Inforce2024上表示，自动推理让我们能看到系统可能的行为，识别并修复不期望的行为。

早期自动推理主要用在机器定理证明，也就是寻找判定公式是否是有效的通用程序。

到了云计算时代，随着系统规模的不断扩展，复杂性也随之增加，数据安全和系统稳定性成为云服务的核心要求。自动推理通过系统性地发现并修复代码中的隐性错误，使企业在大规模分布式系统中实现更高的可维护性，并减少宕机时间。

自动推理同时是人工智能的重要起源，为人工智能提供了一种基本的思维和推理能力，使计算机能够在逻辑和知识表示的基础上进行推理和证明。

亚马逊云科技一直致力于为客户构建简单、易用的服务，但俗话说“台上一分钟，台下十年功”。表面上看到的简单，背后确支撑着庞大且复杂的分布式系统，实现每秒处理数十亿个请求的高效运作。

10多年前亚马逊云科技就已经开始应用自动推理。亚马逊云科技自动推理副总裁及杰出科学家Byron Cook谈到，亚马逊云科技的业务也在不断发展和迭代，很多变化本身就是非常复杂的，必须在不影响亚马逊云科技本身或客户的安全性和韧性的前提下进行。

所以在传统测试方法外，亚马逊云科技还引入了基于数学和逻辑的强大技术“自动推理”进行补充。自动推理可以帮助解答系统能做什么、将做什么以及永远不会做什么的问题，即使是最复杂、规模庞大或潜在无限的系统，自动推理也能提供深入验证，这是传统测试方法无法完全实现的。

事实证明经过验证的代码通常比它所替代的未经验证的代码性能更好。虽然自动推理无法实现完美的系统，但它增强了亚马逊云科技对系统正确性的信心。

成为解放技术研发生产力的秘密武器

现在自动推理技术已成为亚马逊云科技的“秘密武器”，开发、代码、代码部署都能看到它的身影，并且已经形成了一个良性的循环。

在开发层面，自动推理正帮助开发团队更高效地发现系统中的潜在Bug并快速修复。Amazon S3的背后是世界上最大、最复杂的分布式系统之一，它存储了400万亿个对象、EB级别的数据，通常需要每秒处理1.5亿个请求。

即使开发人员能够证明Bug的存在，并可能识别出引发Bug的根本原因，但他们不可能考虑到所有可能的异常情况，更不用说这些异常情况的各种组合。这种复杂性促使亚马逊云科技探索，如何利用自动推理来探索潜藏在不同状态下可能的状态和错误。通过构建系统的正式规范，能够发现Bug并确保未来不会再出现类似问题。

而且亚马逊云科技大约每个季度都会对Amazon S3进行新的改进，任何更改的前提都是在极其谨慎和大量测试下进行，使用自动推理使，亚马逊云科技有信心每隔一两个月发布一次更新和改进。

在代码层面，自动推理能够确保系统在几乎所有情况下遵守特定的安全属性。亚马逊云科技每秒会接收超过12亿次请求，每次API调用都会需经过Amazon IAM授权引擎处理，这一过程必须确保安全性。

亚马逊云科技在re:Invent2023推出了Cedar，是一个专为表达应用程序中细粒度权限而打造的开源授权策略和评估引擎。Cedar也是首个从零开始构建并使用自动推理进行正式验证的策略语言。不到一年的时间里，已有六家独立初创公司基于Cedar开发了付费功能。

亚马逊云科技还推出了用于验证网络访问控制列表（ACL）正确性的内部推理工具。工具针对指定必须允许或禁止的流量的不变量来验证给定的ACL，能够推理大约10的94次方个可能的IPv6组合，每天大约执行800万次评估，并且每次评估用时不到一秒。

在代码部署层面，自动推理让大多数在线交易都依赖加密保护。RSA加密算法通过生成一对密钥来加密和解密数据，确保数据传输和数字签名的安全。在加密场景中，一个小小的bug可能带来灾难性后果。

Amazon Graviton上，针对ARM指令集的加密优化也带来了显著性能提升。加密算法优化过程非常复杂，验证修改后的算法是否正常运行往往需要数月的审查才能确保其可靠性。自动推理不仅让RSA加密更高效，部署也变得更快。同样，将自动推理应用于椭圆曲线密码学时，也看到了类似的提升。

亚马逊云科技是唯一一家如此大规模使用自动推理的云提供商。随着越来越多的人使用自动推理工具，亚马逊云科技在提升自动推理工具的可用性和可扩展性上更容易进行大量的投入。亚马逊云科技正将自动推理应用于更多领域，其与众不同之处就在于，从基础就用可靠的数学推理并持续分析所构建的一切，防止从AI幻觉到分析虚拟机监控程序、密码学和分布式系统等潜在问题的发生。这种精准的可控推动了云计算向更加智能、安全和可持续的时代迈进。