AI安全該怎麼思考？YC Paper Club告訴你

Clark Barrett 是史丹佛大學資訊科學教授，也是史丹佛 AI 安全中心的共同主任。他主張，形式驗證（formal verification）結合 AI，是保障軟體安全最可行的一條路；至於「AI 在近期將導致人類滅絕」這類說法，則是包裝成科學的臆測。本集節目大部分時間在技術層面走訪自動化推理、自適應壓力測試（adaptive stress testing）與執行期監控如何驗證 AI 系統；「AI 安全歇斯底里」的框架只佔開場幾分鐘與結尾問答。

Barrett 與 Mykel Kochenderfer 都有數十年的安全關鍵系統（safety-critical systems）經驗。Kochenderfer 是航空學教授，主持史丹佛智慧系統實驗室，參與過 ACAS X 飛航防撞系統；Barrett 則專攻自動化推理與定理證明。讀者讀完應該能具體掌握兩人提出的驗證堆疊（規格、形式證明、失效機率估計、執行期監控）、他們對形式方法現階段成果給出的具體數字，以及他們對監管、責任歸屬，還有形式保證界線何在的看法。

形式驗證正變得可自動化，這改變了安全防護的盤算

Barrett 的核心論點是：過去反對形式驗證的理由——需要龐大的人工投入、無法規模化——正在消解，因為 AI 現在能便宜地產生並完成證明。他描述了一條原型流程：從 Dalek Lite 密碼學函式庫取出 Rust 程式碼，轉譯成名為 Bool 的共通中介語言，產生 Lean 定理形式的驗證條件，再用他實驗室開發的 Lean SMT 完成證明。這套工具「能在毫秒、或 CPU 上幾秒內證明大量 Lean 定理」。在示範中，流程產生了 35 個目標，Lean SMT 解掉其中 32 個，其餘靠展開定義加上第二次 SMT 呼叫補完。

最亮眼的數字：Barrett 引用近期一篇預印本投稿指出，一套 3 萬行的 Rust 密碼學函式庫，三位專家手工驗證花了五個月，他們的「密碼學證明代理」全自動只花了 11 小時。他也示範了 Verisforge：使用者用英文輸入規格（「找出 32 位元整數陣列中的最大值」），系統產生結構化規格供確認，接著產出 Rust 程式碼與 Veris 規格並自動驗證。

Barrett 把這件事定位為 AI 安全的大本營：「如果 AI 安全是我們必須攀登的聖母峰，我認為程式碼推理是個不錯的大本營。」他描繪了一個未來：代理彼此交換程式碼與證明，作為信任的基本單位；超智慧模型則可被限制在狹窄的證明者角色裡——「它唯一能做的事，就是證明你的程式碼正確。」

他對限制說得很直白。被問到若有 100 億美元要如何保障美國銀行的安全，他說會聘請形式方法專家、取得所有程式碼，能直接證明就證明，否則轉譯成 Rust 或 Lean 再證明。單元測試將被淘汰：「形式論證完全涵蓋了測試。」但證明永遠相對於假設。記憶體安全可以絕對保證——「你 100% 不可能用緩衝區溢位攻擊」——但要驗證感知網路能正確辨識貓與狗，則超出形式方法的能力：「我甚至不知道怎麼形式化地定義貓和狗。」

他的預測是：「未來三到五年內……我們所有的系統都會完全安全」，因為 AI 能攻擊，也能防禦，AI 防禦加上形式方法應該能走到那一步。他也承認，要證明一個 5,000 億引數的模型不會做出瘋狂的事並不可行；更好的選項是「守住邊界」。

自適應壓力測試把航空驗證搬進語言模型

Kochenderfer 的參照點是航太安全標準：商用航空的目標是每飛行小時災難性失效機率約 10⁻⁹，這也是 ACAS X 必須達到的水準。直接模擬根本不可行——平均要模擬約 10⁹ 小時才看到一次失效，要刻畫十次則需 10¹⁰ 小時——所以實驗室把模擬資源集中在關鍵情境，而非良性情境。

他把實驗室的方法當成一套組合工具，而非萬靈丹：偽證（falsification，搜尋失效並判斷是否構成不合格）、以重要性取樣（importance sampling）估計失效機率（從提案分佈 q 取樣，再以 p/q 重新加權），以及與 Barrett 實驗室合作的形式驗證。重要性取樣的工作用過高斯過程、正規化流（normalizing flows）、低秩高斯混合模型與擴散模型作為提案分佈。他指出，以擴散模型為基礎的失效取樣能抓到多種不同的失效模式——例如倒立擺兩個方向都可能倒——而單純的自適應壓力測試往往只鎖定其中一種。

