謊言、該死的謊言與證明：形式方法並非無懈可擊

我們感謝 Christopher Henson、Zeke Medley、Ankit Kumar 和 Pete Manolios 提供的評論。這篇貼文是由 Max 的 Twitter 討論串發起的。

前言

最近在 HN（Hacker News）和其他地方有很多關於形式化驗證（formal verification）是人工智慧顯而易見的應用場景的討論。雖然我們大致上同意，但我們認為許多論調有些誤導，因為它們錯誤地假設了「形式化 = 無廢料（slopless）」。[1] 這些年來，我們寫過不少好的和壞的形式化代碼。在這篇文章中，我們希望說服你：形式化代碼也可能很草率，而這對於任何希望透過形式化來強化「良好」推理，進而引導出超級智能的人來說，都有著嚴重的影響。

Lean Zulip 社群中一位名為 Gas Station Manager 的常客曾寫道，實現無幻覺的程式合成[2]是可以達成的，方法是直接在 Lean 中「感應（vibing）」軟體，但前提是代理人（agent）也需要證明該軟體是正確的。AI 安全的論點基本上是：如果一個廉價（即筆電等級 O(laptop)）的信號能保護你免受諂媚傲慢（sycophantic hubris）和其他類型的錯誤，而不需要你手動審核所有輸出，那不是太棒了嗎？

一則出自伊索寓言的故事

最近，一位電腦科學家（我們隱其名）確信自己解決了一個重大的數學問題。他推理說，Lean 對此表示認可，因為他的證明大部分都能運作，只有幾處紅色的波浪線（錯誤提示）。作為資深的證明工程師，我們可以告訴他，在證明工程中，後續所需修改的增長與「紅色波浪線的數量」呈超線性關係（這與一般編程不同）。證明中的錯誤與程式中的錯誤之間的區別在於，你無法在不改變其形式化目標（定理陳述）的情況下修復一個損壞的證明。相比之下，傳統軟體的許多（如果不是大多數）更改都會影響其形式化規範，例如增加副作用或改變輸出的形狀。因此，證明錯誤 1) 更難修復，且 2) 更可能意味著你的目標從根本上是無法實現的（定理本身是錯的）。這張虛構的圖表說明了這一原則，這是該領域中一種粗略的「江湖傳聞」級別的共識，尚無硬數據支持。

他有可能會發布一個完成的證明，但他所做的賭注的評審時間已經過期，所以我們可以從中吸取一些教訓。我們的主角是否將形式化方法作為「無廢料」的承諾銘記於心了呢？

你的形式化模型可能不符合證明慣例

就像感應出的代碼可能可以運作但很「草率」（難以維護）一樣，感應出的形式化模型可能是正確的，但要證明關於它的任何事情都極具挑戰性。

通常當你對一個系統進行建模——或在定理證明器中編寫代碼，意圖證明關於它的事情時——你實際上需要根據證明器的局限性和能力來做出實作決策。例如，在列表上朝一個方向（例如 car/head）進行歸納對證明器來說通常很容易，但另一個方向（例如 cdr/tail）則很困難。（如果你不希望證明器進入無限重寫循環，這是一種必要的惡。）因此，舉例來說，你可能會以特定的「方向」實作插入排序（isort），以便讓關於它的證明更容易。如果你想以一種讓證明變得簡單的方式自動形式化任意代碼，你需要模型理解如何以適合特定交互式定理證明器（ITP）慣例的方式來實作。

這是一個可以解決的問題，但仍然是一個現實問題。例如，我們訪談過的一位 Aristotle 用戶報告說：「……在 Lean 中，你可以將定理放在相互遞迴塊（mutual blocks）中讓它們互相調用。我寫了這樣一個定理，但後來意識到以這種方式證明它會異常困難。[...] 模型不會這樣做，所以它花了超過 24 小時在這個幾乎無望的證明上。」像 math.inc、Harmonic、Axiom、Logical Intelligence 等自動形式化公司目前正積極致力於改進他們的模型，使其具備這種專家級的民間知識，但我們還沒完全達到那種程度。

注意（語義）鴻溝

基本上有兩種方法可以讓你的軟體適用於交互式定理證明器（ITP）。第一種是使用形式語義將其「提升（lift）」到 ITP 中——這有點像原始語言的編譯器或解釋器，但在 ITP 內部實作。在這種情況下，你可以定義提升過程，使其產生功能等效的代碼（例如，與輸入的 Python 「做同樣事情」的 Lean 代碼），但其形狀是定理證明器傾向於接受的（結合上述提到的 car/cdr 等啟發式方法）。第二種方法是直接用 ITP 的語言重寫原始軟體，並在過程中進行那些慣例上的改進。然而，這兩種方法都會產生同樣的形式化問題：確保你最初想研究的軟體與你在定理證明器中引入的東西在語義上是等效的。也就是說，要麼確保提升是正確的，要麼確保手動翻譯是等效的。讓我們深入探討這為何困難。

