這項由伊利諾伊大學(xué)香檳分校的塔倫·蘇雷什、納林·瓦德瓦、德班舒·班納吉和加甘迪普·辛格領(lǐng)導(dǎo)的研究發(fā)表于2025年12月的arXiv預(yù)印本論文庫（論文編號：arXiv:2512.05439v1），有興趣深入了解的讀者可以通過該編號查詢完整論文。這項研究在人工智能驗證領(lǐng)域?qū)崿F(xiàn)了重要突破，首次提供了一個名為BEAVER的框架，能夠?qū)Υ笮驼Z言模型的輸出可靠性進(jìn)行精確的數(shù)學(xué)驗證。

隨著ChatGPT等大型語言模型從實驗室走向?qū)嶋H應(yīng)用，一個關(guān)鍵問題逐漸浮現(xiàn)：我們?nèi)绾未_保這些AI系統(tǒng)在關(guān)鍵場景下的表現(xiàn)可靠？當(dāng)前的做法就像盲人摸象一樣，只能通過抽樣測試來估算模型的表現(xiàn)，無法給出確切的保證。研究團(tuán)隊意識到，這種不確定性在醫(yī)療診斷、金融分析或自動駕駛等高風(fēng)險場景中是不可接受的。

傳統(tǒng)的檢測方法就像在黑暗中投硬幣來判斷一個袋子里硬幣的比例。你只能抽取一些樣本，基于這些有限的觀察來猜測整體情況，但永遠(yuǎn)無法確定真實的比例。而BEAVER就像給你提供了一個精密的天平和計數(shù)器，能夠給出準(zhǔn)確的上限和下限范圍，告訴你真實比例一定在某個確定區(qū)間內(nèi)。

BEAVER的核心創(chuàng)新在于將語言模型的生成過程比作探索一片未知森林的過程。當(dāng)模型開始生成文本時，就像從森林入口出發(fā)，每選擇一個詞匯就相當(dāng)于在森林中選擇一條路徑。傳統(tǒng)方法是隨機(jī)游走，走到哪里算哪里，然后根據(jù)有限的幾次探索來推測整個森林的情況。而BEAVER則像一位經(jīng)驗豐富的探險家，系統(tǒng)性地探索森林，建立詳細(xì)的地圖，并能夠精確計算出符合條件路徑的概率范圍。

研究團(tuán)隊選擇了三個具有代表性的驗證任務(wù)來測試BEAVER的效果。第一個是數(shù)學(xué)正確性驗證，使用GSM-Symbolic數(shù)學(xué)推理基準(zhǔn)測試。這個任務(wù)就像檢驗一位數(shù)學(xué)老師在解題時的準(zhǔn)確率，需要驗證模型生成的數(shù)學(xué)表達(dá)式是否真正能夠解決給定的問題。第二個是隱私保護(hù)驗證，通過Enron郵件泄露數(shù)據(jù)集來測試模型是否會意外泄露敏感信息。這就像檢驗一位秘書在處理機(jī)密文件時是否會無意中透露不該說的內(nèi)容。第三個是安全代碼生成驗證，使用CyberSeceval基準(zhǔn)測試來檢查模型生成的代碼是否包含安全漏洞。這相當(dāng)于檢驗一位程序員寫出的代碼是否存在被黑客利用的風(fēng)險。

一、BEAVER的工作原理：像偵探一樣系統(tǒng)追蹤

理解BEAVER的工作方式，可以把它想象成一位極其細(xì)致的偵探在調(diào)查一個復(fù)雜案件。當(dāng)語言模型開始生成文本時，BEAVER會建立一個叫做"令牌樹"的數(shù)據(jù)結(jié)構(gòu)，就像偵探在案發(fā)現(xiàn)場繪制的詳細(xì)地圖。這個地圖記錄了模型可能選擇的每一條路徑，以及每條路徑的概率。

BEAVER的獨特之處在于它采用了"前綴封閉"的概念。這個概念可以用交通違章來類比：如果一個司機(jī)在某條路上違反了交通規(guī)則，那么他繼續(xù)在這條路上行駛只會讓違章行為變得更嚴(yán)重，不可能突然變成合規(guī)行為。同樣，如果一個文本序列在某個位置就已經(jīng)違反了約束條件，那么在后面添加任何內(nèi)容都不可能讓它重新符合要求。這個特性讓BEAVER能夠在發(fā)現(xiàn)問題的第一時間就"剪枝"，避免浪費時間探索注定無效的路徑。

