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