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

10 月 22 日，人工智能公司 Anthropic 旗下 Frontier Red Team 發佈一項研究，指出大語言模型目前已具備在更大規模上自動生成形式化證明的能力。該團隊聯合 Theorem，基於 Claude 模型，在 RISC-V 匯編層級對逾 100 個真實開源庫開展了安全性質的形式化驗證——這是迄今首次有 AI 系統在匯編層面對生產級軟件實施的大規模形式化驗證。在證明構建過程中，團隊還意外揭示了多個長期未被發現的安全漏洞。實驗方法是將 Google OSS-Fuzz 中已有的可編譯 fuzz 測試用例轉化為形式化規格，並在單線程靜態二進制、固定內存預算、RISC-V CPU 架構及 Linux 運行環境等約束條件下，對任意大小不超過 64 MB 的輸入執行驗證。