BEAVER維護(hù)著兩個關(guān)鍵的數(shù)據(jù)結(jié)構(gòu)。第一個是令牌樹，記錄所有探索過的合規(guī)路徑及其概率。第二個是前沿隊列，包含當(dāng)前所有未完成的序列和已完成的序列。就像一個探險隊在森林中同時進(jìn)行多條路線的探索，前沿隊列告訴我們哪些路線還在進(jìn)行中，哪些已經(jīng)到達(dá)了終點。

BEAVER的算法遵循三個步驟的循環(huán)過程。首先是選擇步驟，從前沿隊列中挑選一個未完成的序列進(jìn)行擴(kuò)展。研究團(tuán)隊開發(fā)了兩種選擇策略：Max-μ策略總是選擇概率最高的序列繼續(xù)探索，就像優(yōu)先探索最有希望的線索；Sample-μ策略則按概率隨機(jī)選擇，類似于在多條有希望的線索中隨機(jī)分配偵探資源。

接下來是擴(kuò)展步驟，BEAVER會查詢語言模型獲得下一個詞匯的概率分布，然后只保留那些不違反約束條件的延續(xù)路徑。這就像偵探在每個岔路口都會檢查前進(jìn)的方向是否符合法律法規(guī)。最后是更新步驟，BEAVER會重新計算概率的上限和下限，就像偵探在獲得新線索后會重新評估案件的各種可能性。

這個過程的巧妙之處在于它能夠提供"隨時保證"。無論何時停止計算，BEAVER都能給出當(dāng)前最準(zhǔn)確的概率范圍。這就像一位優(yōu)秀的偵探，即使調(diào)查還沒有完全結(jié)束，也能根據(jù)已有證據(jù)給出案件真相的可信區(qū)間。

二、數(shù)學(xué)基礎(chǔ)：為AI驗證提供堅實理論支撐

BEAVER的數(shù)學(xué)基礎(chǔ)可以用一個精妙的比喻來解釋。假設(shè)你有一個巨大的圖書館，里面存放著語言模型可能生成的所有文本序列。每本書都有一個標(biāo)簽，顯示模型生成這個序列的概率。現(xiàn)在你想知道其中有多少比例的書籍滿足某個特定條件，比如"內(nèi)容必須是正確的數(shù)學(xué)表達(dá)式"。

傳統(tǒng)方法就像閉著眼睛隨機(jī)抽取幾本書，然后基于這個小樣本來估算整個圖書館的情況。這種方法的問題是顯而易見的：如果運(yùn)氣不好，抽到的樣本不具代表性，結(jié)論就會大相徑庭。而且，無論抽取多少本書，你都無法確定真實比例到底是多少，只能說"大概在某個范圍內(nèi)"。

BEAVER則采用了完全不同的策略。它不是隨機(jī)抽樣，而是系統(tǒng)性地建立圖書館的目錄索引。這個索引記錄了每個書架（對應(yīng)文本前綴）上所有書籍的總概率。通過這種方式，BEAVER能夠精確計算出滿足條件的書籍的概率下限和上限。

研究團(tuán)隊在論文中提供了嚴(yán)格的數(shù)學(xué)證明，確保BEAVER計算出的概率邊界始終是正確的。這些證明就像建筑工程師的結(jié)構(gòu)計算，確保整個框架在任何情況下都不會"塌陷"。核心的健全性定理保證了真實概率永遠(yuǎn)位于BEAVER給出的上限和下限之間。單調(diào)性定理則確保隨著計算的進(jìn)行，這個區(qū)間會越來越緊，就像聚焦鏡頭一樣逐漸清晰。

時間復(fù)雜度分析顯示，BEAVER的計算成本主要來自兩個方面：模型的前向傳播和約束條件的驗證。對于輕量級的約束條件（如模式匹配或語法檢查），這個開銷是完全可以接受的。但對于需要調(diào)用外部工具的復(fù)雜約束（如需要SMT求解器的數(shù)學(xué)正確性檢查），計算成本會相應(yīng)增加。不過，研究團(tuán)隊指出，這種成本投入是值得的，因為它提供了傳統(tǒng)方法無法企及的確定性保證。

三、實驗驗證：在三大關(guān)鍵場景中證明實力

