近日，AI初創(chuàng)公司Axiom宣布完成2億美元A輪融資，公司估值飆升至16億美元。此次融資由硅谷頂級(jí)風(fēng)投MenloVentures領(lǐng)投，Greycroft、MadronaVenture、BCapital、ToyotaVentures等老股東全部跟投。Axiom的創(chuàng)始人是25歲的洪樂潼（Carina Hong），她讓大模型的推理過程像數(shù)學(xué)證明一樣嚴(yán)格，每一步都可驗(yàn)證。洪樂潼17歲進(jìn)入MIT，3年修完雙學(xué)位，本科期間發(fā)表了9篇學(xué)術(shù)論文，研究方向涵蓋模橢圓曲線、K3曲面上的L函數(shù)、"月光猜想"等基礎(chǔ)數(shù)學(xué)領(lǐng)域。

Axiom采用"數(shù)學(xué)即服務(wù)"模式，通過訓(xùn)練AI系統(tǒng)生成用Lean語言編寫的、經(jīng)過形式化驗(yàn)證的輸出。Lean是一種專為數(shù)學(xué)證明設(shè)計(jì)的編程語言，通過使用Lean，Axiom可以確保AI模型推理過程的每一步都是可機(jī)器檢查的并且在邏輯上得到保證。去年12月，Axiom的核心系統(tǒng)在普特南競(jìng)賽中斬獲滿分，12題全對(duì)。普特南競(jìng)賽是北美地區(qū)最負(fù)盛名的大學(xué)生數(shù)學(xué)競(jìng)賽，成績(jī)的中位數(shù)常常為零（滿分120分）。過去近百年，僅有5人達(dá)成過滿分成就。Axiom的AI做到了。