AI初創(chuàng)公司Axiom完成2億美元A輪融資，創(chuàng)始人：“幫科學(xué)家將好奇轉(zhuǎn)化為真理”

　　來(lái)源|多知

　　作者|王上

　　3月12日，致力于構(gòu)建能夠?qū)浖涂茖W(xué)推理進(jìn)行數(shù)學(xué)驗(yàn)證的AI初創(chuàng)公司Axiom(axiommath.ai)宣布完成A輪融資，本輪融資由Menlo Ventures 領(lǐng)投，籌集了2億美元的新資金，公司估值超過(guò)16億美元。

　　此輪融資代表著對(duì)其所稱的“可信人工智能”(verified AI)這一新范式的押注，該技術(shù)旨在一勞永逸地消除人工智能“幻覺(jué)”的風(fēng)險(xiǎn)。

　　創(chuàng)始人洪樂(lè)潼(Carina Hong)說(shuō)：“此輪融資將我們?cè)谛问綌?shù)學(xué)領(lǐng)域的領(lǐng)先優(yōu)勢(shì)拓展至可信人工智能領(lǐng)域。”

　　洪樂(lè)潼說(shuō)：“數(shù)學(xué)家和理論科學(xué)家構(gòu)想理論，提出假設(shè)。然后他們提出證明，這是一個(gè)包含兩個(gè)步驟的發(fā)現(xiàn)過(guò)程。我們創(chuàng)建Axiom，是為了將好奇的火花轉(zhuǎn)化為已知的真理，并壓縮取得突破的時(shí)間線。”

　　盡管像Claude Code和CodeRabbit這樣的現(xiàn)有工具能夠生成一些確實(shí)令人印象深刻且通常運(yùn)行良好的代碼，但其概率性的本質(zhì)是一個(gè)主要的擔(dān)憂原因。

　　這類工具旨在產(chǎn)生看起來(lái)正確的輸出，而非那些可被證明是正確的輸出。

　　Menlo Ventures 公司的合伙人馬特·克蘭寧(Matt Kraning)和C.C. 龔(C.C. Gong)認(rèn)為，這是一個(gè)大問(wèn)題。在宣布本輪融資的博客文章中，他們寫道，當(dāng)代碼將被用于關(guān)鍵基礎(chǔ)設(shè)施系統(tǒng)時(shí)，“能頻繁工作”是一個(gè)“可怕的標(biāo)準(zhǔn)”。

　　Axiom 通過(guò)訓(xùn)練人工智能系統(tǒng)生成用Lean語(yǔ)言編寫的、經(jīng)過(guò)形式化驗(yàn)證的輸出來(lái)規(guī)避這一問(wèn)題。Lean是一種專為數(shù)學(xué)證明設(shè)計(jì)的編程語(yǔ)言。通過(guò)使用Lean，公理量化可以確保人工智能模型推理過(guò)程的每一步都是“可機(jī)器檢查的”并且在邏輯上得到保證。

　　洪樂(lè)潼說(shuō)：“我們創(chuàng)建 Axiom 的初衷是相信，從夢(mèng)想的假設(shè)到最終的證明，只需幾個(gè)小時(shí)，而非漫長(zhǎng)的一生。經(jīng)過(guò)驗(yàn)證的人工智能將猜想-證明的循環(huán)推廣開(kāi)來(lái)：任何已定義的事物都可以執(zhí)行;任何已指定的事物都可以證明。這適用于數(shù)學(xué)、硬件和軟件等各個(gè)領(lǐng)域。”

　　“我們相信，一旦驗(yàn)證能力突破關(guān)鍵閾值，將引發(fā)智能領(lǐng)域的范式轉(zhuǎn)變。我們相信，實(shí)現(xiàn)已驗(yàn)證人工智能的速度和質(zhì)量決定了超級(jí)智能的速度和質(zhì)量。”洪樂(lè)潼說(shuō)。

