共计 971 个字符，预计需要花费 3 分钟才能阅读完成。
Amazon AWS 的杰出科学家 Byron Cook 最近为“自动化推理”这一概念进行了辩护。自动化推理，也被称为“符号 AI”或“形式验证”，是人工智能领域中的一个古老研究方向。Cook 指出，这一领域正在迅速与生成式 AI 融合，形成一种被称为“神经符号 AI”的新混合体，结合了自动化推理和大型语言模型的优势。
在今年 5 月的纽约 AWS 金融服务研讨会上，Cook 发表了关于自动化推理的演讲。他解释说，自动化推理指的是通过逻辑验证为真的关于世界的陈述或断言的算法。其核心理念是所有知识都严格地由逻辑上能够断言的内容支持。Cook 强调，“推理采用一个模型，并让我们准确地谈论它可以生成的所有可能数据。”
- 
Cook 通过一个简单的代码循环示例展示了自动化推理的工作原理。他解释说，通过逻辑分析，可以回答“这个循环可以永远运行吗？”的问题，而无需实际运行代码。这种通过逻辑而非试错来回答基本问题的能力，正是自动化推理的核心价值。
Cook 表示，自动化推理的历史可以追溯到 20 世纪 50 年代末，当时 IBM 704 机器曾使用自动化推理证明了 Whitehead 和 Russell 的《数学原理》中的所有定理。如今，自动化推理在 AWS 中已有十年的应用历史，用于确保服务交付和验证网络安全。
Cook 指出，自动化推理在网络安全中的应用尤为关键。例如，AWS 的身份和访问管理工具 IAM Analyzer 可以在几秒钟内解决客户提出的复杂问题，而无需进行耗时的详尽测试。
Cook 认为，自动化推理的力量将使其成为“一种人工超级智能的形式”。它已被用于解决开放的数学猜想，并在 AWS 的代码证明和访问授权等任务中发挥了重要作用。所有这些应用都依赖于 AWS 内部的自动化推理基础设施 Zelkova。
Cook 还提到，自动化推理与生成式 AI 的融合将为非技术人员提供强大的工具。通过将自然语言转化为形式逻辑，生成式 AI 可以帮助用户表达目标，而自动化推理则负责严格实施这些目标。
在代理 AI 时代，自动化推理将变得更加重要。Cook 解释说，代理 AI 由多个并行运行的 AI 系统组成，其正确性可以通过自动化推理进行验证。例如，AWS 的 S3 存储系统通过自动化推理证明了其分布式系统设计的正确性。
Cook 对自动化推理和生成式 AI 的未来充满信心。他表示，这两个领域的结合将为人工智能带来新的突破，并为用户提供更强大的工具和解决方案。
