新智元報(bào)道

編輯：傾傾

【新智元導(dǎo)讀】2億美元A輪融資，估值110億，成立僅一年就成為獨(dú)角獸。更震撼的是創(chuàng)始人——25歲的廣州00后洪樂潼，父母是從未上過大學(xué)的普通務(wù)工者。她用數(shù)學(xué)解決AI最大的痛點(diǎn)：讓模型推理步步可驗(yàn)證，徹底杜絕幻覺。為了加入她，弗吉尼亞大學(xué)終身教授直接辭職。

就在上周，全球創(chuàng)投圈被一個(gè)名字刷屏了。

AI初創(chuàng)公司Axiom宣布完成2億美元A輪融資，由硅谷頂級(jí)風(fēng)投Menlo Ventures領(lǐng)投，Greycroft、Madrona Venture、B Capital、Toyota Ventures等老股東全部跟投。公司估值飆升至16億美元。

成立不到一年，直接躋身獨(dú)角獸。

但更讓人震撼的，是這家公司的創(chuàng)始人——25歲的洪樂潼（Carina Hong）。

她讓大模型的推理過程像數(shù)學(xué)證明一樣嚴(yán)格，每一步都可驗(yàn)證。

17歲進(jìn)MIT，3年修完雙學(xué)位

洪樂潼祖籍潮汕，出生在廣州，父母是普通務(wù)工者，但她從小就展現(xiàn)出極其罕見的數(shù)學(xué)天賦。

高一時(shí)，她入選廣東省中學(xué)生英才計(jì)劃，師從中山大學(xué)教授王學(xué)欽。

隨后，她在全國中學(xué)生數(shù)學(xué)奧林匹克（CMO）廣東選拔中脫穎而出，成為僅有的四位女生之一。

2018年，17歲的洪樂潼被麻省理工學(xué)院（MIT）錄取，選擇了數(shù)學(xué)與物理雙專業(yè)。

接下來的履歷，堪稱「開掛」。

她在MIT只用3年就修完兩個(gè)學(xué)位，本科期間發(fā)表了9篇學(xué)術(shù)論文，研究方向涵蓋模橢圓曲線、K3曲面上的L函數(shù)、「月光猜想」等基礎(chǔ)數(shù)學(xué)領(lǐng)域。

她曾獲得全美女性數(shù)學(xué)家最高榮譽(yù)——Alice T. Schafer數(shù)學(xué)獎(jiǎng)，以及表彰北美數(shù)學(xué)專業(yè)本科生杰出研究的AMS-MAA-SIAM摩根獎(jiǎng) 。

2021年，洪樂潼獲得牛津大學(xué)羅德獎(jiǎng)學(xué)金，成為當(dāng)年僅有的四位中國獲獎(jiǎng)?wù)咧弧?/p>

羅德獎(jiǎng)學(xué)金被譽(yù)為「本科諾貝爾獎(jiǎng)」，是世界上歷史最悠久、最負(fù)盛名的國際獎(jiǎng)學(xué)金項(xiàng)目。

在牛津攻讀神經(jīng)科學(xué)碩士期間，她在倫敦大學(xué)學(xué)院蓋茨比計(jì)算單位作為第一作者開展深度學(xué)習(xí)研究，正式踏入AI領(lǐng)域。

隨后她又進(jìn)入斯坦福大學(xué)，攻讀數(shù)學(xué)與法律雙學(xué)科博士。

但博士還沒讀完，她就退學(xué)了。

AI的致命缺陷：概率模型沒有「絕對(duì)正確」

洪樂潼看到的，是AI行業(yè)最尖銳的矛盾。

大模型的能力在狂飆，但可靠性始終是個(gè)黑盒。

日常應(yīng)用中的胡說八道或許無傷大雅，但在金融、國防、關(guān)鍵基礎(chǔ)設(shè)施領(lǐng)域，任何基于概率的錯(cuò)誤都可能釀成災(zāi)難。

去年針對(duì)ChatGPT o3「數(shù)學(xué)測試作弊」?fàn)幾h，作為斯坦福數(shù)學(xué)博士的洪樂潼率先指出癥結(jié)：當(dāng)前AI缺乏嚴(yán)格的邏輯推理訓(xùn)練體系。

