正確程式碼與已驗證程式之間的鴻溝

LLM能寫出可以編譯甚至通過cargo test的Rust程式碼。但牠們目前還無法可靠地寫出形式化證明，來證實程式碼對所有可能的輸入都是正確的。

問題不在Rust語法。形式化驗證要求你明確陳述要證明什麼，找到能讓證明成立的不變量，並用驗證器接受的語言來表達這兩者。LLM訓練的是原始碼，而不是證明行為本身。牠們見過定理，卻很少見過成功證明之前那二十次失敗的嘗試。

如果你把遞迴二分搜尋貼給GPT-4，讓牠「證明這段程式碼正確」，你會得到一份看起來像證明的東西。牠會提到迴圈不變量和前置條件。但牠也很可能混用Dafny語法、引用不存在的引理、斷言弱到不足以導出後置條件的不變量。在你嘗試驗證之前，牠看起來完全正確。

Rust形式化驗證實際長什麼樣

Rust有多種驗證工具。Kani是一個模型檢查器，牠會窮盡探索函式在某一界限內的所有可能狀態。Prusti和Creusot是演繹驗證器，牠們將Rust轉換為邏輯表示式，再讓SMT求解器來證明性質。每種工具都要求使用特定語法的註解。

下面是一個簡單函式，以及Creusot中真實演繹證明的樣子：

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusot驗證前置條件a.len() > 0能保證後置條件result == a[0]。這很平凡，因為邏輯很簡單。現在加大難度：

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

不變量才是難點。人通過思考每次迭代中什麼保持為真來寫出不變量。LLM可能因為訓練資料中有這個模式就猜測s == i * (i - 1) / 2，也可能乾脆省略不變量讓求解器失敗。

當你讓LLM寫證明時會發生什麼

我用多個模型測試過這一點。提示詞是：「用Creusot寫一個經過驗證的Rust函式，計算n的階乘，包含完整的前置條件、後置條件和迴圈不變量。」

回答分成了三類。

第一類，有些模型輸出了看起來像樣但語法錯誤的註解。牠們把#[requires(...)]寫成了#[precondition(...)]，或者把Prusti語法和Creusot語法混用。程式碼連解析都過不了。

第二類，有些模型輸出了語法正確但不變量太弱的註解。階乘函式需要類似res == fact(i)的不變量。模型經常寫成res >= i，這雖然為真，但對證明後置條件毫無幫助。Creusot會報告無法建立目標，而LLM沒有機制來修復牠。

第三類，少數回答猜對了不變量，但幻覺出了一個輔助引理。牠們引用了Creusot標準函式庫中並不存在的math::fact函式。這個邏輯定義必須你自己建構，證明才能成立。

沒有一個模型能在第一次嘗試就輸出能通過驗證的證明。

LLM在驗證工作流程中真正有用的地方

這並不意味著LLM對形式化驗證毫無用處。牠意味著你必須把牠們用在正確的任務上。

牠們擅長生成樣板程式碼。給定一個函式簽章，LLM通常能生成捕獲明顯契約的#[requires]和#[ensures]子句。對於函式fn divide(a: i32, b: i32) -> i32，牠會正確建議#[requires(b != 0)]和#[ensures(result * b == a)]。這些不算深刻洞見，但能省不少按鍵。

牠們解釋驗證器錯誤的能力也還可以。如果Creusot報告「cannot prove loop invariant」，把錯誤資訊貼給LLM，往往能得到關於這個不變量應該做什麼的有用解釋。牠不會給出你需要的精確不變量，但能縮小搜尋範圍。

牠們對翻譯驗證語言也有幫助。如果你有一個Dafny證明想移植到Prusti，LLM可以處理大部分語法對應。底層邏輯是一樣的。這正是LLM擅長的模式匹配任務。

根本限制：證明是搜尋，不是補全

寫證明和寫Web伺服器不一樣。寫Web伺服器時，正確答案有很多個。寫證明時，正確答案只有一個，或只有一小族，其餘全錯。

LLM是下一個詞預測器。牠們根據上下文生成最可能的後續。證明步驟不是最可能的後續。牠是關閉證明義務的那一步，可能是第二個或第二千個最可能的選項。

想想證明排序函式返回輸入的排列。關鍵洞見通常是定義多重集或統計出現次數。LLM可能建議比較長度，這有必要但不充分。需要人來認識到長度相等不意味著排列，並引入計數不變量。

用Kani做模型檢查可以避開部分問題，因為牠不需要不變量。LLM能更可靠地生成kani::proof測試架，因為牠們看起來像單元測試。但Kani只適用於有界驗證。如果你需要無界證明，仍然離不開人。

一個能同時利用兩者的實用工作流程

如果你想在今天驗證Rust，這裡有一個確實有效的工作流程。

先正常寫程式碼。執行cargo test。然後新增契約。用LLM從函式簽章生成#[requires]和#[ensures]子句。仔細審查。模型會把簡單的做對，把難的微妙地做錯。

執行驗證器。牠至少會在一個迴圈上失敗。拿到錯誤訊息後讓LLM解釋缺少哪個不變量。把牠的解釋當作起點，而不是答案。自己寫不變量。

迭代。驗證器會告訴你不變量夠不夠強。LLM不會。把模型當作一個懂語法但從未完成過證明的結對程式設計夥伴。

對這個問題的誠實回答

LLM能為Rust寫形式化證明嗎？不能。還不能。沒有懂邏輯的人在場就不行。

牠們能搭鷹架、解釋錯誤、在工具之間翻譯。但找到讓證明成立的不變量、引理或歸納假設，仍然是人的能力。

如果你在找一種工具，讓你跳過學習分離邏輯或霍爾三元組，LLM不是。如果你在找一種工具，透過替你處理語法和樣板程式碼來讓學習曲線更平緩，讓你專注於邏輯，LLM值得一試。

如果你想做不需要不變量的有界檢查，從Kani開始。當你需要無界證明時，轉向Creusot或Prusti。用LLM來把語法寫對，但證明得自己寫。

常見問題

Rust中的形式化驗證是什麼？

形式化驗證使用數理邏輯來證明程式對所有可能的輸入都滿足規約。在Rust中，Kani、Prusti和Creusot等工具為函式新增註解，描述前置條件、後置條件和不變量。然後由驗證器檢查這些性質是否成立。

ChatGPT能為Kani寫證明嗎？

ChatGPT能寫Kani證明測試架，牠們看起來像帶有#[kani::proof]屬性的單元測試。這些測試架比演繹證明更容易生成，因為牠們不需要迴圈不變量。但包含假設和斷言的複雜測試架仍然需要人工審查。

Kani和Creusot有什麼區別？

Kani是一個有界模型檢查器。牠在一定界限內探索所有可能的執行路徑，檢查panic或斷言失敗。Creusot是一個演繹驗證器。牠將Rust轉換為邏輯公式，用SMT求解器證明對所有輸入都成立的性質，包括無界迴圈，但需要使用者提供不變量。

為什麼LLM在迴圈不變量上表現不佳？

迴圈不變量需要推理每次迭代中什麼保持為真，這是一種歸納推理。LLM訓練的是預測可能的文字延續，而不是搜尋能關閉證明義務的精確邏輯陳述。正確的不變量往往不是最可能的下一個詞。