Anthropic 與合作夥伴 Theorem 聯手，運用 AI 模型「Claude」，嘗試以數學方式證明現有軟體程式碼能正確運作。驗證對象是 Google 安全專案「OSS-Fuzz」收錄的 123 個開源函式庫。據稱，團隊在幾週內生成約 1 億 8,000 萬行證明程式碼，也找出數百個傳統測試未能發現的錯誤。
「通過測試」與「已證明正確」之間的距離
談到如何確認軟體品質，許多人首先想到的會是測試：輸入準備好的資料，確認是否得到預期結果。不過，測試只能確認「測試過的範圍」，無法告訴我們程式在未測試的情況下會如何運作。
形式驗證正是為此而生。它將程式的行為視為數學問題，證明程式在指定條件範圍內一定能正確運作。理論上這種方法威力強大，但所需工夫也多得驚人。據稱，僅驗證小型作業系統核心「seL4」，專家團隊就投入了累計 20 人年的心力。這也難怪形式驗證過去的用途僅限於客機控制軟體等極端重要的情境。
這次 Anthropic 的 Frontier Red Team 與 Theorem 合作，將證明工作交給 Claude。團隊並非讓它撰寫新程式碼，而是以既有軟體為對象，將用來檢查當機問題的測試轉換成數學問題，再一路分析至編譯後的機器碼，讓 Claude 建立大量證明。
負責「評分」證明的是另一套程式
若 AI 自己撰寫證明、又自行宣稱「合格」，就缺乏說服力。這項工作的評分機制相當值得注意：生成的證明會由獨立的驗證程式 Rocq 自動檢查。Anthropic 表示，這個流程幾乎不需要人類審查者介入。
研究團隊將這種證明生成方式稱為「完全自主」。不過，用來證明的工具和形式化基礎，是由 Theorem 的人類團隊打造的。與其說 AI 從零開始創造了一切，不如說是人類先搭好舞台，再由 AI 在其上一次寫下大量證明，這樣更貼近實際情況。
證明過程中發現數百個錯誤
在推進證明的過程中，Claude 遇到了數百個錯誤，也獲准自行修正。研究人員表示，其中許多錯誤只有在輸入檔案極大，或以特定順序存取記憶體等少數情況下才會出現。一般測試未能發現這些錯誤，並不令人意外。
研究團隊也列出具體案例。在驗證一款廣泛使用的 PDF 閱讀器時，團隊只花一週就找出與該軟體通常一年內接獲通報的數量相同的安全漏洞。據稱，另一款應用程式中還有一個邏輯錯誤，直到十多年後才被發現。
另一個不容忽視的地方，是如何看待未能完成的證明。Anthropic 表示，即使證明失敗，實際錯誤也可能在嘗試過程中浮現。換言之，證明不只是為了取得「合格證明」，也能像探測器一樣挖掘錯誤。與其取代一般測試，它看起來更像是補足測試不足之處。
別誤解「已通過形式驗證」的適用範圍
然而，將「已通過形式驗證」解讀成「完全沒有問題」是很危險的。Anthropic 本身也承認，證明只在嚴格限定的條件下成立。假設條件包括特定的處理器配置、以單執行緒執行的程式，以及小於 64MB 的輸入。實際上的函式庫則會在各種硬體和設定下運作。
成本也不低。據稱，個別證明所使用的 token 數量，有時會達到數億。專案整體費用尚未公開。另一方面，小規模的追加實驗顯示，證明可以重複使用；新模型的效率似乎也有提升。據稱，Opus 5.5 解出一半證明所需的 token，比 Opus 5 少約 40%。
問題從「能不能寫程式」開始轉變
如果 AI 能撰寫程式碼，並在特定條件下保證程式碼正確，問題的問法就會改變。焦點不再是「AI 會不會寫程式」，而是「AI 能不能證明自己所寫程式碼的安全性」。對於擔心 AI 生成程式碼可靠性的開發團隊來說，這樣的轉變意義重大。若 AI 能自行驗證程式碼，就能減輕人工審查的負擔，並有可能降低整個開發流程的成本，而不只是驗證工作的成本。
Anthropic 預期，AI 形式驗證在不久的將來會成為與一般測試同樣普遍的手段。Theorem 的發展藍圖已將 glibc、OpenSSL、cURL 等重要基礎設施級軟體列為驗證對象。
此時，關鍵在於讀懂證明的「前提」，而非「內容」。這份證明假設的是什麼環境、什麼輸入？在連檢查都交給 AI 的時代，人類確認這些前提的素養，或許才是安全性的最後一道防線。
コメント