現(xiàn)有的大模型本質(zhì)上是概率機(jī)器。它們通過海量數(shù)據(jù)學(xué)習(xí)模式，然后基于統(tǒng)計(jì)規(guī)律給出答案。

即使是GPT-4、Claude這樣的頂級(jí)模型，其概率性的本質(zhì)依然是主要的擔(dān)憂原因。

洪樂潼的答案是：讓AI像數(shù)學(xué)家一樣工作。

她創(chuàng)立的Axiom采用「數(shù)學(xué)即服務(wù)」模式，通過訓(xùn)練AI系統(tǒng)生成用Lean語言編寫的、經(jīng)過形式化驗(yàn)證的輸出。

Lean是一種專為數(shù)學(xué)證明設(shè)計(jì)的編程語言，通過使用Lean，Axiom可以確保AI模型推理過程的每一步都是可機(jī)器檢查的并且在邏輯上得到保證。

傳統(tǒng)大模型給你一個(gè)答案，你只能信或不信。而Axiom的系統(tǒng)給你一個(gè)答案，同時(shí)附帶一個(gè)完整的、可驗(yàn)證的證明過程，不存在大概是對(duì)的這種模糊地帶。

洪樂潼在接受采訪時(shí)說：

科學(xué)突破往往需要兩步：提出假設(shè)，再用證明去驗(yàn)證。我們創(chuàng)立Axiom，就是要無限壓縮把好奇心轉(zhuǎn)化為真理的時(shí)間。

滿分通過普特南競賽，攻克20年數(shù)論猜想

去年12月，Axiom交出了第一張成績單。

Axiom的核心系統(tǒng)在普特南競賽中，斬獲滿分，12題全對(duì)。

普特南競賽是北美地區(qū)最負(fù)盛名的大學(xué)生數(shù)學(xué)競賽，成績的中位數(shù)常常為零（滿分120分）。

過去近百年，僅有5人達(dá)成過滿分成就。Axiom的AI做到了。

更震撼的還在后面。Axiom可驗(yàn)證地證明了一個(gè)已有20年歷史的數(shù)論猜想，該猜想涉及用于測量曲面距離的微積分元素。

這個(gè)問題，連Axiom的創(chuàng)始數(shù)學(xué)家Ken Ono都曾多年嘗試未能解決。

去年12月，Axiom開發(fā)的AxiomProver系統(tǒng)，使用可驗(yàn)證的Lean語言，完成了埃爾德什問題集中第124題和第481題的形式化證明，分別用時(shí)1天和5小時(shí)，全程無人為干預(yù)。

埃爾德什問題集共包含1109個(gè)關(guān)于組合數(shù)學(xué)和數(shù)論的問題，是匈牙利數(shù)學(xué)家保羅·埃爾德什數(shù)十年來論文的匯集。

迄今為止，只有266個(gè)問題被證明，其中僅10個(gè)問題的證明被轉(zhuǎn)化為計(jì)算機(jī)可驗(yàn)證的形式化版本。

解決數(shù)學(xué)問題只是冰山一角。Axiom正在將這種「絕對(duì)正確」的數(shù)學(xué)推理能力，通過遷移學(xué)習(xí)引入到代碼驗(yàn)證領(lǐng)域，試圖解決生成式AI的種種問題。

目標(biāo)客戶是對(duì)沖基金、量化交易員等高端場景。這些地方，容不得半點(diǎn)「大概對(duì)」。

終身教授辭職加入，只因「見證了數(shù)學(xué)超級(jí)智能的可能」

Axiom最震撼的一次招聘，發(fā)生在去年12月。

Ken Ono（小野?。?，弗吉尼亞大學(xué)Marvin Rosenblum講席教授、前美國數(shù)學(xué)學(xué)會(huì)副主席，辭去終身教職，全職加入Axiom擔(dān)任創(chuàng)始數(shù)學(xué)家。

他是古根海姆獎(jiǎng)、帕卡德獎(jiǎng)、斯隆獎(jiǎng)得主，世界頂尖的拉馬努金數(shù)學(xué)權(quán)威之一 ，還是電影《知無涯者》的副制片人和數(shù)學(xué)顧問，甚至出演過百威啤酒的超級(jí)碗廣告。

并且，他也是唯一一位出演過啤酒廣告的數(shù)論學(xué)家。