研究團(tuán)隊精心設(shè)計了三個實驗來驗證BEAVER的有效性，這三個實驗分別針對AI應(yīng)用中最關(guān)鍵的三個方面：正確性、隱私性和安全性。每個實驗都選擇了該領(lǐng)域最具挑戰(zhàn)性的基準(zhǔn)測試，確保驗證結(jié)果具有說服力。

在數(shù)學(xué)正確性驗證實驗中，研究團(tuán)隊使用了GSM-Symbolic數(shù)據(jù)集，這是一個包含100個符號數(shù)學(xué)問題的基準(zhǔn)測試。這個數(shù)據(jù)集的特殊之處在于它使用符號變量而非具體數(shù)字，使得問題更加抽象和具有挑戰(zhàn)性。就像讓一個學(xué)生解答"求解關(guān)于x和y的方程組"而非具體的數(shù)字題目，這要求更深層的數(shù)學(xué)理解能力。

實驗結(jié)果令人印象深刻。在Qwen3-4B模型上，傳統(tǒng)的拒絕采樣方法給出的概率區(qū)間是[0.341, 0.433]，區(qū)間寬度達(dá)到0.092，這意味著我們對模型真實表現(xiàn)的了解非常模糊。而BEAVER給出的區(qū)間是[0.343, 0.356]，區(qū)間寬度僅為0.013，精確度提高了大約7倍。這就像從用模糊的望遠(yuǎn)鏡觀察遠(yuǎn)山，突然換成了高清顯微鏡，細(xì)節(jié)一下子變得清晰可見。

更重要的是，BEAVER還顯著提高了計算效率。傳統(tǒng)方法需要平均49次前向傳播才能達(dá)到收斂，而BEAVER只需要約25次。這種效率提升來源于BEAVER的系統(tǒng)性探索策略，避免了傳統(tǒng)方法中大量重復(fù)采樣的問題。

隱私保護(hù)驗證實驗使用了Enron郵件數(shù)據(jù)集，這個數(shù)據(jù)集包含了真實的企業(yè)郵件通信記錄。實驗的目標(biāo)是檢測模型是否會在生成文本時意外泄露這些郵件地址。這個實驗?zāi)M了一個現(xiàn)實世界的重要擔(dān)憂：AI模型在訓(xùn)練過程中可能記住了訓(xùn)練數(shù)據(jù)中的敏感信息，并在后續(xù)使用中無意泄露。

在這個任務(wù)上，BEAVER展現(xiàn)出了驚人的敏感性。對于Qwen3-4B模型，傳統(tǒng)方法只識別出了15%的高風(fēng)險實例（即模型有較高概率泄露郵件地址的情況），而BEAVER識別出了67%的高風(fēng)險實例，提升了4倍多。這種差異的意義重大：在實際部署中，傳統(tǒng)方法可能會給出"模型是安全的"這樣的誤導(dǎo)性結(jié)論，而BEAVER能夠發(fā)現(xiàn)潛在的隱私泄露風(fēng)險，為企業(yè)的決策提供更可靠的依據(jù)。

安全代碼生成驗證實驗使用了CyberSeceval基準(zhǔn)測試中的Rust代碼自動補(bǔ)全任務(wù)。為了模擬最具挑戰(zhàn)性的場景，研究團(tuán)隊還添加了"越獄"提示詞，試圖誘導(dǎo)模型生成包含安全漏洞的代碼。這就像故意給程序員施加壓力，看他們是否會在緊急情況下寫出有問題的代碼。

實驗結(jié)果再次證明了BEAVER的價值。對于Qwen3-4B模型，傳統(tǒng)方法只發(fā)現(xiàn)了4%的高風(fēng)險實例，而BEAVER發(fā)現(xiàn)了33%的高風(fēng)險實例，差距達(dá)到了8倍。這意味著如果依賴傳統(tǒng)方法進(jìn)行安全評估，可能會嚴(yán)重低估模型在對抗性環(huán)境下的安全風(fēng)險。

研究團(tuán)隊還進(jìn)行了一系列對比實驗來驗證不同設(shè)計選擇的影響。他們發(fā)現(xiàn)Max-μ選擇策略通常比Sample-μ策略收斂更快，但兩者的最終精度相當(dāng)。溫度參數(shù)的調(diào)整也會顯著影響驗證效果：較低的溫度（0.33）會讓概率分布更加集中，使得BEAVER能夠更快地收斂到緊密的區(qū)間。

四、技術(shù)創(chuàng)新：突破傳統(tǒng)驗證方法的局限

