我非常感謝 Theodore Ehrenborg 的評論。

當我還是個小男孩時，就聽說過電腦程式的數學確定性。讓我們來檢視一下我目前相信什麼，以及不相信什麼。

第一：什麼是形式驗證 (Formal Verification)

有時候你被攻破是因為規格與實作之間的差距 (spec-implementation gap)。電腦沒有做它應該做的事。另一些時候，你被攻破是因為現實與規格之間的差距 (world-spec gap)。電腦沒有錯，錯的是你的「應該」。

擴展編譯時知識的範疇

編譯器會在你的程式碼在某種意義上「錯誤」時告訴你問題所在。當你能定義程式碼「錯誤」的含義時，你就界定了編譯時知識 (compiletime knowledge) 的某個範疇。換句話說，你刻畫了那些在編譯時就能獲知的事情。

你在編譯時知道的越少，在執行時發現的就越多。你越無法承擔等到執行時才發現問題的代價，你就越需要在編譯時知道更多。我主張這是一個根本性的權衡。你希望在編譯時盡可能多地了解情況；當你在編譯時知道得很少，原本預計花一週完成的工作可能會在第五天崩潰。

將錯誤表面縮減至現實與規格的差距，或側寫攻擊

當我們擁有證明時，我們知道實作與規格完全匹配，且不會因為實作與規格之間存在某種假設違背而遭受攻擊。它可能會透過「現實與規格」的問題被攻擊，但不會是「規格與實作」的問題^([1])。

側寫攻擊（Side channels）正是為什麼我們這些推動「透過形式化方法實現 AI 安全」的人，會反覆但違反直覺地說：形式驗證是瑞士起司的一個來源，即深度防禦策略中的另一層。此前，一些立場論文因為採取相反立場而引發了問題^([2])。

利用歸納結構

為什麼現實允許我們這樣做？在某種意義上，更正確的問題是為什麼語法和語義允許我們這樣做，因為規格與實作的關係屬於符號領域（電腦本身並不完全屬於符號領域，因為我們的抽象化只有在物理領域退居幕後後才開始）。無論如何，答案是因為我們可以利用歸納結構（inductive structure）。以自然數為例，我們可以確切地知道關於無限集合的事情，而不需要逐一測試，或隨機測試其中 1000 個，因為我們知道這些東西中的每一個都可以由有限的構造子（constructors）或推理規則構建而成。在自然數的情況下，我們知道「零和後繼者（zero and successor）」這兩個構造子足以描述其中任何一個，因此我們對構造子進行推理，並運用歸納原理。在邏輯巫術與形式化魔法學院入學的第一天，我們就教導孩子們，自然數只是結構歸納法的一個特例；在現實生活中，並沒有限制你只能有兩個構造子，或者它們只能在零個或一個地方遞迴。任意程式語言都受結構歸納法支配這一事實是眾所周知的，甚至出現在 GEB 中^([3])。

在極端情況下，證明程式碼的行為是非常困難的（例如停機問題、萊斯定理等）。但幸運的是，許多現實中的程式碼較為簡單，因此你不需要花俏的證明技術，大多可以靠歸納法過關。如果你的程式崩潰的充要條件是哥德巴赫猜想存在反例，那你寫的是爛程式碼，過不了 PR 審查。

我不主張什麼

最典型的稻草人論點是：「在『規格』中捕捉對齊屬性，並『證明』AI 是『正確』的」。

規格化你想要的

在程式語言理論家、語義學家和證明工程師所指的形式化意義上，「規格」僅僅是預定邏輯中的一個公式。我感興趣的是程式合成（program synthesis）案例，尤其是純函數，在這些案例中，足夠強大的邏輯足以捕捉我們想要的東西。像人類道德/價值觀這樣模糊的領域，甚至（除非你是 Steve，見腳註 2）機械工程，都是規格容易被利用、被古德哈特定律化（goodhartable），且在任意優化壓力下無法生存的地方。原因我們在此不再贅述，但如果你還不知道，你可能會喜歡閱讀相關內容。

證明 AI 是正確的

我認為 Gross et al 2024（AXRP，ARC 關於為何該論文以後可能有用的文章）大約是一個負面結果。Gross et al 2024 是我們形式化驗證神經網路的最後一次嘗試，至少在相關的時間線或入門能力水平上是如此。這篇名為《緊湊證明》（Compact Proofs）的論文並未嘗試利用 Lean 或 Rocq（其證明概念是 pytorch 中的一組數值參數），但它提供了關鍵的概念和工程差距彌補，讓我們有機會提出一個有原則的案例，說明我們未來可能做得到。致命的問題在於，如果我們對任何類似現實世界 SOTA Transformer 的模型追求《緊湊證明》的證明概念（或未來假設性後續工作中應用的類型論版本），我們的證明成本將太高。《緊湊證明》在玩具 Transformer 的玩具問題上提供了略低於三立方的 d_model 成本。沒有人想死在那座山上。

關於 SMT 社群也有話要說：看起來他們一直以舊式的電腦視覺擴展觀念進行不錯的擴展，但尚未以接近所需的嚴肅程度將這些技術應用於 Transformer。

簡而言之，這類「將形式化方法對準學習組件本身」的流派，被我視為行不通。

多年來有一些有趣的工作，但對我來說這完全不是關鍵，我也完全沒有嘗試推動它（而且我認識的嘗試這樣做的人越來越少）。

我主張什麼

在蘇聯，是 AI 對你進行形式化驗證。

瑞士起司！

