形式化驗證或能解決AI的審查瓶頸

形式化驗證作為一種嚴格的數學方法，正在成為解決AI生成程式碼審查瓶頸的關鍵技術。傳統軟體工程中，AI生成的程式碼需要經過人工審查才能確保正確性，而這已成為開發效率的瓶頸。然而，形式化驗證透過將程式碼的規範形式化，使得AI生成的程式碼無需人工審查即可自動驗證其正確性。

文章以電路最佳化器為具體案例，詳細展示了這一方法的實際應用。電路最佳化器的核心任務是確保輸出電路與輸入電路等價（即功能相同），同時儘可能減小電路規模。團隊使用Lean語言編寫了約500行的規範，精確描述了最佳化器正確性的含義。編寫規範耗時約兩天，加上一天的團隊審查。之後，AI代理根據這些規範生成了所有最佳化器程式碼及其證明，整個過程幾乎不需要人工干預。團隊僅透過檢查CI標籤和基準測試結果來“審查”PR，完全不審查生成的程式碼。

基準測試結果表明，最佳化器在電路規模縮減方面與之前的Rust實現相當，儘管執行時速度較慢，但最近三天內最慢的測試用例速度提升了三倍以上。團隊透過FFI將Lean編譯的C程式碼整合到現有的Rust程式碼庫中，逐步替換元件，無需重寫整個程式碼庫。

作者認為，這種方法的關鍵在於編寫和審計規範的成本必須低於編寫和維護程式碼的成本。未來，可複用的規範庫和模組化方法可能使形式化驗證更廣泛地應用。軟體開發可能最終從關注程式碼轉向關注需求，關鍵屬性被形式化，其他部分透過提示和測試驗證。開發者可能不再直接看到生成的程式碼，甚至不知道其程式語言。這為AI時代的軟體工程提供了全新方向，有望顯著縮短從開發到部署的週期。