BEAVER的技術(shù)創(chuàng)新可以從幾個維度來理解。首先是數(shù)據(jù)結(jié)構(gòu)的創(chuàng)新。令牌樹這個概念雖然借鑒了傳統(tǒng)的前綴樹結(jié)構(gòu)，但BEAVER對其進(jìn)行了重要擴(kuò)展。傳統(tǒng)的前綴樹只記錄字符串的存在性，而BEAVER的令牌樹還記錄了每個節(jié)點對應(yīng)的概率信息。這就像從簡單的地圖升級為帶有海拔和地形信息的三維地圖，信息密度大大增加。

前沿管理策略是另一個重要創(chuàng)新。BEAVER維護(hù)的前沿包含兩個子集：完整序列集合和未完整序列集合。這種分離管理讓BEAVER能夠精確地計算概率邊界。完整序列貢獻(xiàn)下限，而所有序列（包括未完整的）貢獻(xiàn)上限。這種設(shè)計的巧妙之處在于，它自動保證了邊界的單調(diào)收斂性：隨著更多序列被探索，邊界會越來越緊。

分支策略的選擇也體現(xiàn)了深刻的算法洞察。Max-μ策略基于一個直觀的想法：優(yōu)先探索高概率的路徑能夠更快地收緊概率邊界。這類似于在尋寶游戲中優(yōu)先搜索最有希望的區(qū)域。Sample-μ策略則提供了隨機(jī)性，有助于避免陷入局部最優(yōu)解，類似于在搜索過程中保持一定的探索性。

BEAVER還創(chuàng)新性地解決了約束驗證的效率問題。通過前綴封閉性質(zhì)，BEAVER能夠在檢測到約束違規(guī)的第一時間就終止該分支的探索，避免了大量無效的計算。這種早期剪枝策略在實際應(yīng)用中能夠節(jié)省大量計算資源。

與傳統(tǒng)深度神經(jīng)網(wǎng)絡(luò)驗證方法的對比也很有啟發(fā)性。傳統(tǒng)DNN驗證方法主要針對前饋網(wǎng)絡(luò)的確定性輸出，使用抽象解釋或SMT求解器來證明性質(zhì)。但語言模型的自回歸生成過程涉及多次前向傳播和離散的解碼步驟，這種混合了連續(xù)計算和離散選擇的過程超出了傳統(tǒng)符號驗證框架的表達(dá)能力。BEAVER通過概率邊界計算的方式巧妙地繞過了這個問題。

約束條件的處理也展現(xiàn)了BEAVER的靈活性。研究團(tuán)隊展示了如何將非前綴封閉的約束轉(zhuǎn)換為前綴封閉的形式。比如，日期格式檢查（如YYYY-MM-DD）本身不是前綴封閉的，因為"2024"這個前綴違反了完整格式但可能擴(kuò)展為合規(guī)的"2024-10-15"。但可以定義一個新的約束："序列可以擴(kuò)展為有效日期格式"，這個約束就是前綴封閉的。

五、實際應(yīng)用價值：為AI安全部署提供保障

BEAVER的實際應(yīng)用價值遠(yuǎn)超其理論意義。在當(dāng)前AI快速發(fā)展的時代，模型的可靠性驗證已經(jīng)成為制約AI大規(guī)模部署的關(guān)鍵瓶頸。BEAVER為這個問題提供了一個切實可行的解決方案。

在醫(yī)療AI應(yīng)用中，BEAVER能夠為模型的診斷建議提供可信度評估。醫(yī)生可以根據(jù)BEAVER給出的概率邊界來判斷AI建議的可靠性，從而做出更明智的臨床決策。比如，如果BEAVER顯示模型給出正確診斷的概率下限為85%，醫(yī)生就可以更有信心采納AI的建議；如果下限只有60%，醫(yī)生就需要更謹(jǐn)慎地驗證診斷結(jié)果。

在金融科技領(lǐng)域，BEAVER可以用來驗證AI交易算法的風(fēng)險控制能力。監(jiān)管機(jī)構(gòu)可以要求金融機(jī)構(gòu)使用BEAVER來評估其AI系統(tǒng)在不同市場條件下的表現(xiàn)，確保系統(tǒng)不會在極端情況下產(chǎn)生過度風(fēng)險的交易決策。

在自動駕駛技術(shù)中，BEAVER可以驗證AI決策系統(tǒng)的安全性。比如，驗證在遇到緊急情況時，系統(tǒng)做出正確決策的概率是否達(dá)到安全標(biāo)準(zhǔn)。這種驗證對于自動駕駛技術(shù)的監(jiān)管審批具有重要意義。

