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

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

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

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

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