Lean 與 LLMs 的證明自動化
Lean 與 LLMs 的證明自動化
LLMs 正讓形式化驗證變得實用
歷史上，採用依賴型別語言的主要障礙一直是「證明工作量」——證明一個程式遵守其指定不變式所需的巨額手動勞動。seL4 微核心專案成為此開銷的基準，工程師花費約 10 倍的時間來證明系統，而設計與實現則較少，導致證明程式碼的行數是 C 程式碼的 20 倍。
大型語言模型 (LLM) 正透過自動生成這些證明來改變這種情況。因為像 Lean 這樣的依賴型別系統可以機械化驗證證明是否正確，LLM 的「幻覺」風險被消除：如果 LLM 產生了錯誤的證明，型別檢查器會直接拒絕它。這種轉移將軟體工程的負擔從編寫實作和證明，轉移到編寫精確的正式規格。
案例研究：在 Lean 中的已驗證 Zstandard 解壓縮器
為了探索 Lean 與 LLM 自動化的交叉點，實作了一個 Zstandard (zstd) 解壓縮器。Zstandard 是一種高效能的壓縮工具，它結合了 LZ77 和一種稱為 Finite State Entropy (FSE) 的複雜熵編碼器。
FSE 的挑戰
FSE 是一種基於狀態機的熵編碼器，透過將符號分佈到多個狀態來允許每個符號具有分數位元。這使其能夠實現比霍夫曼編碼更高的壓縮率，而霍夫曼編碼僅限於整數位元增量。然而，FSE 要求解壓縮器從區塊的末端倒序讀取位元，這增加了顯著的實作複雜度。
形式化不變式
在一般語言中，優化解碼循環所需的假設通常被放在註解或運行時檢查中。在 Lean 中，這些可以被編碼為正式定理。對於 FSE 表的構建，以下普遍性質在 LLM 的協助下被正式證明：
- 正確表大小：表格符合指定的精度常數。
- 符號分佈：分配給符號的狀態數量正確反映其概率。
- 狀態有效性：對任何狀態，加上基線值和讀取的位元總是會得到一個有效的狀態編號。
- 可達性：對於每個非零概率的符號，恰好有一個狀態可以到達任何給定的目標狀態。
這些證明傳統上需要數小時或數天的手動工作，但在 LLM 的協助下約 20 分鐘內就被生成。
Lean 在系統程式設計中的技術優勢
Lean 提供了幾項功能，使其比傳統定理證明器更適合程式設計：
- 嚴格求值：與 Haskell 的惰性求值不同，Lean 是嚴格的，使得效能和資源使用更易於推理。
- 命令式語法糖：Lean 的單子
do表示法支援 for 迴圈、return 語句和 break 語句，允許使用命令式編碼風格。 - 引用計數優化：當物件的引用計數為一時，Lean 可以就地變異該物件，從而實現類似命令式語言的高效陣列更新。
已驗證軟體未來的觀點
朝向規格工程的轉移
產業討論表明，程式設計師的角色正在朝向「規格工程」轉移。如果實作是由 LLM 生成並由定理證明器驗證的製品，則軟體唯有人類面向的部分就成為規格本身。這要求規格必須是模組化的、可組合的，且足夠簡短以供人類驗證。
擴展問題
一些批評者認為，依賴型別在一般維護方面無法擴展。為程式添加新的不變式通常需要精煉每個依賴型別，並適應整個代碼庫中的每個證明，因為計算和證明是交織在一起的。建議的替代方案是主要在模組邊界使用依賴型別來暴露不透明類型，同時將內部問題分開處理。
已驗證的組合語言與效能
人們對使用類似 AWS 的 LNSym（AArch64 的語義與模擬器）工具產生了濃厚興趣，以證明高階 Lean 函式與最佳化組合語言實作之間的等價性。這將使 LLMs 能夠激進地優化組合語言程式碼，而不會引入功能錯誤，因為等價性可以被形式化驗證。
『錯誤事物的正確性』風險
形式化驗證證明實作符合規格，但無法證明規格本身正是使用者實際想要的。正如社區討論所指出的，如果提供給 LLM 的規格本身也是錯誤的，LLM 仍會勤勉地證明一個完全顛倒實作的功能的正確性。