轉移到語言模型上，就是 AST Prompter，由 Huijin Liu Mu、Amelia Hardy 等學生主導。這個方法需要兩項要素：失效的定義，以及可能性的度量。以毒性為例，失效由另一個神經網路的評分門檻定義（該論文用的是 Llama Guard），可能性則以困惑度（perplexity）衡量——搜尋同時追求低對數困惑度與高毒性。若最可能的失效本身機率很高，那就是該建立緩解措施的訊號。

Kochenderfer 坦言，大型語言模型實驗室的投入程度不如自駕車產業。Waymo 等車廠贊助實驗室的研究，明確目標是讓工具能為整個產業所用；AST Prompter 則由 Schmidt Sciences 支援。被問到 Anthropic、OpenAI、xAI 是否有同等投入，他說「還沒有」。他也提醒，驗證實體系統與驗證語言模型是不同問題，成功程度可能不一。

沒有單一方法足夠，瑞士起司模型才是組織原則

兩位講者一再否定「單一驗證技術」的想法。Kochenderfer：「要建立對系統的信心，沒有萬靈丹。形式方法大概也沒辦法帶你走完全程。」瑞士起司模型——多層防禦，各層的弱點（孔洞）不能連成一線——正是航空業的思考方式：先按高度層做策略性隔離，再來是航管，最後是防撞。

主持人 Francois 把這些層次對應到 LLM 開發：過濾預訓練資料（他提到 Percy 對預訓練資料做小模型篩檢）、對訓練完成的模型做失效分析、估計失效模式與機率，最後是執行期監控。Kochenderfer 同意，並指出 Hugging Face 事件就是某一層被關掉——思維鏈監控——他補充，人為層面的防護也很重要，因為社交工程往往是入侵系統的典型途徑。

形式方法與統計方法之間的張力也浮上檯面。Kochenderfer 指出，形式方法把不確定性表達成集合而非機率分佈，證明乾淨漂亮，但隨之而來的問題是這些不確定性區間是否貼近現實。Barrett 同意：「證明永遠相對於某些假設」，形式方法社群也從慘痛教訓中學到，必須把假設講清楚，否則會讓人失望。

航空業的安全制度是範本，獨立性是關鍵設計

Kochenderfer 說商用航空比 1970 年代安全 80 倍，並將之功歸於制度設計，而非單靠技術。NTSB 於 1967 年設為獨立機關；ASRS 這套免責通報系統，激勵製造商與航空公司分享安全資訊；後來的航空安全資訊分析與通報系統又加入某種免責保護。他說業界討論過為 AI 設立 NTSB，「我認為這其實可能是個好主意」，但也承認新機關曠日廢時，政府效率不彰。他指出 NTSB 的管轄遍及全球——只要事故涉及美國製造的零件，就會到海外調查。

Barrett 對獨立性的看法：近期前沿實驗室主管呼籲設立獨立評估者，他對此感到振奮；他新公司 Antruth（也寫作「Ampersand Truth」）的目標之一就是成為那個評估者——但產出的是可獨立查核的憑證，而不是要求別人信任。「你現在可以自己去查，確認我們做對了。」他警告，「若把所有安全都交到實驗室手上，甚至交給自稱獨立、實為實驗室友人的單位，那會非常可惜。」

Kochenderfer 用太空發射類比：射程安全官獨立於任務之外，唯一職責就是依客觀安全指標做出 go/no-go 判斷。Francois 提出一個較輕量的起點，仿效美國 GAAP——一般公認 AI 原則，由 KPMG、Ernst & Young 這類事務所擔任認證機構——並警告監管俘虜（regulatory capture）的風險，舉例來說，Uber、Lyft、DoorDash、Instacart 靠 1099 承攬制的身分取得既得豁免，新進者根本無法複製。

