超越教科書：評估 LLM 在真實世界 TLA+ 建模中的表現

多年來，TLA+ 一直是規範化並行與分散式系統的金標準，讓工程師能在寫下第一行程式碼之前就發現關鍵的設計缺陷。隨著大型語言模型 (LLM) 的興起，人們越來越傾向於將這一嚴謹的過程委派給 AI。然而，一個關鍵問題仍然存在：AI 究竟是在對當前系統進行建模，還是在僅僅背誦其訓練數據中廣為人知的教科書式實作？

來自 Specula 團隊的最新研究介紹了 SysMoBench，這是一個旨在揭露「教科書式建模」與忠實系統表示之間差距的自動化基準測試。透過在十一個真實世界系統（從並行同步原語到像 Etcd 和 ZooKeeper 這樣複雜的分散式協定）上評估 LLM，該團隊揭示了目前 LLM 在處理形式化規範時的系統性失敗。

正確性的幻覺

當被要求為 Etcd 的 Raft 實作撰寫 TLA+ 規範時，領先的 LLM 通常會產生能通過語法檢查並在 TLC model checker 中無錯誤運行的程式碼。乍看之下，結果看起來很完美。然而，經過仔細檢查，該規範往往反映的是原始 Raft 論文的附錄，而非 Etcd 實際實作中的特定架構選擇。

這是基於 LLM 的建模所面臨的核心挑戰。因為 LLM 看過網路上幾乎所有的 TLA+ 範例，要求提供「Raft spec」會觸發其召回機制而非抽象機制。要真正地對一個系統進行建模，LLM 必須能夠從複雜的原始碼中抽象出邏輯，並將該抽象轉化為正確的形式化模型。

SysMoBench 如何運作

為了區分召回與建模，SysMoBench 採用了四階段評估流程：

  1. Syntax Phase: 檢查規範是否能編譯。
  2. Runtime Phase: 驗證 TLC model checker 是否能在不崩潰的情況下執行該規範。
  3. Conformance Phase: 使用 trace validation 來比較實際程式碼的執行軌跡與模型之間的差異。
  4. Invariant Phase: 檢查該規範是否滿足關鍵的安全 (safety) 與活性 (liveness) 屬性。

雖然大多數前沿 LLM 在語法階段得分接近 100%，但它們在一致性 (conformance) 與不變量 (invariant) 測試中的表現大幅下降。在複雜的分散式系統上，即使是最強大的模型，其總分也經常掉到 10% 到 50% 之間。

兩種「教科書式建模」的模式

研究識別了兩種常見的失敗模式，即 LLM 依賴通用模板而非實作細節：

1. 容許不可能的狀態

LLM 經常使用與系統實際數據結構不符的形式化模板。例如，在 ZooKeeper Fast Leader Election (FLE) 規範中，Claude Sonnet 將伺服器的 recvset 視為集合聯集，允許它累積所有投票作為證據。在真實的 ZooKeeper 程式碼中，這是一個以發送者為鍵 (key) 的 map，這意味著新投票會覆蓋舊投票。這種差異使得規範可以進入真實系統永遠無法到達的狀態。

2. 抹除可達狀態

相反地，LLM 經常將多個實作步驟合併為單個原子守衛 (atomic guard)。在同樣的 ZooKeeper 範例中，LLM 將更新本地邏輯時鐘與處理訊息的行為合併為一個步驟。在實際的程式碼中，這些是按順序發生的。透過將它們合併，LLM 抹除了真實系統在每次選舉輪次中都會進入的狀態，使得規範中的某些轉換 (transitions) 變得不可能。

轉換驗證：細粒度的方法

為了精確定位這些失敗，SysMoBench 利用了 Transition Validation。系統不再對整個模組進行二元式的通過/失敗判定，而是從真實運行中收集執行軌跡，並將其切割成「轉換窗口」(transition windows)（前狀態、動作、後狀態）。

每個窗口都會輸入到 TLC 以驗證該規範的動作是否真的能將系統從前狀態移動到後狀態。這提供了一個針對每個動作的評分卡，讓開發者能精確看到究竟是哪個特定的狀態轉換失敗以及原因，而非僅僅依賴粗略的總分。

更廣泛的影響與開放性挑戰

研究結果顯示，雖然 LLM 在 TLA+ 的語言方面表現出色，但在特定實作的邏輯方面卻很吃力。這引發了關於形式化方法未來發展的更廣泛討論：

  • Coupled Verification: 有人主張採用 Verus 等方法，將實作與驗證結合在一起，以防止模型與程式碼產生分歧。
  • Human Intent: 存在一種哲學上的擔憂，即自動化設計過程會移除人類的意圖。正如一位評論者所言，如果 LLM 生成了設計與程式碼，那麼「證明」可能缺乏有意義的人類保證。
  • Liveness Properties: 用戶指出，與安全屬性相比，LLM 在處理活性屬性（確保某件好事最終會發生）時特別困難。

儘管存在這些障礙，Specula 團隊正在開發專門的代理 (agents) 能夠自主閱讀儲存庫 (repositories) 並驅動規範流程。他們的專門代理 Specula 已經展現出能於目前的 SysMoBench 任務中達到完全一致性與不變量得分的能力，這表明未來的路徑在於代理式工作流 (agentic workflows)，而非單純的 LLM 提示詞 (prompting)。

結論

寫出一個能編譯的 TLA+ 模組是一個很低的門檻；將該模組與特定系統的實際行為對齊齊才是真正的挑戰。隨著我們邁向代理式模型檢查 (agentic model checking)，焦點必須從語法轉向一致性。目標不是產生一個看起來像 Raft 的規範，而是一個就是該系統的規範。

Sources