Bend 2 與「氛圍編碼」陷阱：為何忽略既有研究會導致冗餘的形式化驗證工作

核心要點

Bend 2 試圖讓人類編寫「法則」(laws)，並由 LLM 生成實作與證明，但這種方法需要 58 行法則規範與 442 行 AI 生成的證明。相比之下，同樣的正確性屬性可以在 SPARK 中以不到 12 行的程式碼表達並自動驗證，這顯示忽略既有研究可能會產生不必要的複雜解決方案。

Bend 2 聲稱提供的功能

人類編寫的法則：開發者編碼高階不變量（例如：「玩家永遠不能觸碰旗幟」）。
LLM 生成的實作：AI 填寫遊戲邏輯。
LLM 生成的證明：AI 同時編寫形式化證明，確保實作符合法則。
編譯器驗證：Bend 編譯器檢查證明的健全性。

Bend 首頁的示範包含一個 LAWS.bend 檔案（58 行）以及對應的 PROOF.bend 檔案（442 行）。該部落格文章的作者認為，這種冗長顯示了設計上的缺陷。

「氛圍編碼」陷阱解析

「氛圍編碼 (Vibe coding) 讓人們在尚未充分了解問題、無法識別出更好的解決方案存在之前，就先建立了一個龐大的系統。」

氛圍編碼 指的是在沒有先調查現有文獻的情況下，僅憑模糊的想法提示 LLM 產生一個完整的系統。當出現以下情況時，陷阱就會顯現：

跳過研究 – 開發者依賴 LLM 的輸出，而不是檢查該問題是否已經被解決。
產生冗餘工作 – 最終系統重複了成熟工具已經提供的功能。
複雜度膨脹 – LLM 必須生成大量的樣板程式碼（例如 442 行的證明），而這些本可以透過現有的自動化證明器來避免。

具體比較：Bend 2 與 SPARK

部落格作者在 SPARK 中重現了 Bend 的示範，這是一種專為形式化驗證設計的 Ada 語言。SPARK 版本包含：

針對欄、列與遊戲狀態的型別定義。
一個表達不變量的 Safe 幽靈函式 (ghost function)。
一個帶有確保安全性保持之後置條件 (post-condition) 的 Step 程序。
一個帶有玩家永遠不會獲勝之後置條件的 Replay 函式。
一個簡單的驅動程式來顯示遊戲。

在此程式碼上執行 gnatprove 會得到：

Success: all checks proved (12 checks).

僅產生了十幾個驗證條件，且不需要手動編寫證明腳本。整個正確性論證由底層的 SMT 求解器自動處理。

關鍵差異

項目	Bend 2	SPARK
規範大小	58 行法則	約 30 行 Ada 型別與合約
證明大小	442 行 AI 生成證明	0 行（自動 SMT 證明）
工具鏈成熟度	新穎、高度依賴 AI、99% AI 編寫的編譯器	數十年歷史、經審計、與 GNAT 工具鏈整合
社群支援	小型、主要為實驗性質	成熟的 Ada/SPARK 社群、豐富的函式庫

Hacker News 上的社群反應

@pu_pe 指出關於 Bend 作者聲譽的討論，認為爭論焦點更多在於個人而非技術本質。
@z7 糾正了關於作者不了解形式化驗證的說法，並指出作者先前關於該主題的文章。
@captainmuon 主張現有的驗證語言語法通常過於沉重，開發者渴望使用更熟悉的語言（如 C# 或 JavaScript）並內建合約。
@mentalgear 強調任何由 LLM 驅動的專案都應先執行「先進行既有研究」的步驟，以避免重複造輪子。
@LightMachine 為設計選擇辯護，稱明確的證明是為了效能考量，且該語言的核心刻意保持精簡。
@simonw 分享了個人工作流程：在開始專案前，要求具備搜尋功能的 LLM 找出既有技術，這為他節省了時間。
@thomasahle 澄清 SPARK 的自動證明依賴於 SMT 求解器，這些屬於暴力破解，無法擴展到像 Lean 或 Bend 這類互動式證明器的表達能力。
@mccoyb 強調 Bend 2 是一個 定量型別理論 (QTT) 系統，使其在驗證光譜中處於與 Ada/SPARK 不同的位置。

這些評論顯示了分歧的觀點：有些人認為 Bend 2 是不必要的重新發明，而另一些人則將其視為對不同驗證範式的有益探索。

給使用 LLM 開發者的建議

從文獻調查開始 – 在編寫程式碼之前，要求 LLM 列出與您問題相關的現有工具、語言與函式庫。
識別驗證模型 – 決定您需要的是自動化基於 SMT 的驗證（如 SPARK、Dafny）還是互動式定理證明（如 Coq、Lean、Bend 2）。
衡量節省的工作量 – 將規範與證明的大小與已知基準進行比較；過多的樣板程式碼可能表示錯過了現有的解決方案。
利用社群資源 – 成熟的生態系統提供經審計的編譯器、標準函式庫與工具，能降低風險。
將 LLM 輸出視為草稿 – 審查生成的證明，確保其正確性並符合目標驗證框架中的最佳實踐慣例。

結論

Bend 2 展示了 AI 輔助形式化驗證的願景，但其冗長的證明生成凸顯了一個更廣泛的「氛圍編碼」風險：在未了解技術現狀的情況下建構複雜系統。透過進行簡短的既有技術搜尋，開發者通常可以用少量的自動驗證條件取代數千行 AI 生成的證明，從而節省時間、Token 並減少潛在 Bug。關於 Bend 2 的討論提醒我們，LLM 在提升生產力的同時，也放大了重複解決已解決問題的風險。