編輯 | 言征
出品 | 51CTO技術(shù)棧（微信號(hào)：blog51cto）
AI 的一個(gè)顯著缺陷是它會(huì)不自知地“產(chǎn)生幻覺(jué)”，編造沒(méi)有真實(shí)數(shù)據(jù)依據(jù)的合理答案。
AWS 正試圖通過(guò)解決這個(gè)問(wèn)題，一個(gè)不錯(cuò)的路徑是：引入 Amazon Bedrock 自動(dòng)推理檢查。
Amazon Bedrock 是一項(xiàng)面向生成式 AI 應(yīng)用程序的托管服務(wù)。
上個(gè)月，AWS 首席執(zhí)行官 Matt Garman 在拉斯維加斯的 re:Invent 大會(huì)上發(fā)表講話(huà)時(shí)表示，這些檢查“可以防止由于模型幻覺(jué)而導(dǎo)致的事實(shí)錯(cuò)誤......Bedrock 可以檢查模型所做的事實(shí)陳述是否準(zhǔn)確。
他說(shuō)，這一切都基于“合理的數(shù)學(xué)驗(yàn)證”。如何理解這句話(huà)？他們背后隱藏著什么？
AWS 首席執(zhí)行官 Matt Garman 介紹了 Bedrock 的自動(dòng)推理
AWS 自動(dòng)推理小組的負(fù)責(zé)人 Byron Cook 近日在采訪(fǎng)中透露更多詳細(xì)的思考。
1.與其解決AI幻覺(jué)，不如證明是否正確
“我一直在正式推理和工具領(lǐng)域工作。大約從 10 年前開(kāi)始，我就將這種功能引入 Amazon，然后 AI 也有一些應(yīng)用。現(xiàn)在突然之間，我所在的區(qū)域，以前非?；逎y懂，突然變得不朦朧了。
如何減輕 AI 幻覺(jué)帶來(lái)的風(fēng)險(xiǎn)，問(wèn)題是可以解決的嗎？
“從某種意義上說(shuō)，幻覺(jué)是一件好事，因?yàn)樗莿?chuàng)造力。但在語(yǔ)言模型生成過(guò)程中，其中一些結(jié)果將是不正確的，“他說(shuō)。
“但是，根據(jù)誰(shuí)的定義是錯(cuò)誤的呢？事實(shí)證明，定義真理是什么，出奇地困難。即使在您認(rèn)為每個(gè)人都應(yīng)該同意的領(lǐng)域?！?/span>
“我曾在航空航天、鐵路調(diào)車(chē)、操作系統(tǒng)、硬件、生物學(xué)等領(lǐng)域工作過(guò)，在所有這些領(lǐng)域中，我所看到的是，在構(gòu)建這類(lèi)工具時(shí)，大部分時(shí)間都花在了領(lǐng)域?qū)＜业臓?zhēng)論中，爭(zhēng)論正確的答案應(yīng)該是什么，這些例子是由出現(xiàn)和打擊極端情況的具體例子驅(qū)動(dòng)的。”
庫(kù)克補(bǔ)充道：“另一件事是，有些問(wèn)題是無(wú)法決定的。例如，圖靈已經(jīng)證明了這一點(diǎn)。沒(méi)有程序可以始終、權(quán)威地、在有限的時(shí)間內(nèi)以 100% 的準(zhǔn)確率回答問(wèn)題。”
如果你嘗試將所有陳述的領(lǐng)域分塊，有些是相對(duì)正式的，而另一些則不是。什么是好的音樂(lè)將很難正式化，人們可能對(duì)此有一些理論，但他們之間可能不同意。
其他領(lǐng)域就像生物學(xué)一樣，有生物系統(tǒng)如何運(yùn)作的模型，但他們所做的部分工作是獲取這些模型，然后檢查真實(shí)的系統(tǒng)。他們正在努力改進(jìn)模型，所以模型可能是錯(cuò)誤的。在這些警告下，你可以做很多事情。
AWS 自動(dòng)推理小組負(fù)責(zé)人 Byron Cook
Cook 介紹了 Automated Reasoning 工具，并引用了示例案例，例如根據(jù)個(gè)人的損益表確定正確的稅碼。
他說(shuō)，該工具“采用自然語(yǔ)言中的陳述并將其轉(zhuǎn)化為邏輯，然后證明或反駁該領(lǐng)域下的有效性?！?/span>
通過(guò)工具研究模型“怎么會(huì)出錯(cuò)”，比如：從自然語(yǔ)言到邏輯的翻譯有可能出錯(cuò)，此外，人們決定什么是稅法并將其正式化也可能會(huì)出錯(cuò)。因此，我們?nèi)匀挥锌赡艿玫藉e(cuò)誤的答案，但在假設(shè)我們翻譯正確的情況下，在我們幫助客戶(hù)正式定義 [規(guī)則] 的假設(shè)下，我們可以在數(shù)學(xué)邏輯中構(gòu)建一個(gè)被證明是正確的論點(diǎn)，即他們得到的答案是正確的。
庫(kù)克說(shuō)，幻覺(jué)“是我們必須長(zhǎng)期忍受的問(wèn)題。畢竟人類(lèi)也會(huì)產(chǎn)生幻覺(jué)......作為一個(gè)社會(huì)，我們總是在逐漸研究什么是真理，我們?nèi)绾味x它，以及誰(shuí)來(lái)決定它是什么。
庫(kù)克還對(duì)一個(gè)著名的 AI 幻覺(jué)案例發(fā)表評(píng)論，這位律師引用了 OpenAI 的 ChatGPT 發(fā)明的案例。庫(kù)克說(shuō)，這并不完全是自動(dòng)推理工具所能解決的那種幻覺(jué)?！拔覀兛梢越⒁粋€(gè)包含所有已知 [法律案件] 結(jié)果的數(shù)據(jù)庫(kù)，并將其正式化，”他說(shuō)?！拔也淮_定這是否是最好的應(yīng)用程序。”
圖片
2.不適用于編程，但有利于開(kāi)發(fā)者防御性編程
開(kāi)發(fā)者們的問(wèn)題是：這個(gè)自動(dòng)推理工具能否為幫他們檢查生成的算法代碼是否正確？
“這個(gè)產(chǎn)品不是為程序員設(shè)計(jì)的，”Cook 說(shuō)。“但它并沒(méi)有逃過(guò)我們的注意。實(shí)際上我們一直在做對(duì)代碼進(jìn)行推理......25 年來(lái)，我一直在證明程序是正確的。這是擁有重資產(chǎn)的巨頭企業(yè)的領(lǐng)域，因?yàn)檫@樣做非常具有挑戰(zhàn)性。但生成式 AI 似乎已經(jīng)準(zhǔn)備好能夠顯著降低這一進(jìn)入門(mén)檻，幫助開(kāi)發(fā)者正式確定想要證明的程序是什么。這非常令人興奮，但這不包括“自動(dòng)推理”產(chǎn)品。
Cook 的團(tuán)隊(duì)還在 Amazon 解決了其他問(wèn)題，例如證明訪(fǎng)問(wèn)控制策略按預(yù)期工作，以及類(lèi)似的加密、聯(lián)網(wǎng)、存儲(chǔ)和虛擬化。事實(shí)證明，“證明代碼在數(shù)學(xué)上是正確的”有一個(gè)好的副作用，其中之一就是代碼效率更高。
“當(dāng)你有一個(gè)自動(dòng)推理工具來(lái)檢查你的家庭作業(yè)時(shí)，你可以更積極地進(jìn)行優(yōu)化。當(dāng)開(kāi)發(fā)人員沒(méi)有這種能力時(shí)，他們所做的是相當(dāng)保守的，如果你愿意，可以稱(chēng)之為防御性編碼。使用這些工具，他們可以執(zhí)行對(duì)他們來(lái)說(shuō)非常可怕的優(yōu)化。我們給他們很多安全。
3.Rust的借用檢查器本質(zhì)上就是一個(gè)推理引擎
他補(bǔ)充說(shuō)，Rust 是可證明編程的天作之合?！爱?dāng)你用 Rust 編程時(shí)，你實(shí)際上是在用定理證明器。很多人并不清楚程序員實(shí)際上已經(jīng)開(kāi)始了‘做內(nèi)存安全的證明’，而 Rust 中的借用檢查器本質(zhì)上是一個(gè)演繹定理證明器。它是一個(gè)推理引擎。開(kāi)發(fā)人員正在指導(dǎo)該工具完成這一過(guò)程。
Rust 可以比 C 更快，原因是它能夠用內(nèi)存做一些他們?cè)?C 中做不到的聰明事情，當(dāng)然在 Java 或其他語(yǔ)言中也做不到，因?yàn)樗麄円呀?jīng)讓程序員去做正確性地證明。
“所以 Rust 是自動(dòng)推理技術(shù)、類(lèi)型系統(tǒng)、編譯器的非常聰明的集成，然后它們有非常好的錯(cuò)誤消息，使該工具非常有用。因此，我們已經(jīng)看到某些類(lèi)型的程序遷移到 Rust 后取得了很好的結(jié)果。
