編輯 | 言征
出品 | 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 后取得了很好的結果。