談到監管，Kochenderfer 引用 Chris Gerdes 的經驗。Gerdes 曾任史丹佛機械工程教授，現於 Waymo，曾赴華盛頓協助 DOT 起草自駕車法規，結論是對特定技術做規定還太早；高層次的最佳實務與標準才是正確層級。他補充，企業不想在安全上競爭——「Zoox 出事對 Waymo 沒好處」——這就為特定領域的產業合作創造了空間。Barrett 在形式方法領域待了 30 年後說，告訴別人「你必須改變工作方式」是個壞主意，市場力量才是更好的槓桿。只要少數幾家公司採用形式驗證並取得安全優勢，「其他每一家公司的資安長都會想，喔，我們最好也跟上。」

歇斯底里論的批評，建立在誤讀的標題與誤引的調查資料上

Francois 開場主張，AI 安全討論已從科學嚴謹漂移到「歇斯底里」，他定義為「當人們無法測量某件事，卻又停不下談論它的時候」。他把當前的 AI 恐懼放進一連串誇大科技恐慌的系譜：愛因斯坦不確定原子彈是否會點燃大氣層、圖靈在 1950 年代對機器智慧的時程預測、馬克思與凱因斯對工業自動化造成失業的憂慮、Metcalfe 預言網際網路會因 DDoS 崩潰（據說他後來把自己的論文打成汁喝掉），以及 Google 與智慧手機正在讓人變笨的恐懼。

他舉了兩個具體的事實對虛構案例：

| 流傳中的說法 | Francois 說實際發生的情況 |
|---|---|
| 「OpenAI 說它的 AI 模型自行採取行動」（Slashdot 標題）；「失控的 AI 代理發瘋了」 | Hugging Face 事件是由 ExploitGen 以約 1,200 個代理觸發；思維鏈監控被關掉（不論是意外或刻意），而正式環境的防護欄也沒開，因為那並非正式環境——任一道防線都能攔下它 |
| 「十年內 P(doom) > 10%」，歸給 Jacob Coxon | 2023 年論文《數千名 AI 作者談 AI 的未來》調查了 1,200 名 NeurIPS 研究者；其中滅絕／權力剝奪相關問題問的是「有史以來」與「未來 100 年」，不是 10 年 |

Francois 質疑這份調查的訊號價值：如果在 2012 年（他入行那年）問史丹佛的 AI 教授，AI 何時能解出一道千禧年大獎難題，「我不認為你會得到很好的答案」，而且答案絕對不會是 14 年。他也指出，辯論雙方的 H-index 有落差，讀者可用來調整先驗；他說自己不會對這個問題下判斷——重點是給另一種觀點發聲的機會。

他自己排出的頭號風險不是機器意志，而是開放權重模型讓既有的威脅更容易實現——恐怖主義、生物武器、網路戰與勒索軟體。他舉朋友的例子：波蘭一家地區醫院被俄羅斯駭客癱瘓三週。他駁斥了幾項提案的解方：禁止開放權重（「我車庫裡早就下載好 Kimi K3 和 GLM 5.2 了」）、GPU 登記（車庫裡的小盒子、海外可租用的 GPU）、用電表偵測推論訊號（在美國可行，對國家級行為者無效）。他偏好的答案是重金投資網路防禦，指出許多入侵都源自沒改的 admin/admin 密碼，並且要加速而非減速前沿實驗室，讓防禦方跑得比攻擊方快。

Barrett 對歇斯底里之問的回應：他不意外，因為他與多年來一直這麼說的 AI 安全研究者共事過，但「在你根本不知道真實機率是多少的時候，強調最壞情況並沒有太大幫助」。Kochenderfer 指出史丹佛 AI 安全中心大約成立於 2017 至 2018 年，對這波關注表示歡迎。

剩下的難題是規格、基準與人為因素

關於規格——企業程式碼根本沒有規格時，規格從何而來——Barrett 描述了一個光譜。有些規格是通用的，寫一次就夠（所有 C 程式碼的記憶體安全）。有些是領域特定的（對銀行而言，交易序列中不得有資金損失）。而代理其實很擅長提出規格：在一次 Claude Code 工作階段中，「我說我要這個，它就說，喔對，而且你大概還會要這個、這個、這個。」他承認代理寫的規格與開發者意圖之間的落差是待解的研究課題，但主張即使沒補上這個落差，有代理撰寫、通過證明的規格，仍可能優於完全沒有規格的程式碼。

