LLM 時代的可靠軟體開發

背景

隨著大型語言模型（LLM）在軟體開發中的普及，如何驗證 AI 生成代碼的正確性成為一大挑戰。Informal Systems 團隊提出利用 Quint 規範語言作為 AI 與實際代碼之間的驗證橋樑，透過將自然語言需求轉化為可執行的規範，並結合模型檢查與測試，試圖在 AI 輔助開發的時代建立一套可靠的軟體工程流程。

社群觀點

Hacker News 社群對於這套流程的看法呈現兩極化。部分討論者對「AI 時代」這類術語感到疲勞，甚至戲稱當前為「垃圾資訊十年」（Slop Decade），認為 AI 生成的大量代碼若缺乏嚴謹審核，只會增加系統的混亂。然而，也有資深開發者指出，軟體可靠性的本質並未因 AI 而改變，單元測試、集成測試與監控依然是核心。他們將 AI 視為一種「匿名開源貢獻者」，雖然能提供大量產出，但核心團隊必須具備更強的審核能力，才能處理這種高頻率且可能帶有隱蔽錯誤的代碼貢獻。

在技術實踐層面，社群對「規格驗證」（Spec Validation）的重要性達成了一定共識。有評論者分享，自己在開發過程中投入在規格細化與驗證上的資源，往往是生成代碼本身的十倍以上。這種觀點支持了文章的主張，即人類開發者的重心應從編寫代碼轉向定義屬性與邊界。然而，也有反對聲音認為，理解並驗證 AI 生成的複雜代碼，有時比從零開始編寫還要耗時，因為開發者必須先理清 AI 的邏輯才能進行形式化驗證，這反而可能降低整體的開發效率。

此外，關於測試策略的轉變也引起了熱烈討論。有開發者發現，為了防止 AI 「鑽漏洞」通過測試，必須建立更龐大且多樣化的測試分類體系。例如，過去人類編寫代碼時不會考慮的荒謬錯誤（如介面元素無故閃爍），在 AI 時代可能需要專門的測試來捕捉。這種現象顯示出，雖然 AI 降低了代碼生成的門檻，卻顯著提升了對測試魯棒性的要求。同時，模型更新導致的行為漂移也是一大隱憂，即便測試通過，模型內部的判斷邏輯變化仍可能在不知不覺中破壞既有的契約。

延伸閱讀

• Quint: 一種基於 TLA+ 語法但更接近現代程式語言（如 C 或 TypeScript）的規範語言，強調類型安全與可執行性。
• TLA+: 由 Leslie Lamport 開發的正式規範語言，用於設計、建模和驗證並行與分散式系統，是 Quint 的理論基礎。
• Hitchens' Razor（希欽斯剃刀）: 討論中提到的邏輯原則，意指「無須證據的斷言，可以無須證據地駁回」，被留言者用來評論 AI 生成內容的品質爭議。