AI 程式碼引軟體信任危機，Theorem 押注形式化驗證讓抓 Bug 精準又自動化
隨著 AI 重塑軟體開發產業，來自美國舊金山的新創公司 Theorem，選擇押注下一個潛力無窮的商機，那就是該如何讓企業在產生大量 AI 程式碼的同時，也能夠「信任」這些程式碼。
日前 Theorem 對外宣布，公司已經完成價值 600 萬美元的新一輪融資，主要由 Khosla Ventures 領投，加上 Y Combinator 及多位天使投資人參與。
Theorem 特別強調，公司順利取得融資後，將以打造自動化工具為目標，用以驗證 AI 生成軟體的正確性。
AI 寫程式高速狂奔，驗證速度卻如牛步
對於 Theorem 甚至整個軟體產業來說，如何信任 AI 所生成的程式碼，早已成為業界急需解決的問題。
包含 GitHub、Amazon 和 Google 的 AI 技術在內，全世界的 AI 工具，每年生成規模已達數十億行程式碼等級，協助軟體開發者打造新程式，企業採用率也同步飆升。然而，驗證 AI 所寫的軟體是否運作正常，其檢驗速度卻遠遠跟不上。
Theorem 創辦人 Jason Gross 指出，上述情況就是軟體開發產業的「監管缺口（Oversight Gap）」，該問題對全世界的金融系統、電網等關鍵基礎設施，構成了十分重大的威脅。
Jason Gross 直言，在軟體開發領域邁入 AI 時代後，假如有人叫他審查多達 6 萬行的程式碼，自己根本就無從下手，這就是軟體業當前面臨的最大問題。
將數年的形式化驗證，縮短到只要數天
為了自動化驗證 AI 程式碼的正確性，Theorem 所開發的核心技術，結合了「形式化驗證（Formal Verification）」與 AI 模型。
簡單來說，形式化驗證是一種數學技術，能夠證明軟體行為完全符合規範，至於 Theorem 則藉由訓練 AI 模型，自動生成並檢查這些數學證明。
根據 Theorem 的說法，他們的 AI 核心技術能夠將原本需要博士級工程師，耗費數年才可以完成的工作，縮短成數週甚至數天——在過去，實施形式化驗證的成本開銷極高，每 1 行程式碼往往需要 8 行數學證明，導致該技術僅被應用於航空電子、核反應爐控制、加密協議等，絕對不能出錯的領域。
Jason Gross 以自身經驗舉例，他過去於麻省理工學院（MIT）攻讀博士時，曾參與驗證 HTTPS 安全協議的專案，而由於該專案採用了形式化驗證，所以直到完成至少就耗費了超過 15 人年（Person-years）的人力。
Jason Gross 說，由此可見，過去在軟體開發領域採用形式化驗證，顯然並不符合經濟效益，然而，當今充分發展的 AI 技術將有能力代勞。
聰明運用算力，打破上下文窗口限制
深度探討 Theorem 核心技術的基礎原理，Jason Gross 將它稱為「fractional proof decomposition」；該原理要求 AI 模型聰明運用算力，不要全面測試程式碼的每一個行為，而是改成依據組件的重要性，按比例分配驗證資源。
Theorem 所採用的方法，最近在某大型 AI 系統中抓到了一個傳統測試未發現的 Bug；而在另一個被稱為 SFBench 的技術展示中，Theorem 透過 AI 將 1,276 個數學問題，從 Rocq 語言翻譯成 Lean 語言，並自動化證明每個翻譯版本與原始版本等效。
根據 Theorem 公司估算，SFBench 技術展示的工作量，若由人類團隊來執行，至少將需要 2.7 人年。
Jason Gross 表示，Theorem 的架構能處理複雜、跨檔案的相依程式碼，這是目前大多數受限於「上下文窗口（Context Window）」的 AI 程式碼撰寫工具難以做到的。
效能提升百倍，不必人工審查就部署
在技術上擁有獨特優勢的 Theorem，目前已經開始跟 AI 實驗室、電子設計自動化及 GPU 運算領域的客戶進行合作。
Jason Gross 回憶，曾經有名客戶帶著一份 1,500 頁的 PDF 規格書，以及一套充滿記憶體洩漏（Memory Leaks）、崩潰及隱性 Bug 的舊系統向 Theorem 發起求助。該客戶希望將系統效能從 10 Mbps 提升至 1 Gbps，也就是翻上 100 倍，而且不能出現任何錯誤。
最後，Theorem 的 AI 生成了超過 16,000 行的「正式程式碼」，並且在客戶沒有進行任何人工審查的情況下，就直接部署上線。
Theorem 之所以對翻新後的系統如此具備信心，在於他們透過數學驗證，確保了新程式碼與客戶預期中的目標行為完全一致，甚至僅靠僅幾百行程式碼，就概括了 PDF 規格書的所有內容。
AI 時代軟體安全，驗證技術成為關鍵
隨著電腦程式成為金融市場、醫療設備和電網的運作基礎，AI 雖然加速了軟體的迭代，但也讓微小的 Bug 更加容易擴散，並吸引駭客和攻擊者的覬覦。
因此 Jason Gross 認為，當 AI 開始讓駭客攻擊基礎設施的成本大幅下降，防禦者將更需要明白「不對稱防禦」的重要性，即防禦能力的擴展，並不需要耗費同等比例的資源。
同時 Jason Gross 強調，如果業界想要一套能夠承受數代模型升級後，依然持續有效的軟體安全解決方案，那麼「驗證技術」將會變得更加關鍵。
Jason Gross 以非常針對性的角度向外媒直言，軟體安全是科技攻防之間的微妙平衡，當形式化驗證的成本已經被降得夠低，監管機構若不強制要求關鍵基礎設施，必須使用形式化驗證技術，藉此保障系統的整體安全性，那麼這將會成為監管機構的「重大過失」。
不只算數學，更要解決系統工程問題
若跟其他 AI 程式碼驗證公司相較，除了核心技術，Theorem 又有哪些獨特之處來贏得競爭？
對此 Jason Gross 認為，Theorem 專注於解決「系統工程」問題，而非純數學領域，他們的工具是為了那些「接近硬體底層」、需要高度正確性保證的工程團隊所設計。
Theorem 的團隊背景也反映出了這種技術導向。Jason Gross 本人擁有程式語言理論的深厚知識，以及大規模部署驗證工程的相關經驗；至於共同創辦人 Rajashree Agrawal 則專注於訓練機器學習模型，透過 AI 驅動驗證流程。
AI 超越人類開發能力將「難以避免」
在獲得充足融資後，Theorem 計劃擴充目前僅有 4 人的公司團隊，並增加訓練驗證模型所需的運算資源，同時考慮進軍機器人、再生能源、加密貨幣及藥物合成等新興產業。
如 Theorem 這類新創公司的崛起，或許預示著企業的技術領導者，評估 AI 程式碼撰寫工具的方式，即將出現重大轉變。
第一波 AI 程式輔助開發浪潮，為開發者帶來生產力的提升，使程式碼的輸出變得更多、更快；而 Theorem 則押注第二波浪潮，希望以數學證明的方式，確保程式碼產出速度的提升，不會以犧牲安全為代價。
Jason Gross 批判指出，如果 AI 繼續以指數級速度進步，那麼人工智慧某一天超越人類的軟體工程能力，將會變得無法避免。因此 Jason Gross 警告，假若人類根本沒有準備好，運用更準確、更先進的驗證手段，並徹底改變現有的監管方式，適應未來的全新經濟模式，最終人類只會打造出，連自己都無法控制的新系統。
【推薦閱讀】
◆ 晶片設計 70% 時間在寫程式？Cadence 推 AI 代理 ChipStack，稱生產力提升 10 倍
◆ 縮短 30% 上市時間、降低 60% 檢測成本！合成數據重塑製造業品質管理
◆ AI 寫程式只能選巨頭？開源黑馬 OpenCode 崛起，用「多代理零衝突」打破壟斷
＊本文開放合作夥伴轉載，參考資料：VentureBeat、Radical Data Science，首圖來源：Nano Banana Pro
（責任編輯：鄒家彥）