Claude為開源軟件撰寫機器可驗證證明

驗證工作內容

形式化驗證指以數學方法證明軟件在指定範圍內不會出現某類錯誤。今次工作中，Claude負責找出缺陷並修復，再產出證明，說明該類錯誤不會重現。

項目覆蓋123個開源庫中的239個測試入口，歷時數周，最終證明代碼均經機器檢查確認，整體規模在業界屬於首次見到的量級。

匯編層級意義

有別於以往集中在高階語言的做法，這次驗證直接在匯編代碼層級進行，覆蓋更接近機器執行的層面，對生產級軟件的安全要求更具參考價值。

團隊指出，這是已知首次大規模借助人工智能在匯編層級完成此類工作，顯示大型模型有能力承擔過去倚賴人工專家的驗證任務。

行業應用前景

形式化驗證長期成本高昂，多用於關鍵系統。若人工智能能大幅降低成本，相關技術有望更廣泛應用於一般軟件的可靠性保障及漏洞防範。

業界近年陸續測試以人工智能輔助程序分析，形式化驗證被視為提升關鍵軟件可靠性的方向之一。