　　洪樂(lè)潼出生于廣州，現(xiàn)年24歲，是一位學(xué)術(shù)成就卓越的斯坦福數(shù)學(xué)博士。她本科就讀于麻省理工學(xué)院，獲得數(shù)學(xué)和物理雙學(xué)位，隨后考取斯坦福大學(xué)數(shù)學(xué)博士，研究方向?yàn)閿?shù)論、組合學(xué)和概率學(xué)。在校期間，她的論文已發(fā)表在《美國(guó)數(shù)學(xué)會(huì)會(huì)報(bào)》、《拉馬努金期刊》等權(quán)威刊物，并于2021年獲得牛津大學(xué)羅德獎(jiǎng)學(xué)金，成為僅有的4名中國(guó)獲獎(jiǎng)?wù)咧弧?/p>

　　洪樂(lè)潼組建了一個(gè)超級(jí)團(tuán)隊(duì)，Axiom 的創(chuàng)始數(shù)學(xué)家肯·小野(Ken Ono)是古根海姆、帕卡德和斯隆獎(jiǎng)學(xué)者，曾任美國(guó)數(shù)學(xué)學(xué)會(huì)副主席，也是世界頂尖的拉馬努金數(shù)學(xué)權(quán)威之一。

　　Axiom 的首席技術(shù)官是前Facebook人工智能研究總監(jiān)舒博·森古普塔(Shubho Sengupta)，他曾幫助英偉達(dá)公司編寫了基礎(chǔ)性的圖形處理器庫(kù)。團(tuán)隊(duì)還包括弗朗索瓦·沙爾東(François Charton)，他因率先應(yīng)用Transformer模型解決了一個(gè)困擾專家130多年的數(shù)學(xué)難題而聞名。

　　Axiom 在去年10月已經(jīng)完成了6400萬(wàn)美元的種子輪融資，此后取得了顯著進(jìn)展。去年12月，其確定性人工智能在普特南數(shù)學(xué)競(jìng)賽(Putnam Competition)中取得了完美成績(jī)，該競(jìng)賽被數(shù)學(xué)家們認(rèn)為是世界上最具挑戰(zhàn)性的本科生數(shù)學(xué)考試。

　　Axiom 可驗(yàn)證地證明了一個(gè)已有20年歷史的數(shù)論猜想，該猜想涉及用于測(cè)量曲面距離的微積分元素。這是一個(gè)挑戰(zhàn)，肯·小野多年來(lái)屢次嘗試都未能解決。

　　對(duì)于人工智能的每一個(gè)輸出Axiom 都會(huì)生成一個(gè)由海量經(jīng)過(guò)驗(yàn)證的數(shù)據(jù)組成的“可信數(shù)據(jù)飛輪”。這些數(shù)據(jù)隨后被反饋回訓(xùn)練循環(huán)中，以增強(qiáng)其模型的能力，同時(shí)避免引入“模型崩潰”的風(fēng)險(xiǎn)。“模型崩潰”指的是數(shù)據(jù)污染給未經(jīng)驗(yàn)證的人工智能模型帶來(lái)的問(wèn)題。通過(guò)這種方式，Axiom 形成了一個(gè)遞歸的自我改進(jìn)循環(huán)。

　　研究公司Constellation Research的霍爾格·穆勒(Holger Mueller)表示，對(duì)于日益依賴“氛圍編碼”工具的開(kāi)發(fā)者來(lái)說(shuō)，一個(gè)能解決其風(fēng)險(xiǎn)的可行方案?jìng)涫茏放酢ＫJ(rèn)為，如果公理量化成功，將贏得大量擁躉。“大語(yǔ)言模型產(chǎn)生幻覺(jué)的風(fēng)險(xiǎn)并不‘可愛(ài)’;當(dāng)涉及到它們編寫的代碼時(shí)，這是完全錯(cuò)誤的，而且往往非常危險(xiǎn)，”該分析師說(shuō)。“Axiom 采取了正確的方法，利用數(shù)學(xué)來(lái)驗(yàn)證和核實(shí)人工智能生成的代碼是安全可靠的。”

　　此輪融資的領(lǐng)投方Menlo Ventures‌ 是一家成立于1976年的美國(guó)知名風(fēng)險(xiǎn)投資機(jī)構(gòu)，專注于對(duì)消費(fèi)科技和生命科學(xué)領(lǐng)域的早期至擴(kuò)張期初創(chuàng)企業(yè)進(jìn)行投資。

　　相關(guān)閱讀：

　　AI初創(chuàng)公司Axiom獲6400萬(wàn)美元種子輪投資，CEO：我們起點(diǎn)是AI數(shù)學(xué)家