編輯 |  言征

出品 | 51CTO技術(shù)棧（微信號：blog51cto）

AI 的一個顯著缺陷是它會不自知地“產(chǎn)生幻覺”，編造沒有真實數(shù)據(jù)依據(jù)的合理答案。

AWS 正試圖通過解決這個問題，一個不錯的路徑是：引入 Amazon Bedrock 自動推理檢查。

Amazon Bedrock 是一項面向生成式 AI 應(yīng)用程序的托管服務(wù)。

上個月，AWS 首席執(zhí)行官 Matt Garman 在拉斯維加斯的 re:Invent 大會上發(fā)表講話時表示，這些檢查“可以防止由于模型幻覺而導致的事實錯誤......Bedrock 可以檢查模型所做的事實陳述是否準確。

他說，這一切都基于“合理的數(shù)學驗證”。如何理解這句話？他們背后隱藏著什么？

AWS 首席執(zhí)行官 Matt Garman 介紹了 Bedrock 的自動推理

AWS 自動推理小組的負責人 Byron Cook 近日在采訪中透露更多詳細的思考。

1.與其解決AI幻覺，不如證明是否正確

“我一直在正式推理和工具領(lǐng)域工作。大約從 10 年前開始，我就將這種功能引入 Amazon，然后 AI 也有一些應(yīng)用?，F(xiàn)在突然之間，我所在的區(qū)域，以前非?；逎y懂，突然變得不朦朧了。

如何減輕 AI 幻覺帶來的風險，問題是可以解決的嗎？

“從某種意義上說，幻覺是一件好事，因為它是創(chuàng)造力。但在語言模型生成過程中，其中一些結(jié)果將是不正確的，“他說。

“但是，根據(jù)誰的定義是錯誤的呢？事實證明，定義真理是什么，出奇地困難。即使在您認為每個人都應(yīng)該同意的領(lǐng)域?！?/p>

“我曾在航空航天、鐵路調(diào)車、操作系統(tǒng)、硬件、生物學等領(lǐng)域工作過，在所有這些領(lǐng)域中，我所看到的是，在構(gòu)建這類工具時，大部分時間都花在了領(lǐng)域?qū)＜业臓幷撝?，爭論正確的答案應(yīng)該是什么，這些例子是由出現(xiàn)和打擊極端情況的具體例子驅(qū)動的?！?/p>

庫克補充道：“另一件事是，有些問題是無法決定的。例如，圖靈已經(jīng)證明了這一點。沒有程序可以始終、權(quán)威地、在有限的時間內(nèi)以 100% 的準確率回答問題。”

如果你嘗試將所有陳述的領(lǐng)域分塊，有些是相對正式的，而另一些則不是。什么是好的音樂將很難正式化，人們可能對此有一些理論，但他們之間可能不同意。

其他領(lǐng)域就像生物學一樣，有生物系統(tǒng)如何運作的模型，但他們所做的部分工作是獲取這些模型，然后檢查真實的系統(tǒng)。他們正在努力改進模型，所以模型可能是錯誤的。在這些警告下，你可以做很多事情。

AWS 自動推理小組負責人 Byron Cook

Cook 介紹了 Automated Reasoning 工具，并引用了示例案例，例如根據(jù)個人的損益表確定正確的稅碼。

他說，該工具“采用自然語言中的陳述并將其轉(zhuǎn)化為邏輯，然后證明或反駁該領(lǐng)域下的有效性。”

通過工具研究模型“怎么會出錯”，比如：從自然語言到邏輯的翻譯有可能出錯，此外，人們決定什么是稅法并將其正式化也可能會出錯。因此，我們?nèi)匀挥锌赡艿玫藉e誤的答案，但在假設(shè)我們翻譯正確的情況下，在我們幫助客戶正式定義 [規(guī)則] 的假設(shè)下，我們可以在數(shù)學邏輯中構(gòu)建一個被證明是正確的論點，即他們得到的答案是正確的。

庫克說，幻覺“是我們必須長期忍受的問題。畢竟人類也會產(chǎn)生幻覺......作為一個社會，我們總是在逐漸研究什么是真理，我們?nèi)绾味x它，以及誰來決定它是什么。

庫克還對一個著名的 AI 幻覺案例發(fā)表評論，這位律師引用了 OpenAI 的 ChatGPT 發(fā)明的案例。庫克說，這并不完全是自動推理工具所能解決的那種幻覺。“我們可以建立一個包含所有已知 [法律案件] 結(jié)果的數(shù)據(jù)庫，并將其正式化，”他說。“我不確定這是否是最好的應(yīng)用程序?！?/p>

圖片

2.不適用于編程，但有利于開發(fā)者防御性編程

開發(fā)者們的問題是：這個自動推理工具能否為幫他們檢查生成的算法代碼是否正確？

“這個產(chǎn)品不是為程序員設(shè)計的，”Cook 說。“但它并沒有逃過我們的注意。實際上我們一直在做對代碼進行推理......25 年來，我一直在證明程序是正確的。這是擁有重資產(chǎn)的巨頭企業(yè)的領(lǐng)域，因為這樣做非常具有挑戰(zhàn)性。但生成式 AI 似乎已經(jīng)準備好能夠顯著降低這一進入門檻，幫助開發(fā)者正式確定想要證明的程序是什么。這非常令人興奮，但這不包括“自動推理”產(chǎn)品。

Cook 的團隊還在 Amazon 解決了其他問題，例如證明訪問控制策略按預(yù)期工作，以及類似的加密、聯(lián)網(wǎng)、存儲和虛擬化。事實證明，“證明代碼在數(shù)學上是正確的”有一個好的副作用，其中之一就是代碼效率更高。

“當你有一個自動推理工具來檢查你的家庭作業(yè)時，你可以更積極地進行優(yōu)化。當開發(fā)人員沒有這種能力時，他們所做的是相當保守的，如果你愿意，可以稱之為防御性編碼。使用這些工具，他們可以執(zhí)行對他們來說非?？膳碌膬?yōu)化。我們給他們很多安全。

3.Rust的借用檢查器本質(zhì)上就是一個推理引擎

他補充說，Rust 是可證明編程的天作之合?！爱斈阌?Rust 編程時，你實際上是在用定理證明器。很多人并不清楚程序員實際上已經(jīng)開始了‘做內(nèi)存安全的證明’，而 Rust 中的借用檢查器本質(zhì)上是一個演繹定理證明器。它是一個推理引擎。開發(fā)人員正在指導該工具完成這一過程。

Rust 可以比 C 更快，原因是它能夠用內(nèi)存做一些他們在 C 中做不到的聰明事情，當然在 Java 或其他語言中也做不到，因為他們已經(jīng)讓程序員去做正確性地證明。

“所以 Rust 是自動推理技術(shù)、類型系統(tǒng)、編譯器的非常聰明的集成，然后它們有非常好的錯誤消息，使該工具非常有用。因此，我們已經(jīng)看到某些類型的程序遷移到 Rust 后取得了很好的結(jié)果。 

本文轉(zhuǎn)載自??51CTO技術(shù)棧??，作者：言征