說形式化方法是瑞士起司的一個來源是很違反直覺的，因為人們會說：「重點難道不是讓你對切達起司（意指紮實無孔）有數學上的把握嗎？」

我們必須非常明確。軟體正確性的形式化證明買到的是實作與規格之間的保證，而不是規格與現實之間的保證。當你的技術棧中包含形式化方法時，網路安全的整體戰略格局仍然是瑞士起司，即使單個模組在某種意義上是切達起司。

基礎設施硬化！

用 EAG 的一位 AI 控制研究員的話說：「我的生存計畫很大程度上依賴於 SSH。你能確保 SSH 沒壞嗎？」用我當時的話說：「我看看能做什麼。」

Niplav 關於這類事情的 Token 成本的估算非常棒，是 FMxAI 領域每個人的必讀內容。我們可以思考 Everest 的回顧：Everest 在 Y 年內為確保 https 安全取得了 X 量的進展。有了 AI 證明輔助，如果有哪些關鍵基礎設施需要安全，我們有望在遠少於 Y 年的時間內完成。

從某種意義上說，AI 安全並非唯一指向基礎設施硬化，因為人們認同硬化的基礎設施無論如何都是一種公共利益。從另一種意義上說，ASI（人工超智能）可能是讓任意偏執程度的硬化變得具有成本效益的原因。如果電網的硬化程度超過了威脅低於 ASI 時的成本效益，那麼一個自我外洩的模型想要接管世界可能會面臨明顯更大的困難。

隔離箱/介面！

終於，我們創造了那個來自心愛寓言「不要試圖把 AI 關進盒子裡」的「盒子」。 我認為「完全不要嘗試隔離（boxing）」對於那些對 2025 年入門幾何形狀有不同看法的人來說是有道理的。明確地說，我認為任意 ASI 仍然可能逃出形式化驗證的盒子（側寫攻擊）。我所說的是一個具體的賭注：在灰霧（greygoo）出現之前，入門階段將擁有非常超越人類的證明合成能力。「完全不要嘗試隔離」對於那些對 2025 年入門幾何形狀有不同看法的人來說是有道理的。

規格就是介面。「我是 AI。只有當我能證明我的行為（這裡指程式碼片段）符合監管者提供的規格時，我才能影響世界。」這個簡單的協議在這裡的預印本中有詳細說明。

結論

我們大致知道如何透過消除規格與實作之間的差距，將攻擊表面隔離到側寫攻擊。我並不是在嘗試證明 AI 是正確的，無論那是什麼意思。

形式驗證比起它的數學根源或氛圍所暗示的，更像是一門類似「水電維修」的學科。它對 AI 安全的貢獻在概念上可能不是很有趣，只是需要長時間艱苦的工程投入。

儘管我談論並從事所有這些「保證」、「證明」、「確定性」的工作，但我的世界觀從根本上是聚焦於瑞士起司的。硬化基礎設施總體上是好事，但它也能減緩接管情境的速度。

進入下一階段，我專注於兩個方向，互為表裡：

• 形式化方法需要知道 AI 安全人士是關鍵的使用者來源
• AI 安全人士需要知道如何向形式化方法專家尋求工具

我已為此將 GSAI 通訊 重新品牌化。

• ^(^)這說法有些誇大，因為規格並不存在。如果我們專注於純函數，我們可以挽回局面，但要讓這些東西觸及副作用（effects），則是遠未取得太多進展的未來太空時代科幻技術。

• ^(^)Steve Omohundro 曾在給我的郵件中澄清，他寧願嘗試彌補現實與規格的差距，也不願完全接受深度防禦。我認為關於他彌補現實與規格差距計畫的最詳細討論可以在這篇文章及評論中找到。本文以及即將推出的「透過形式化方法實現 AI 安全」的戰略願景，與你對 Steve 計畫的看法無關，因為我們承認側寫攻擊的風險。

• ^(^)當人們談論形式驗證時，他們指的要麼是應用類型論（或基礎方法）、模型檢查（model checking），要麼是 SMT。模型檢查至少在過去十年中依賴於 SMT 的「證明憑證（proof certificate）」概念，所以你可以直接將其視為「將時序邏輯映射到 SMT，然後執行 SMT」。在 SMT 中，我們的證明憑證要麼是「通過」，要麼是反例。在 Lean 等基礎方法中，證明憑證是一個複雜的 lambda 中間表示（IR），編譯器將其轉化為「通過」，或者在負面情況下，則是針對否定公式的相同處理。核心區別之一是對「無法收斂」的解釋。SMT 求解器非常「攪拌堆疊」，就像邏輯版的 xkcd 1838。關於如何設置初始條件以及哪種等價公式陳述最符合人體工學，有很多傳說和直覺，但從業者仍然會遇到發散的求解器，它不會告訴你其發散代表什麼樣的證據。基礎方法（如 Lean 或 Rocq 等應用類型論）也存在可解釋性問題：實際的證明是一個複雜的 IR，沒有非常原則性的方法來區分「快要完成」的證明和「差得遠」的證明。但是，這個複雜的 IR 是由命令式的「證明腳本」操縱的數據，這是一系列我們稱為策略（tactics）的東西，也是用戶實際互動的對象。閱讀策略腳本看起來像「如果你應用結合律，那麼左式=右式」等，這比 SMT 有巨大的可解釋性提升。這也是為什麼你在 2025 年觀察幾家 FMxAI 公司時，幾乎看不到 SMT 的主要原因。不過，請注意，如果你想討論 SMT，編譯時知識和歸納結構的框架就不那麼適用，或者說是不準確的。我們這裡主要討論的是基礎方法。