在Ken Ono長達(dá)四十年的執(zhí)教生涯中，曾指導(dǎo)過十位摩根獎(jiǎng)得主，洪樂潼正是其中之一。

為什么一個(gè)功成名就的終身教授，會(huì)放棄穩(wěn)定的學(xué)術(shù)生涯，去為一個(gè)25歲的年輕人工作？

華爾街日報(bào)報(bào)道稱，Ken Ono在人工智能徹底改變他的職業(yè)生涯和生活之前，一直對(duì)人工智能持懷疑態(tài)度。

直到最近，他開始談?wù)撊斯ぶ悄軙r(shí)，還總是嘲諷圍繞這項(xiàng)新興技術(shù)的炒作 。

但見到Axiom的系統(tǒng)后，他頓悟了。

除了Ken Ono，Axiom的團(tuán)隊(duì)堪稱「夢之隊(duì)」：

CTO Shubho Sengupta曾任Meta AI研究總監(jiān)，此前參與過Google分布式訓(xùn)練系統(tǒng)的研究工作，也是最早開發(fā)CUDA技術(shù)的專家之一 ；

核心科學(xué)家Fran?ois Charton，是率先將Transformer模型引入數(shù)學(xué)領(lǐng)域的先驅(qū)，曾用大模型推翻過一個(gè)長達(dá)30年未解的學(xué)術(shù)猜想。

一位投資人忍不住感慨：

她兼具深厚的數(shù)學(xué)功底、驚人的運(yùn)營效率，以及吸引世界一流人才的能力。這是我過去二十年的硅谷生涯中，見過的最令人印象深刻的創(chuàng)始人，沒有之一。

目前，Axiom擁有30多名員工，招聘速度還在不斷加快。

00后集體登場，AI創(chuàng)業(yè)進(jìn)入「理想主義者」時(shí)代

就在上周，成立僅一年多的公司靈初智能宣布完成天使輪及Pre-A輪共計(jì)20億元融資。

其聯(lián)合創(chuàng)始人陳源培，出生于2001年，曾就讀于北京大學(xué)、斯坦福大學(xué)，師從李飛飛。

同為00后的楊豐瑜在耶魯博士畢業(yè)后選擇回國創(chuàng)業(yè)，2024年成立了具身智能公司優(yōu)理奇，完成數(shù)億元的天使輪及天使+輪融資。

2025年，由三位00后創(chuàng)立的AI招聘網(wǎng)站Mercor也宣布完成1億美元的B輪融資，公司估值達(dá)20億美元。

這一代創(chuàng)業(yè)者，和上一代有什么不同？

曾在DeepSeek火爆全球之際，洪樂潼發(fā)出這樣的感慨：

一個(gè)小而專注、特立獨(dú)行的團(tuán)隊(duì)。一群理想主義者組成的優(yōu)秀合作伙伴。他們執(zhí)行力強(qiáng)，親力親為。最珍貴的，是那份理想與使命交織的信念。這就是DeepSeek的故事，也是我想親自書寫的故事。

有投資人私下交流時(shí)回憶，洪樂潼在創(chuàng)立Axiom期間于朋友圈寫下的自勉：

祝自己做花也做樹。繽紛熱情，孤離兀立。

談話間，她幾乎不談?wù)擄L(fēng)口與顛覆，更多在意對(duì)問題本身的好奇和對(duì)技術(shù)可能性的清晰判斷。

對(duì)于Axiom的終極使命，洪樂潼留下了一句極具張力的注腳：

Verified AI關(guān)注的，絕不僅僅是修補(bǔ)AI的缺點(diǎn)。真正瞄準(zhǔn)的，是AI的上限，是通向超級(jí)智能的階梯。

從廣州普通家庭走出的女孩，到掌舵估值110億的AI獨(dú)角獸。

從MIT的數(shù)學(xué)天才，到讓終身教授辭職追隨的創(chuàng)業(yè)者。

洪樂潼和她這一代00后創(chuàng)業(yè)者的故事，正在改寫硅谷的敘事規(guī)則：不是為了風(fēng)口而創(chuàng)業(yè)，而是為了解決真正困難的技術(shù)問題。

AI的上限在哪里？或許答案就藏在這群25歲年輕人的選擇里。

參考資料：

https://mp.weixin.qq.com/s/msJXxZMSyfXMXDPMCdtznQ