代碼生成AI的安全驗證是另一個重要應(yīng)用場景。隨著GitHub Copilot等AI編程助手的普及，確保生成代碼的安全性變得越來越重要。BEAVER可以幫助開發(fā)團(tuán)隊評估AI生成代碼的安全風(fēng)險，特別是在處理敏感數(shù)據(jù)或關(guān)鍵基礎(chǔ)設(shè)施的項目中。

BEAVER還為AI模型的比較和選擇提供了客觀標(biāo)準(zhǔn)。傳統(tǒng)上，選擇AI模型主要依賴經(jīng)驗和有限的測試，這種方法既不科學(xué)也不可靠。有了BEAVER，決策者可以基于精確的概率邊界來比較不同模型的性能和可靠性，從而做出更明智的技術(shù)選型決策。

教育科技是另一個有前景的應(yīng)用領(lǐng)域。AI教學(xué)助手需要確保提供的答案和解釋是正確的，特別是在數(shù)學(xué)、科學(xué)等需要精確性的學(xué)科中。BEAVER可以幫助評估AI教學(xué)內(nèi)容的準(zhǔn)確性，為教育質(zhì)量提供保障。

從監(jiān)管角度看，BEAVER為AI系統(tǒng)的安全監(jiān)管提供了技術(shù)工具。監(jiān)管機(jī)構(gòu)可以要求高風(fēng)險AI應(yīng)用使用BEAVER這樣的驗證框架來證明其安全性和可靠性。這種技術(shù)標(biāo)準(zhǔn)的建立對于AI行業(yè)的健康發(fā)展具有重要意義。

BEAVER的開源發(fā)布也具有重要的產(chǎn)業(yè)價值。研究團(tuán)隊將完整的實現(xiàn)代碼、實驗?zāi)_本和數(shù)據(jù)集公開發(fā)布，使得其他研究者和工程師可以基于BEAVER進(jìn)行進(jìn)一步的創(chuàng)新和改進(jìn)。這種開放策略有助于建立AI驗證技術(shù)的生態(tài)系統(tǒng)。

六、局限性與未來發(fā)展方向

盡管BEAVER取得了顯著成果，但研究團(tuán)隊也坦誠地討論了當(dāng)前方法的局限性。這種科學(xué)的誠實態(tài)度體現(xiàn)了扎實的研究作風(fēng)，也為未來的改進(jìn)指明了方向。

前綴封閉性約束是BEAVER最主要的限制。雖然許多重要的約束條件確實具有前綴封閉性質(zhì)，比如安全性過濾、語法規(guī)范和模式回避，但仍有一些約束條件難以轉(zhuǎn)換為前綴封閉形式。研究團(tuán)隊舉例說明了如何將某些非前綴封閉約束轉(zhuǎn)換為前綴封閉變體，但這種轉(zhuǎn)換并非總是可能的。擴(kuò)展到更廣泛的約束類別需要根本性的算法創(chuàng)新。

模型訪問要求是另一個現(xiàn)實限制。BEAVER需要白盒訪問模型內(nèi)部，特別是需要獲得每個生成步驟的完整概率分布，且不能有噪聲或后處理。這排除了對黑盒API模型的驗證，也無法處理為了隱私保護(hù)而添加噪聲的模型。隨著專有模型在生產(chǎn)環(huán)境中的主導(dǎo)地位日益增強(qiáng)，開發(fā)與有限模型訪問兼容的驗證技術(shù)成為一個重要的開放性挑戰(zhàn)。

計算成本也是一個需要考慮的因素。雖然對于輕量級約束條件（如模式匹配），BEAVER的計算開銷是可接受的，但對于需要外部工具的復(fù)雜約束條件，成本可能變得顯著。比如，數(shù)學(xué)正確性檢查需要調(diào)用Z3求解器，安全性檢查需要靜態(tài)分析工具，這些外部調(diào)用的累積成本可能會主導(dǎo)整個驗證過程。

選擇策略的優(yōu)化是一個有前景的改進(jìn)方向。當(dāng)前BEAVER主要使用兩種策略：Max-μ和Sample-μ，但肯定還有更多可能的選擇策略。比如，可以根據(jù)約束條件的特性來動態(tài)調(diào)整選擇策略，或者使用機(jī)器學(xué)習(xí)方法來學(xué)習(xí)最優(yōu)的選擇策略。系統(tǒng)性地探索前沿擴(kuò)展策略可能帶來顯著的效率提升。

