编辑 | 言征
出品 | 51CTO技术栈（微信号：blog51cto）
AI 的一个显着缺陷是它会不自知地“产生幻觉”，编造没有真实数据依据的合理答案。
AWS 正试图通过解决这个问题，一个不错的路径是：引入 Amazon Bedrock 自动推理检查。
Amazon Bedrock 是一项面向生成式 AI 应用程序的托管服务。
上个月，AWS 首席执行官 Matt Garman 在拉斯维加斯的 re:Invent 大会上发表讲话时表示，这些检查“可以防止由于模型幻觉而导致的事实错误......Bedrock 可以检查模型所做的事实陈述是否准确。
他说，这一切都基于“合理的数学验证”。如何理解这句话？他们背后隐藏着什么？
AWS 首席执行官 Matt Garman 介绍了 Bedrock 的自动推理
AWS 自动推理小组的负责人 Byron Cook 近日在采访中透露更多详细的思考。
1.与其解决AI幻觉，不如证明是否正确
“我一直在正式推理和工具领域工作。大约从 10 年前开始，我就将这种功能引入 Amazon，然后 AI 也有一些应用。现在突然之间，我所在的区域，以前非常晦涩难懂，突然变得不朦胧了。
如何减轻 AI 幻觉带来的风险，问题是可以解决的吗？
“从某种意义上说，幻觉是一件好事，因为它是创造力。但在语言模型生成过程中，其中一些结果将是不正确的，“他说。
“但是，根据谁的定义是错误的呢？事实证明，定义真理是什么，出奇地困难。即使在您认为每个人都应该同意的领域。”
“我曾在航空航天、铁路调车、操作系统、硬件、生物学等领域工作过，在所有这些领域中，我所看到的是，在构建这类工具时，大部分时间都花在了领域专家的争论中，争论正确的答案应该是什么，这些例子是由出现和打击极端情况的具体例子驱动的。”
库克补充道：“另一件事是，有些问题是无法决定的。例如，图灵已经证明了这一点。没有程序可以始终、权威地、在有限的时间内以 100% 的准确率回答问题。”
如果你尝试将所有陈述的领域分块，有些是相对正式的，而另一些则不是。什么是好的音乐将很难正式化，人们可能对此有一些理论，但他们之间可能不同意。
其他领域就像生物学一样，有生物系统如何运作的模型，但他们所做的部分工作是获取这些模型，然后检查真实的系统。他们正在努力改进模型，所以模型可能是错误的。在这些警告下，你可以做很多事情。
AWS 自动推理小组负责人 Byron Cook
Cook 介绍了 Automated Reasoning 工具，并引用了示例案例，例如根据个人的损益表确定正确的税码。
他说，该工具“采用自然语言中的陈述并将其转化为逻辑，然后证明或反驳该领域下的有效性。”
通过工具研究模型“怎么会出错”，比如：从自然语言到逻辑的翻译有可能出错，此外，人们决定什么是税法并将其正式化也可能会出错。因此，我们仍然有可能得到错误的答案，但在假设我们翻译正确的情况下，在我们帮助客户正式定义 [规则] 的假设下，我们可以在数学逻辑中构建一个被证明是正确的论点，即他们得到的答案是正确的。
库克说，幻觉“是我们必须长期忍受的问题。毕竟人类也会产生幻觉......作为一个社会，我们总是在逐渐研究什么是真理，我们如何定义它，以及谁来决定它是什么。
库克还对一个著名的 AI 幻觉案例发表评论，这位律师引用了 OpenAI 的 ChatGPT 发明的案例。库克说，这并不完全是自动推理工具所能解决的那种幻觉。“我们可以建立一个包含所有已知 [法律案件] 结果的数据库，并将其正式化，”他说。“我不确定这是否是最好的应用程序。”
图片
2.不适用于编程，但有利于开发者防御性编程
开发者们的问题是：这个自动推理工具能否为帮他们检查生成的算法代码是否正确？
“这个产品不是为程序员设计的，”Cook 说。“但它并没有逃过我们的注意。实际上我们一直在做对代码进行推理......25 年来，我一直在证明程序是正确的。这是拥有重资产的巨头企业的领域，因为这样做非常具有挑战性。但生成式 AI 似乎已经准备好能够显着降低这一进入门槛，帮助开发者正式确定想要证明的程序是什么。这非常令人兴奋，但这不包括“自动推理”产品。
Cook 的团队还在 Amazon 解决了其他问题，例如证明访问控制策略按预期工作，以及类似的加密、联网、存储和虚拟化。事实证明，“证明代码在数学上是正确的”有一个好的副作用，其中之一就是代码效率更高。
“当你有一个自动推理工具来检查你的家庭作业时，你可以更积极地进行优化。当开发人员没有这种能力时，他们所做的是相当保守的，如果你愿意，可以称之为防御性编码。使用这些工具，他们可以执行对他们来说非常可怕的优化。我们给他们很多安全。
3.Rust的借用检查器本质上就是一个推理引擎
他补充说，Rust 是可证明编程的天作之合。“当你用 Rust 编程时，你实际上是在用定理证明器。很多人并不清楚程序员实际上已经开始了‘做内存安全的证明’，而 Rust 中的借用检查器本质上是一个演绎定理证明器。它是一个推理引擎。开发人员正在指导该工具完成这一过程。
Rust 可以比 C 更快，原因是它能够用内存做一些他们在 C 中做不到的聪明事情，当然在 Java 或其他语言中也做不到，因为他们已经让程序员去做正确性地证明。
“所以 Rust 是自动推理技术、类型系统、编译器的非常聪明的集成，然后它们有非常好的错误消息，使该工具非常有用。因此，我们已经看到某些类型的程序迁移到 Rust 后取得了很好的结果。
想了解更多AIGC的内容，请访问：
51CTO AI.x社区
https://www.51cto.com/aigc/
