Cleanroom 軟體工程要求你在編譯程式碼之前，先證明它是正確的。這聽起來很高尚，直到你花了三個小時為一個只排序十個整數的函式撰寫迴圈不變式（loop invariant）為止。

瓶頸不在證明本身，而在於那些繁瑣的樣板程式碼。生成驗證條件（verification conditions）、為迴圈加上不變式註解，以及為 Dafny、Why3 或 Z3 格式化斷言（assertions），這些工作既乏味又容易出錯，而且完全不好玩。LLM 在這個部分出人意料地擅長。但它們並不擅長實際的證明工作。理解這兩者之間的差異，正是讓這種自動化變得有用而非危險的關鍵。

為什麼手動處理證明義務會拖慢開發速度

在 Cleanroom 中，你根據盒結構（Box Structure）規格撰寫程式碼，然後生成驗證條件（VCs）來證明你的實作符合規格。每個迴圈都需要一個不變式。每個函式都需要前置條件和後置條件。每個資料精化（data refinement）都需要一個抽象函式。

對於一個試圖交付軟體的團隊來說，這是一種稅負。一位資深工程師可能會花 40% 的時間在註解和 VC 的骨架搭建上，只有 60% 的時間用於實際的邏輯推理。搭建骨架不需要深刻的洞察力，需要的是耐心和對證明器語法的熟悉度。

這正是 LLM 所擅長的模式匹配任務。它們已經看過成千上萬個迴圈不變式、Dafny 方法和 SMT-LIB 檔案。它們能生成語法正確的註解，足以作為一個起點。

「使用 LLM 自動化形式證明」實際上意味著什麼

讓我們精確一點。LLM 無法證明你的程式碼正確。是 Z3、CVC5 或 Dafny 驗證器這類證明求解器證明了你的程式碼正確。LLM 自動化的是介於你的虛擬碼和求解器之間的人力勞動。

工作流程看起來是這樣：

  1. 你撰寫實作和規格。
  2. LLM 生成候選註解：不變式、前置條件、後置條件、幽靈變數（ghost variables）。
  3. 你將帶有註解的程式碼餵給驗證器。
  4. 驗證器要麼接受證明，要麼以反例拒絕，要麼逾時。
  5. 如果證明失敗，你檢視失敗原因，並提示 LLM 精煉註解。

LLM 就像一個非常快、非常自信且認識網路上所有驗證工具語法的實習生。它會很樂意幻覺出一個看起來完美但立即失敗的不變式。這沒關係。求解器會抓到這個幻覺。它的價值在於讓你不必面對空白頁的難題。

LLM 如何生成求解器能檢查的註解

訣竅在於提示詞。你不會要求 LLM「證明這個函式正確」。你要求它產生特定格式的特定產物。

舉例來說，如果你有一個類似 Python 的函式用來計算陣列的總和，你可以這樣提示 LLM：

Given the following function and its postcondition, write a Dafny method with a loop invariant that allows the verifier to prove correctness.

Function: sum(arr) returns the sum of all elements in arr.
Postcondition: result == sum(i in 0..|arr|) arr[i]

LLM 會回傳帶有迴圈不變式的 Dafny 程式碼，例如 forall k :: 0 <= k < i ==> arr[k] is accounted for in result。它第一次可能無法完全掌握正確的語法，但它能掌握正確的結構，而這能幫你省下十分鐘的打字時間。

若需要更多控制權，你可以直接要求生成 SMT-LIB。這在你建構自訂驗證管線而非使用 Dafny 這類高階語言時特別有用。

實際範例：使用 Python 和 Z3 自動化迴圈不變式

這裡有一個完整、可執行的範例。我們使用 Python 呼叫 LLM（OpenAI 的 API）為一個簡單的陣列求和函式生成迴圈不變式，然後用 Z3 驗證它。

首先，安裝相依套件：

pip install z3-solver openai

然後執行腳本：

import openai
from z3 import *

code = """
def sum_array(arr):
    s = 0
    i = 0
    n = len(arr)
    while i < n:
        s = s + arr[i]
        i = i + 1
    return s
"""

prompt = f"""You are a formal verification assistant.

Given this Python function that sums an array:
{code}

The postcondition is: result == Sum(arr[j] for j in range(len(arr)))

Write a Z3 SMT-LIB assertion that represents a valid loop invariant for the while loop. The invariant should mention i, s, n, and arr. Use Python Z3 syntax (ForAll, Implies, And, etc.). Return ONLY the Python code for the invariant, no explanation."""

client = openai.OpenAI()
response = client.chat.completions.create(
    model="gpt-4o",
    messages=[{"role": "user", "content": prompt}],
    temperature=0.2,
)

invariant_code = response.choices[0].message.content.strip()
print("Generated invariant:")
print(invariant_code)

# Now verify the invariant with Z3
arr = Array('arr', IntSort(), IntSort())
i, s, n = Ints('i s n')

