公司估值超過16億美元。
AI初創公司Axiom完成2億美元A輪融資，創始人：“幫科學家將好奇轉化為真理”
來源|多知
作者|王上
3月12日，致力于構建能夠對軟件和科學推理進行數學驗證的AI初創公司Axiom(axiommath.ai)宣布完成A輪融資，本輪融資由Menlo Ventures 領投，籌集了2億美元的新資金，公司估值超過16億美元。
此輪融資代表著對其所稱的“可信人工智能”(verified AI)這一新范式的押注，該技術旨在一勞永逸地消除人工智能“幻覺”的風險。
創始人洪樂潼(Carina Hong)說：“此輪融資將我們在形式數學領域的領先優勢拓展至可信人工智能領域。”
洪樂潼說：“數學家和理論科學家構想理論，提出假設。然后他們提出證明，這是一個包含兩個步驟的發現過程。我們創建Axiom，是為了將好奇的火花轉化為已知的真理，并壓縮取得突破的時間線。”
盡管像Claude Code和CodeRabbit這樣的現有工具能夠生成一些確實令人印象深刻且通常運行良好的代碼，但其概率性的本質是一個主要的擔憂原因。
這類工具旨在產生看起來正確的輸出，而非那些可被證明是正確的輸出。
Menlo Ventures 公司的合伙人馬特·克蘭寧(Matt Kraning)和C.C. 龔(C.C. Gong)認為，這是一個大問題。在宣布本輪融資的博客文章中，他們寫道，當代碼將被用于關鍵基礎設施系統時，“能頻繁工作”是一個“可怕的標準”。
Axiom 通過訓練人工智能系統生成用Lean語言編寫的、經過形式化驗證的輸出來規避這一問題。Lean是一種專為數學證明設計的編程語言。通過使用Lean，公理量化可以確保人工智能模型推理過程的每一步都是“可機器檢查的”并且在邏輯上得到保證。
洪樂潼說：“我們創建 Axiom 的初衷是相信，從夢想的假設到最終的證明，只需幾個小時，而非漫長的一生。經過驗證的人工智能將猜想-證明的循環推廣開來：任何已定義的事物都可以執行;任何已指定的事物都可以證明。這適用于數學、硬件和軟件等各個領域。”
“我們相信，一旦驗證能力突破關鍵閾值，將引發智能領域的范式轉變。我們相信，實現已驗證人工智能的速度和質量決定了超級智能的速度和質量。”洪樂潼說。
洪樂潼出生于廣州，現年24歲，是一位學術成就卓越的斯坦福數學博士。她本科就讀于麻省理工學院，獲得數學和物理雙學位，隨后考取斯坦福大學數學博士，研究方向為數論、組合學和概率學。在校期間，她的論文已發表在《美國數學會會報》、《拉馬努金期刊》等權威刊物，并于2021年獲得牛津大學羅德獎學金，成為僅有的4名中國獲獎者之一。
洪樂潼組建了一個超級團隊，Axiom 的創始數學家肯·小野(Ken Ono)是古根海姆、帕卡德和斯隆獎學者，曾任美國數學學會副主席，也是世界頂尖的拉馬努金數學權威之一。
Axiom 的首席技術官是前Facebook人工智能研究總監舒博·森古普塔(Shubho Sengupta)，他曾幫助英偉達公司編寫了基礎性的圖形處理器庫。團隊還包括弗朗索瓦·沙爾東(François Charton)，他因率先應用Transformer模型解決了一個困擾專家130多年的數學難題而聞名。
Axiom 在去年10月已經完成了6400萬美元的種子輪融資，此后取得了顯著進展。去年12月，其確定性人工智能在普特南數學競賽(Putnam Competition)中取得了完美成績，該競賽被數學家們認為是世界上最具挑戰性的本科生數學考試。
Axiom 可驗證地證明了一個已有20年歷史的數論猜想，該猜想涉及用于測量曲面距離的微積分元素。這是一個挑戰，肯·小野多年來屢次嘗試都未能解決。
對于人工智能的每一個輸出Axiom 都會生成一個由海量經過驗證的數據組成的“可信數據飛輪”。這些數據隨后被反饋回訓練循環中，以增強其模型的能力，同時避免引入“模型崩潰”的風險。“模型崩潰”指的是數據污染給未經驗證的人工智能模型帶來的問題。通過這種方式，Axiom 形成了一個遞歸的自我改進循環。
研究公司Constellation Research的霍爾格·穆勒(Holger Mueller)表示，對于日益依賴“氛圍編碼”工具的開發者來說，一個能解決其風險的可行方案備受追捧。他認為，如果公理量化成功，將贏得大量擁躉。“大語言模型產生幻覺的風險并不‘可愛’;當涉及到它們編寫的代碼時，這是完全錯誤的，而且往往非常危險，”該分析師說。“Axiom 采取了正確的方法，利用數學來驗證和核實人工智能生成的代碼是安全可靠的。”
此輪融資的領投方Menlo Ventures 是一家成立于1976年的美國知名風險投資機構，專注于對消費科技和生命科學領域的早期至擴張期初創企業進行投資。
相關閱讀：