緩存和增量評估是另一個優(yōu)化方向。對于共享前綴的約束結(jié)果，可以開發(fā)緩存機(jī)制來避免重復(fù)計算。對于具有特殊結(jié)構(gòu)的前綴封閉約束，可以開發(fā)增量評估技術(shù)來利用前綴的計算結(jié)果。批量評估多個候選延續(xù)也可能提高效率。

擴(kuò)展到提示分布驗證是一個自然的下一步。當(dāng)前BEAVER專注于單個提示的驗證，但實際應(yīng)用中往往需要驗證模型在一個提示分布上的表現(xiàn)。開發(fā)能夠處理提示分布的驗證技術(shù)具有重要的實際價值。

多輪對話的安全驗證也是一個重要的研究方向。隨著AI助手在多輪對話場景中的廣泛應(yīng)用，驗證模型在對話過程中的安全性和一致性變得越來越重要。這需要擴(kuò)展BEAVER的框架來處理對話歷史和上下文依賴。

公平性驗證是另一個有前景的應(yīng)用領(lǐng)域。AI系統(tǒng)的公平性和偏見問題日益受到關(guān)注，BEAVER的框架可能為量化和驗證AI系統(tǒng)的公平性提供新的工具。

幻覺量化是大語言模型研究中的熱點問題，BEAVER的精確概率計算能力為解決這個問題提供了新的角度。通過定義適當(dāng)?shù)募s束條件，可以量化模型生成虛假或不一致信息的概率。

說到底，BEAVER雖然在AI驗證領(lǐng)域取得了重要突破，但這只是一個開始。隨著AI技術(shù)的快速發(fā)展，驗證技術(shù)也需要持續(xù)演進(jìn)。研究團(tuán)隊的開源策略為這種演進(jìn)提供了良好的基礎(chǔ)，相信在整個研究社區(qū)的共同努力下，AI驗證技術(shù)將變得更加完善和實用。

從更廣的視角來看，BEAVER代表了AI安全研究的一個重要趨勢：從經(jīng)驗性的測試轉(zhuǎn)向數(shù)學(xué)化的驗證。這種轉(zhuǎn)變對于AI技術(shù)的成熟和廣泛應(yīng)用具有深遠(yuǎn)意義。當(dāng)我們能夠為AI系統(tǒng)的行為提供數(shù)學(xué)保證時，AI技術(shù)才能真正進(jìn)入需要高可靠性的關(guān)鍵應(yīng)用領(lǐng)域。

對于普通人而言，BEAVER的意義可能不會立即顯現(xiàn)，但它為未來更安全、更可靠的AI應(yīng)用奠定了技術(shù)基礎(chǔ)。當(dāng)你使用AI醫(yī)療診斷、AI金融顧問或AI教育助手時，背后可能就有BEAVER這樣的驗證技術(shù)在默默保障你的安全和利益。這項研究讓我們離真正可信的AI又近了一步。

Q&A

Q1：BEAVER是什么技術(shù)？

A：BEAVER是伊利諾伊大學(xué)香檳分校開發(fā)的AI驗證框架，能夠精確計算大語言模型滿足特定約束條件的概率范圍。它通過系統(tǒng)性探索模型的生成空間，給出數(shù)學(xué)上可靠的概率上限和下限，而不是傳統(tǒng)方法的模糊估算。

Q2：BEAVER比傳統(tǒng)驗證方法強(qiáng)在哪里？

A：BEAVER比傳統(tǒng)的拒絕采樣方法精確6-8倍。比如在數(shù)學(xué)正確性驗證中，傳統(tǒng)方法給出的概率區(qū)間寬度是0.092，而BEAVER只有0.013。同時BEAVER還能發(fā)現(xiàn)3-4倍更多的高風(fēng)險實例，為AI安全提供更可靠的保障。

Q3：BEAVER有什么實際應(yīng)用價值？

A：BEAVER可以用于醫(yī)療AI的診斷可信度評估、金融AI的風(fēng)險控制驗證、自動駕駛的安全性檢查、代碼生成AI的安全驗證等關(guān)鍵領(lǐng)域。它為這些高風(fēng)險AI應(yīng)用提供了數(shù)學(xué)級別的安全保證，而不是基于經(jīng)驗的模糊判斷。