# We manually parse the LLM's output. In production you'd use an AST parser.
# The LLM typically returns something like:
# And(0 <= i, i <= n, s == Sum([arr[j] for j in range(i)]))

# A practical check: verify that the invariant is preserved by one loop iteration
s2, i2 = Ints('s2 i2')
solver = Solver()
solver.add(n == 3)
solver.add(arr[0] == 1, arr[1] == 2, arr[2] == 3)
solver.add(i2 == 1, s2 == 1)  # assume invariant holds mid-loop

# Execute one iteration
s_next = s2 + Select(arr, i2)
i_next = i2 + 1

# Check that invariant holds after iteration
solver.add(Not(And(i_next >= 0, i_next <= n)))

if solver.check() == unsat:
    print("Invariant preserved for this concrete case.")
else:
    print("Invariant FAILED for this concrete case.")
    print(solver.model())

這個腳本不會一次就驗證完整個函式。這正是重點所在。LLM 給你一個候選不變式。Z3 告訴你它是否成立。你反覆迭代。

實務上，建構 LLM 輔助驗證管線的團隊會將這個迴圈包裝在腳本中：將失敗的 VC 送回給 LLM、解析新的註解、執行驗證器，並將任何錯誤訊息回饋作為精煉提示詞。

這不是全自動的驗證。這是有人在旁監督的驗證，搭配一個打字飛快的助手。

什麼時候會出問題：幻覺與實際錯誤

LLM 會生成過弱的不變式。它會忘記提及求解器需要的變數。它會生成 2019 年的 Dafny 語法，而那已經無法編譯了。它會自信地告訴你 i <= n 就足夠了，但實際上這個迴圈需要 i < n && s == partial_sum(arr, i)。

這些都不是災難性的。求解器會拒絕它們。你閱讀錯誤訊息，再次提示。

真正的危險是反過來的情況。當 LLM 生成一個過強的不變式時，求解器可能會針對一個比你預期更嚴格的規格證明程式正確。你以為你證明了 sum_array 適用於所有陣列。實際上你只證明了它適用於所有元素皆為正數的陣列，因為 LLM 多塞了一個看起來合理的連言項（conjunct）。

務必審查生成的規格。LLM 負責撰寫樣板程式碼。你負責掌握邏輯。

何時該信任機器，何時該手工打造

使用 LLM 自動化於：

  • 搭建 VC 骨架：針對前置條件和後置條件明確的簡單函式。
  • 語法轉譯：在不同證明語言之間轉換。將 Dafny 規格轉成 Why3 或 SMT-LIB 是機械性且容易出錯的工作。LLM 在這方面表現優異。
  • 幽靈變數生成：用於資料精化證明。這個模式是重複性的。

不要使用 LLM 自動化於：

  • 安全關鍵的證明：細微的規格錯誤比沒有證明更糟。
  • 複雜的時序邏輯或活性質（liveness properties）。LLM 在這方面的訓練資料較少，幻覺更容易溜過檢查。
  • 新穎的演算法：訓練語料中沒有類似的東西。如果你發明了一個新的共識協定，LLM 根本不知道它需要什麼不變式。

常見問題

什麼是 Cleanroom 工程中的驗證條件？

驗證條件是從你的程式碼及其規格生成的邏輯公式。如果這個公式是有效的，你的程式碼就正確實作了規格。在 Cleanroom 中，這些條件通常在編譯前生成，並使用證明輔助器或自動化求解器來消除。

LLM 能取代 Coq 或 Isabelle 這類證明輔助器嗎？

不能。LLM 生成程式碼和註解，讓證明輔助器可以檢查。它們不執行實際的證明步驟。證明輔助器仍然是判定證明是否有效的權威。

哪個 LLM 最適合生成形式驗證註解？

GPT-4o 和 Claude 3.5 Sonnet 在 Dafny 和 SMT-LIB 語法方面都表現良好。較小的模型常常難以掌握證明求解器所需的精確語法。將溫度（temperature）設低（0.1–0.2）以減少創意性的幻覺。

如何防止 LLM 生成錯誤的規格？

你無法防止。你應將 LLM 的輸出視為草稿。務必將生成的註解餵給你的驗證器執行。務必閱讀生成的前置條件和後置條件，確保它們符合你的意圖。永遠不要假設驗證成功就代表規格是正確的。

從無聊的部分開始

如果你的團隊正在進行 Cleanroom 或任何正確性導向建構（correctness-by-construction）的工作，最高價值的自動化並非某個宏大的 AI 定理證明器。而是一個能為你生成迴圈不變式、格式化 SMT-LIB 的腳本，讓你不必親自動手。

找出你的codebase中最煩人的五種註解模式。為每一種撰寫提示詞模板。將它們餵給 LLM、驗證輸出，並將通過的結果提交。就這樣。你只花了一筆 API 呼叫的費用，就買回了 40% 的驗證時間。

困難的證明仍然屬於你。但至少你不必從零開始打字了。