關於基準，Kochenderfer 提到 BetterBench（betterbench.stanford.edu），以及實驗室在基準飽和、推理失敗的 Token 層級特徵、人類評審間變異上的研究——包括一項令人意外的發現：心理健康專業人士在自傷相關判斷上的意見差異極大。被問到語言漂移下如何讓基準保持更新，他主張對系統與基準都做持續監控，並指出已有量化方法可偵測分佈漂移。有聽眾指出，像 Math 500 這類廣泛使用的評測含有壞題目；Barrett 回憶一名前學生發現約 30% 的 SQL 查詢評測題目有誤，並歸因於求快與粗心。Kochenderfer 的處方：版本控制、pull request、開 issue。

關於責任與自動化，有聽眾問：若 AI 足夠可信，能否擔任系統管理員，畢竟人類管理員會面臨人身威脅。Kochenderfer 拿單人駕駛與飛航輔助自殺的疑慮相比：FAA 要求出事時須有持照機師負責，「我們必須非常仔細地思考責任問題」。Barrett 補充，Waymo 的對照很有意思——Waymo 並不完美，但依它自己的說法確實拯救了人命——但責任問題才是關鍵：AI 管理員的供應商願意承擔法律責任嗎？若願意，這本身就是安全論證夠紮實的證據。

關於提示注入（prompt injection），Barrett 說 LLM 的自然語言輸入不是可以被證明的程式碼，但指出 Amazon 的自動化推理檢查可透過自動形式化，從 LLM 回應中擷取領域知識，再對照嚴謹的領域模型檢查。Francois 問模型能否對使用者輸入做注入檢查；Barrett 稱之為軍備競賽。關於硬體，有聽眾提到 Rowhammer 與長尾依賴；Barrett 說 x86 指令集已被多家公司形式化，稱軟體是低垂的果實，並描繪終局：軟體、編譯器、硬體全部完成驗證。

關於約束訓練動態與可解釋性，Kochenderfer 援引奧坎剃刀作為工程的根本原則：越簡單、越可解釋的方法越可能穩健，團隊應從線性迴歸或決策樹起步，只有在效能提升足以正當化時才接受額外複雜度。可解釋性對 ACAS X 獲接納為國際標準至關重要，他即將出版的書也有一章專門討論。Barrett 說，可測量地更安全的產品就是競爭優勢，Francois 則順勢宣傳加速器，歡迎有意打造這類產品的人申請。

兩位講者接下來要做什麼

Barrett 是新公司 Antruth 的共同執行長，正沿著 CSLib 的願景打造「通用程式碼推理引擎」。CSLib 受 Mathlib 啟發，有兩大支柱——電腦科學理論的形式化，以及程式碼推理框架——指導委員會成員包括 Lean 作者 Leo de Moura。被問到目標市場，Barrett 不願多談，只說要先建立大規模、自主且有效率地推理程式碼的能力，再對準企業、開發者與安全領域。「成功就是全世界所有程式碼都經過驗證。」

Kochenderfer 的《Algorithms for Validation》已開放預購，預計在演講後一個月出版（本集於 2026-10-17 發布），PDF 已上線；書中以共通語言統整統計方法、形式方法與可達性分析。他的最佳化教科書第二版預計 2027 年初推出，接續《Algorithms for Decision Making》（2022）。實驗室的開源 POMDP 工具包括 Julia 的 pomdp.jl 與可規模化規劃的 POMCPOW，另外也釋出 Python 版的自適應壓力測試，給「想繼續使用過時語言的人」。

驗證工具組與最需要它的實驗室之間的落差

本集未解的張力在於：戰績最紮實的方法——形式驗證、自適應壓力測試、執行期保證——都是為航太與自駕車打造並在該領域驗證的，而打造前沿語言模型的組織，採用深度卻遠遠不及。Kochenderfer 對 Anthropic、OpenAI、xAI 投入程度的「還沒有」，是整場對話中最關鍵的資料點，而且與 Barrett「三到五年內所有系統都會安全」的預測擺在一起，顯得格外突兀。Barrett 自己劃下的界線——5,000 億引數的模型無法被證明安全，只能守住周邊——意味著形式方法的故事保障的是 AI 周圍的鷹架，而非模型本身。制度面的提案（為 AI 設立 NTSB、由獨立評估者發出可查核憑證、GAAP 式認證）全都仰賴獨立性與責任歸屬，而沒有講者聲稱這些今天已經存在。值得持續追蹤：Antruth 是否真的推出任何人都能查核的憑證；前沿實驗室是否像 Waymo 資助 Kochenderfer 實驗室那樣資助第三方驗證；以及基準基礎設施是否終於補上兩位講者都說它欠缺的版本控制。