Anthropic：Claude 已大規模形式化驗證開源庫

ChainCatcher 消息，人工智能公司 Anthropic 旗下 Frontier Red Team 于 10 月 22 日發布研究，稱大語言模型已能在更大規模上自動撰寫形式化證明。團隊與 Theorem 合作，使用 Claude 在 RISC-V 匯編層對超過 100 個真實開源庫證明安全性質，并稱這是已知首次用 AI 在匯編層對生產軟件做大規模形式化驗證。寫證明過程中還發現了多年未被發現的漏洞。實驗將 Google OSS-Fuzz 中已有的可編譯 fuzz 測試轉為規格：在單線程靜態二進制、固定內存預算、RISC-V CPU 與 Linux 等假設下，對小于 64 MB 的任意輸入，程序應正常退出且不觸發內存安全錯誤或斷言失敗。數周內，Claude 在修補所發現問題后，對 123 個 OSS-Fuzz 庫中的 239 個入口點證明了上述性質。證明針對編譯后的 RISC-V 指令，約 1.8 億行 Rocq，并由 Rocq 內核檢查。頁面稱，這并不等于這些庫沒有漏洞，剩余問題可能位于受信任組件或證明范圍之外。頁面還稱，團隊讓 Claude 形式化 RFC 1950，并在 x86 二進制層證明 Linux 內核中的 zlib 實現符合該規格；用 Rust 編寫覆蓋 Python 大子集的解釋器，對超過 170 萬個隨機生成程序與 CPython 行為一致的比例為 99.95%。在 36 個小型驗證任務上，Opus 5.5 證明其中一半所需 token 比 Opus 5 少約 40%。團隊同時指出，證明針對單線程、靜態鏈接的 RISC-V 二進制，且證明檢查器不能判斷規格是否符合現實。

• 喜歡使用社交軟體關注？關注我們的 Twitter，或者加入 Telegram！
• 想關注最新資訊？ 下載CoinCarp App吧
• 有新聞需要爆料，官方公告需要發布? 來給我們發郵件吧！[email protected]