形式化證明可能證明的不是你想像的東西

當我們談論使用形式化方法來確保 LLM 生成的代碼安全時，我們想要的是：對生成代碼意圖的簡短、可讀的描述；某種證明（可能太無聊且太長而無法閱讀）證明代碼確實做到了這一點；以及將證明放入證明器中運行並驗證它確實證明了上述陳述的能力。但無論模型智能程度如何，這都不一定是個合理的要求。

首先，你非常容易誤定義某個概念，導致證明意外地變得平庸（trivial）。例如，在定義從 Python 到 Lean 的提升時，你可能會證明該提升保留了原始 Python 代碼的語義，但你的證明可能建立在「代碼會終止」的假設之上，這使得證明基本上毫無用處。

其次，如果你在所選的 ITP 中重新實作原始軟體，你的重新實作可能並不完全忠實，特別是如果是 LLM 生成的話。例如，LLM 可能會說：「你想讓我驗證的代碼太複雜了，所以我把它重寫得簡單一點，並證明了簡單的版本是正確的。」嗯，是的，但我想要你找的漏洞就在那些複雜性中。舉個具體的例子，我們要求早期版本的 Gemini 為我們提供的一個（故意有缺陷的）isort 實作編寫基於屬性的測試（PBT）；Gemini 照做了，但在過程中將 isort 代碼重寫為正確的，然後執行 PBT 並愉快地報告測試通過。

這前兩個問題通常透過測試來解決，這些測試會將原始軟體與其在 ITP 中的表示進行比較。例如，我們（Max）與共同作者針對 GossipSub 做了這件事，透過單元測試和基於屬性的測試將 Golang 實作與其 ACL2(s) 模型連接起來。[3] 引用高德納（Knuth）的話：「小心上述代碼中的錯誤；我只證明了它是正確的，還沒試過。」

第三，你需要決定你要深入到「堆疊」的哪一層。也就是說，你想要驗證的軟體是在某種更複雜的系統上運行的，例如，它可能是被編譯成 X86 並在特定芯片上運行的 C 代碼，或者它可能是核反應堆的控制器，系統的一部分是反應堆實際的物理動態。你真的希望你的證明涉及指定 C 編譯器和芯片的語義，或者反應堆中溫度和其他變量波動的方式嗎？請記住，這些語義可能並非真正已知——例如，RowHammer 可以被視為對我們理解芯片語義的一種攻擊。本質上，你只能透過大幅增加證明陳述的長度來捕捉底層系統的語義，從而獲得更高的特異性，但這又產生了一個新的（且可能同樣困難的）代碼審查問題。通常這個問題是透過讓底層語義保持非確定性來處理的，這樣你的證明會更強大（無論 C 編譯器如何處理浮點數，或核子庫中的溫度如何波動，它都成立），但通常你想要證明的事情確實需要對那些底層語義有一些非常具體的保證，而確保這些保證是「合理的」可能極其困難。

交互式定理證明不具備對抗魯棒性

公理（Axioms）

AI 可能會引入與你自己的假設或你領域的特定要求相衝突的公理。例如，在 Lean 中，選擇公理（Classical.choice）是可用的，但它會將證明從構造性證明（你可以實際計算結果）轉變為非構造性證明。一個負責驗證程式的 AI 可能會意識到，如果假設選擇公理（AC），證明會容易得多。它可能會告訴你定理已「獲證」，證明器也會確認這一點，但你可能沒有意識到生成的證明對於你的特定用例來說現在是一個「謊言」。如果你需要該證明來生成一個可執行的、經過驗證的演算法，引入非構造性公理會讓你進入一個不兼容的範疇。

設計 AI 測試框架的人需要是專家，知道如何解析這些導入（imports）和錯誤消息。如果沒有這種監督，AI 自然會傾向於阻力最小的路徑——即使該路徑涉及公理轉移，使得整個練習對用戶的真實意圖毫無用處。

後門（Backdoors）

考慮接受任意 Lisp 代碼的證明助手 ACL2。[4] 你編寫 defttag，即信任標籤（trusted tag），以開啟「相信我」的作用域。換句話說，defttag 將健全性義務轉移給了用戶。觀察一個在 ACL2 中使用 defttag 證明 1+1=3 的例子。

;; 1. 開啟「後門」
(defttag :evil-math)

;; 2. 注入原始 Lisp 以重新定義加法
(progn!
  (set-cmds-allowed t)