AWS真的能修复AI幻觉吗？

面试人工智能的一个显着缺陷是它习惯于“产生幻觉”，编造出没有现实数据基础的看似合理的答案。AWS 正在尝试通过引入 Amazon Bedrock 自动推理检查来解决这个问题。

Amazon Bedrock 是一项针对生成式 AI 应用程序的托管服务，根据 AWS 首席执行官马特·加曼 (Matt Garman) 的说法，他上个月在拉斯维加斯举行的 re:Invent 会议上发言，这些检查“可以防止由于模型幻觉而导致的事实错误......Bedrock 可以检查模型所做的事实陈述是准确的。”

他说，这一切都是基于“合理的数学验证”。

这些都是重大主张。他们的背后隐藏着什么？AWS 自动推理小组的负责人、伦敦大学学院计算机科学教授拜伦·库克 (Byron Cook) 表示登记册：

很多人不明白他们欺骗了程序员做内存安全的证明，而 Rust 中的借用检查器本质上是一个演绎定理证明器。它是一个推理引擎......

“我一直致力于形式推理和工具领域的工作。大约 10 年前，我将这种功能引入亚马逊，然后在人工智能中得到了一些应用。现在突然之间，我的领域变得非常模糊了。，突然间就不那么晦涩难懂了。”

如何减轻人工智能幻觉带来的风险，问题是否可以解决？

“从某种意义上说，幻觉是一件好事，因为它是创造力。但在语言模型生成过程中，其中一些结果将是不正确的，”他说。

“但是，谁的定义是错误的？事实证明，定义真理是什么是出奇的困难。即使在你认为每个人都应该同意的领域也是如此。

“我曾在航空航天、铁路交换、操作系统、硬件、生物学领域工作过，在所有这些领域中，我看到构建这些工具时花费的大部分时间都是与领域专家争论什么是正确的。答案应该是，由针对极端情况的具体例子驱动。”

库克补充道：“另一件事是，有些问题是无法判定的。例如，图灵就证明了这一点。没有任何程序可以在有限的时间内始终权威地以 100% 的准确率回答问题。

“如果你尝试将所有陈述的领域进行划分，就会发现有些是相对形式化的，而另一些则不是。什么是好的音乐将很难形式化，人们可能对此有一些理论，但是他们之间可能存在分歧，例如生物学，有生物系统如何工作的模型，但他们正在做的部分工作是采用这些模型，然后检查真实的系统，因此他们正在尝试改进模型。在这些警告下，该模型可能是错误的。你可以做很多事情。”

库克描述了自动推理工具，参考示例案例，例如根据个人的损益表确定正确的税码。 

但人类也会产生幻觉——作为一个社会，我们总是在削弱什么是真理，以及我们如何定义它以及谁决定它会成为什么。

他说，该工具“采用自然语言的陈述并将其翻译成逻辑，然后证明或反驳该领域下的有效性。这怎么会出错呢？从自然语言到逻辑的翻译有机会得到一点点然后人们决定什么是税法并将其形式化，因此仍然有可能得到错误的答案，但前提是我们的翻译是正确的，并且假设我们帮助了他们。客户正式定义【规则】，我们可以用数学逻辑建立一个被证明是正确的论证，他们得到的答案是正确的。”

库克说，幻觉“是我们必须长期面对的一个问题。但人类也会产生幻觉……作为一个社会，我们总是在削弱什么是真理，以及我们如何定义它以及谁来决定什么”事情就这样了。”

我们请库克评论一个著名的人工智能幻觉案例，一位律师引用 Open AI 的 Chat GPT 发明的案例库克表示，这并不是自动推理工具可以解决的那种幻觉。“我们可以建立一个包含所有已知[法律案件]结果的数据库并将其正式化，”他说。“我不确定这是否是最好的应用程序。”

那么软件开发人员渴望知道人工智能为他们生成的算法是否正确呢？“这个产品不是为程序员设计的，”库克说。“但这并没有逃过我们的注意。我们一直在做的实际上是对代码进行推理……25 年来我一直在证明程序的正确性。这是拥有非常重要资产的大型企业的领域，因为它是但生成式人工智能似乎能够显着降低进入门槛，帮助您正式确定您想要证明的程序内容，这非常令人兴奋，但这不包括[自动化]。推理]产品”。

• AWS 表示人工智能可能会颠覆一切，并希望 Windows 也能做到这一点
• LLM 性能作弊代码：推测性解码简介
• 据报道，谷歌正在开发一款可以控制浏览器的人工智能代理
• AI 代码助手无法停止发明包名称

库克的团队还致力于解决亚马逊的其他问题，例如证明访问控制策略按预期工作，以及加密、网络、存储和虚拟化方面的类似问题。他告诉我们，事实证明，能够在数学上证明代码正确会带来有益的副作用，其中之一就是提高代码效率。

“当你有一个自动推理工具来检查你的作业时，你可以在执行优化时更加积极。开发人员在不具备这种能力时所做的事情相当保守，如果你喜欢的话，可以将其称为防御性编码。有了这些工具他们可以执行对他们来说非常可怕的优化，我们为他们提供了很多安全性。”

他补充说，Rust 非常适合可证明的编程。“当你用 Rust 编程时，你实际上是在使用定理证明器。很多人不明白他们已经欺骗程序员做内存安全的证明，而 Rust 中的借用检查器本质上是一个演绎定理证明者。这是一个推理引擎，开发人员正在指导该工具……Rust 可以比 C 更快，原因是它能够利用内存完成 C 无法做到的聪明的事情，当然。在Java或其他语言中做不到，因为它们已经让程序员做证明了。

“所以 Rust 是自动推理技术、类型系统和编译器的非常巧妙的集成，然后它们有非常好的错误消息，使该工具非常有用。因此，我们看到了迁移到 Rust 的巨大成果对于某些类型的程序。”®