AI寫程式易出錯？矽谷新創Axiom獲2億美元投資 挑戰程式碼驗證

商傳媒｜責任編輯／綜合外電報導

AI 技術在程式碼生成方面的應用日益廣泛，然而程式碼錯誤的問題也隨之浮現。矽谷新創公司 Axiom 瞄準此一痛點，致力於開發程式碼驗證技術，並於 3 月 16 日宣布獲得 2 億美元的最新一輪融資。

Axiom 總部位於美國加州帕奧圖，鄰近祖克柏（Mark Zuckerberg）創立 Facebook 的辦公室舊址。這家成立僅一年的新創公司，目前約有 20 名員工，估值已達 16 億美元。此輪融資由 Menlo Ventures、Greycroft 和 Madrona 等創投公司領投，顯示投資者對其技術潛力的看好。

Menlo Ventures 合夥人克拉寧（Matt Kraning）表示，目前使用 AI 撰寫程式碼的最大問題在於難以辨識程式碼中是否含有錯誤。他認為，Axiom 等公司的技術有助於解決此問題。

AxiomProver 數學驗證技術

Axiom 的技術核心為 AxiomProver，最初是為了解決數學問題而開發。去年 12 月，AxiomProver 在 Putnam Exam 數學競賽中獲得滿分，該競賽旨在測試頂尖大學生的數學能力。透過電腦程式語言 Lean，AxiomProver 能夠正式驗證答案的正確性。

Axiom 的目標是將這項數學驗證技術應用於電腦程式碼的驗證。該公司表示，其技術在程式碼驗證的標準測試中已取得高分。研究人員稱此為「遷移學習」，意指系統學習一項技能（如驗證數學問題）後，能成功將該技能轉移到不同的任務（如驗證電腦程式碼）。

程式碼驗證的挑戰與限制

卡內基美隆大學電腦科學教授瓦西列斯庫（Bogdan Vasilescu）指出，數學問題的正確與否有明確區分，但電腦程式設計的正確性更難界定，尤其是在社交媒體服務等需要處理全球數百萬用戶的複雜情境下。他認為，AI 雖然可以在某些方面驗證程式碼，但並非所有問題都能迎刃而解。

儘管面臨挑戰，Axiom 執行長洪（Carina Hong）表示，隨著公司持續訓練系統進行程式碼驗證，AI 生成程式碼的品質將可進一步提升。