Google DeepMind 發表 AlphaProof Code，僅需四週即完成 Signal 加密核心驗證

Google DeepMind 發表了全新人工智慧系統 AlphaProof Code，旨在透過數學方式嚴格驗證軟體是否符合其安全性規範且完全無誤。

為了展示其強大能力，研究人員利用這項技術驗證了加密通訊軟體 Signal 的加密協定。AlphaProof Code 在短短四週內便完成了 Signal 核心加密程式碼的形式驗證（formal verification），而這項工作過往通常需要耗費人類專家數年的努力。

大規模驗證真實世界的程式碼

根據 DeepMind 研究人員 Pushmeet Kohli 與 Swarat Chaudhuri 的說法，過去的形式驗證工作往往僅停留在理論設計階段。而 AlphaProof Code 則更進一步，直接驗證了在使用者裝置上運行的實際加密程式碼。

該系統依賴建立在 Google Gemini Carbon 基礎上的 AI 代理。在專家定義好形式安全性需求後，AI 代理協助制定規範，並以 Lean 證明語言產生了超過 600 萬行的形式證明，獨立證明該軟體符合這些條件。

在此過程中，AI 標記了約 1% 的程式碼供專家進行人工審查。為了評估其可靠性，研究人員還故意在程式碼庫中植入了兩個漏洞進行測試，而 AlphaProof Code 立即抓出了這兩個漏洞。

擴展至關鍵基礎設施

Signal 協定成功通過驗證，凸顯出人工智慧在保護敏感數位系統方面扮演著越來越重要的角色。Signal 技術長 Ehren Kret 指出，隨著威脅情勢演變，這種驗證方法有助於強化人們對資料隱私的信任。

展望未來，Google DeepMind 計劃運用 CodeMender 等系統，將形式驗證方法論從即時通訊軟體進一步擴展至醫療器材與電網等真實世界的關鍵基礎設施。