"別擋在AI基礎模型廠商進化的路上做創(chuàng)業(yè)生意。"
OpenAI創(chuàng)始人山姆·奧爾特曼的這句話含金量還在上升。
其中一個原因是，在模型進化的路上，即使是在一個窄小的領(lǐng)域，實現(xiàn)AI的無幻覺性能，都是一項困難的任務，初創(chuàng)公司很難有資源與模型大廠抗衡。
一家名叫Harmonic的初創(chuàng)公司偏不信邪，其正試圖解決這個問題——開發(fā)完美無缺的零幻覺AI。
近日，這家公司推出了面向IOS和Android的聊天機器人應用程序測試版，普通用戶可以通過這款程序，訪問其人工智能模型Aristotle。其首席執(zhí)行官兼聯(lián)合創(chuàng)始人Tudor Achim表示，Aristotle是人類可以進行推理并正式驗證產(chǎn)出的第一款產(chǎn)品，在Aristotle支持的領(lǐng)域——定量推理，可以保證沒有幻覺。同時，Harmonic還表示計劃發(fā)布一個API，讓企業(yè)訪問Aristotle。在Harmonic的官網(wǎng)中宣稱，其正在Github上公開發(fā)布Aristotle的完整證明，由于其經(jīng)過正式驗證，無需人工檢查，這使得Aristotle在前沿人工智能模型中，處于高級數(shù)學推理性能的最前沿。
Harmonic在新產(chǎn)品的宣傳攻勢中表示，Aristotle在第 66 屆國際數(shù)學奧林匹克IMO2025中取得了金牌。這場比賽也被視為AI數(shù)學能力和AI推理能力的“成人禮”。
雖然這一成績也同樣被谷歌和OpenAI斬獲，但Harmonic認為這兩家大廠“并非通過形式化驗證手段取得結(jié)果”。從目前AI領(lǐng)域發(fā)展的整體來看，形式化（Formal）和非形式化（Informal）兩種路徑，到底哪種更有優(yōu)勢仍難以說清。
“如果從數(shù)學的角度，Scaling Law這條路跑到最后，一定會收斂。”一位頭部基金合伙人告訴虎嗅，即便已經(jīng)具備極高的行業(yè)地位，他仍然會每天閱讀最新的論文，尋找突破AI邊界的新的理論創(chuàng)新，這將是如今最具潛力和價值的地方。
也正因如此，Harmonic，這個成立僅兩年，專注解決AI邊界問題的初創(chuàng)企業(yè)，吸引了幾乎所有頂級投資機構(gòu)的目光，估值從零飆升到接近9億美元。
不久之前，它就像一塊磁石般吸引了近2億美元的投資——從紅杉資本到凱鵬華盈，從Index Ventures到Paradigm。這對于一家初創(chuàng)公司來說，都是一個不小的數(shù)字。
不過，針對基礎模型的技術(shù)創(chuàng)新和創(chuàng)業(yè)，從來是一項燒錢的生意，一位硅谷投資人表示，如今基于基礎模型的創(chuàng)業(yè)，早已是“富二代”的游戲，要么足夠天才，要么足夠有錢。
如果回溯Harmonic兩位創(chuàng)始人的經(jīng)歷，這兩個條件，Harmonic都具備。
我們試圖拆解這家在數(shù)學領(lǐng)域，和Open AI同臺競賽的初創(chuàng)公司，其背后的技術(shù)路線和厲害之處，回答Harmonic這將近9億美金的估值，憑什么？其究竟如何實現(xiàn)數(shù)學推理中的AI零幻覺？
Harmonic的兩位聯(lián)合創(chuàng)始人——Vlad Tenev和Tudor Achim背景獨特，一位在數(shù)學天賦上得天獨厚，而另一位則在AI領(lǐng)域積累了深厚的經(jīng)驗，還有一個關(guān)鍵因素是，Vlad Tenev很有錢。
左為Vlad Tenev，右為Tudor Achim
Vlad Tenev數(shù)學出身，他在斯坦福大學學數(shù)學，還曾在加州大學洛杉磯分校讀過數(shù)學碩士，甚至還師從數(shù)學大師陶哲軒。
后來他投身金融科技創(chuàng)業(yè)，創(chuàng)立并擔任Robinhood首席執(zhí)行官，如果要更形象地比喻，Robinhood，是一個用手機 App 把股票、期權(quán)、加密貨幣甚至 IPO 打新都變成零傭金、低門檻、游戲化交易的互聯(lián)網(wǎng)券商平臺。2021年，Robinhood在納斯達克上市，這家公司在Forbes 的實時估值已經(jīng)達到約 55 億美元。
Vlad Tenev的公司Robinhood的Forbes實時估值
這也是為何Harmonic和Vlad Tenev被稱為“美國版DeepSeek”和“梁文鋒”的原因，創(chuàng)始人資金非常雄厚，在最一開始可以以非常純粹的態(tài)度進行技術(shù)研究。Harmonic成立之初，用的一部分，就是Vlad Tenev的個人資金。
Tudor Achim則是計算機科學的專家，他從卡耐基梅隆大學計算機科學系畢業(yè)，后來在斯坦福讀博士，后來因為創(chuàng)業(yè)中途離開。
2016年，他和別人一起創(chuàng)立了自動駕駛公司Helm.ai并擔任技術(shù)總監(jiān)。在那里，他積累了豐富的AI算法開發(fā)經(jīng)驗，深知如何把AI技術(shù)應用到復雜的現(xiàn)實問題中。Helm.ai至今已經(jīng)融資1.02億美元，還得到了本田的支持。
Tudor Achim創(chuàng)立和自動駕駛公司的產(chǎn)品演示
兩位創(chuàng)始人有個共同理念，就是"讓AI會思考、講真話，不撒謊"。他們的想法可以歸納為四點，首先，AI必須說實話：AI的輸出必須經(jīng)過嚴格檢驗，確保結(jié)論準確無誤；其次，AI不能胡說八道，模型不能編造不存在的事實，寧可說"我不知道"也不要亂猜，通過嚴格的邏輯約束避免無根據(jù)的回答；第三，讓AI像科學家一樣思考：把假設-推理-驗證的科學方法植入AI，讓它能夠自動探索和證明新結(jié)論；第四，人機合作而非替代，Harmonic認為AI數(shù)學助手應該幫助人類，而不是讓用戶沒事可做。他們希望AI負責處理繁瑣的證明工作，人類負責提出有創(chuàng)意的想法。
正如他們在官網(wǎng)中寫道，驗證問題，是拓展人工智能工具效用的主要瓶頸，他們的使命是，探索人類理解的前沿。
Harmonic做了什么？
通用語言大模型的幻覺率長期居高不下，已成為制約其深入 AI下半場——“應用”的最大阻礙，也正因為如此，“幻覺”同時也是業(yè)界眼中的“最美的一塊肥肉”。哪家初創(chuàng)企業(yè)在這塊陣地將幻覺率限制到一個較低的水平，同時保持AI的智能水平，誰就能撬動更加龐大的市場。
比如，我們看到各類 AI 應用在 C 端紛紛強調(diào)“實用性”與“可交付性”，努力用工具鏈與插件系統(tǒng)來彌補模型輸出不穩(wěn)定的問題，但在追求極低容錯率的B端精密場景——像是金融建模、自動化編程、科學推理、法律合規(guī)等“不允許幻覺出現(xiàn)”的領(lǐng)域，通用大模型仍然舉步維艱。
2024年，Harmonic的當家產(chǎn)品誕生了，一個叫Aristotle（亞里士多德）的數(shù)學推理AI模型。
Aristotle的特別之處在于，它是個一站式數(shù)學AI：從理解普通話的數(shù)學問題，到生成嚴格的數(shù)學證明，再到用人話解釋答案，一個模型全包了。雖然還沒有關(guān)于Aristotle底層技術(shù)架構(gòu)的豐富信息，但Harmonic已經(jīng)通過官網(wǎng)公開了不少信息和成果。
主要解決了三個問題：
首先是幻覺問題。通用大模型經(jīng)常無中生有，編造不存在的內(nèi)容。Aristotle通過Lean證明這個"硬約束"徹底解決了這個問題：每一步推導都需要得到系統(tǒng)認可，不允許憑空編造。一旦模型想輸出錯誤結(jié)論，Lean立即報錯拒絕。
其次，推理過程不清楚。傳統(tǒng)AI即使能給出正確結(jié)論，推理步驟往往混亂或不完整。Aristotle通過詳細展示每一步推理來解決這個問題。由于有Lean檢查，整個推理鏈上的每個環(huán)節(jié)都必須邏輯清晰，讓最終證明既正確又透明。這就像給出了"答案的答案"——不僅告訴使用者結(jié)論，還展示如何一步步得到它。
最后，傳統(tǒng)大模型往往不夠嚴謹。普通AI對問題的回答可能對錯不分、過于自信，而Aristotle因為內(nèi)置了數(shù)學邏輯，回答風格更謹慎客觀。任何定理未經(jīng)證明就不能用于下一步推導，這種嚴謹性確保了Aristotle非常適合高風險場景（如金融模型檢查、醫(yī)療推理），因為它不會"差不多就下結(jié)論"。
2024年中，Harmonic宣布Aristotle在評估AI是否能讀懂、建模并證明數(shù)學題的一項測試集——MiniF2F中創(chuàng)下了新紀錄，領(lǐng)先了一眾大模型，這個測試集包含 488 道形式化數(shù)學題目，涵蓋數(shù)學核心領(lǐng)域（如代數(shù)、數(shù)論）。
比如，其官網(wǎng)展示了一道2001年國際數(shù)學奧林匹克的難題：給出題目和人類證明草稿后，Aristotle能自動生成完整的嚴格數(shù)學證明。這個例子顯示了Aristotle如何把人類的自然語言證明翻譯成機器能檢查的嚴格代碼。
來源：Harmonic官網(wǎng)
在最近，Harmonic最新推出的Chatbot式應用程序的一波宣傳攻勢中，兩位創(chuàng)始人聲稱 Aristotle做數(shù)學推理問題時給出的答案完全“無幻覺”。 此外，Harmonic還計劃發(fā)布一個to B的 API以讓企業(yè)可以訪問，以及一個面向消費者的網(wǎng)絡應用程序。
兩年估值接近9億美元
Harmonic自成立以來，就受到了投資界的熱烈追捧，短短兩年內(nèi)就完成了多輪大額融資。
從融資時機來看，Harmonic踩得很準， 2024年，OpenAI推出了新模型，雖然展現(xiàn)了一定的數(shù)學能力，但還是會犯錯，幻覺率仍居高不下。
這讓整個行業(yè)開始意識到"AI需要更嚴謹?shù)耐评砟芰?，正好給Harmonic這樣的公司創(chuàng)造了機會。
A輪融資時，投資方大多有學術(shù)或技術(shù)背景，他們看好Harmonic在學術(shù)上的突破。
進入2025年，AI行業(yè)競爭越來越激烈，各大公司都在搶著布局更強的多模態(tài)和推理AI。特別是DeepMind在2024年底推出的AlphaProof取得成功，更是引發(fā)了市場對"AI證明"這個領(lǐng)域的關(guān)注。
Harmonic在此時又適時開始融資B輪，正值整個行業(yè)尋求將AI從“能用”到“可用”的節(jié)點。
根據(jù)公開信息，Harmonic的種子階段由聯(lián)合創(chuàng)始人Vlad Tenev 個人和天使投資人提供啟動資金，主要用來組建團隊和開展基礎研究。
A輪融資在2024年9月完成，拿到7500萬美元，公司估值達到3.25億美元。B輪融資于2025年7月宣布，又融了1億美元，公司估值接近9億美元，離10億美元大關(guān)僅差一小步。
Harmonic的融資圖
Harmonic的投資人陣容相當亮眼，既有頂級硅谷投資機構(gòu)，也有行業(yè)基金和學術(shù)背景的資本，不僅有傳統(tǒng)的頂級風投，還有新興的科技基金。
例如其A輪由硅谷知名的紅杉資本（Sequoia Capital）領(lǐng)投，歐洲著名的Index Ventures緊跟其后。
同時，多家國際基金和知名個人也參與投資。B輪融資則由老牌投資機構(gòu)Kleiner Perkins領(lǐng)投，專注加密和前沿科技的Paradigm大手筆跟投。紅杉和Index作為老投資者繼續(xù)投錢，金融科技投資機構(gòu)Ribbit Capital新加入。此外，Quora聯(lián)合創(chuàng)始人查理·切沃（Charlie Cheever）也以個人身份參與了B輪。
一個叫做“Lean”的超級“數(shù)學監(jiān)理”
Harmonic究竟做了什么解決AI在數(shù)學推理上的瓶頸？
這要從數(shù)學界正在發(fā)生一些有趣的變化說起。
越來越多的數(shù)學家開始使用一種叫Lean的工具來寫數(shù)學證明，這是一個由微軟研究院開發(fā)的交互式定理證明系統(tǒng)，它能結(jié)合數(shù)學證明和編程的系統(tǒng)，能用代碼形式精確地表達并驗證復雜的數(shù)學理論，這成為了Harmonic的技術(shù)核心。
在Lean之前，大模型寫數(shù)學證明的時候，幻覺往往表現(xiàn)在，看起來似乎說得頭頭是道，但往往會出現(xiàn)中間某一步是“AI覺得對”。
Lean則相當于一個數(shù)字化的超級監(jiān)理和3D打印機器人。
每寫下一行代碼，它就立刻像監(jiān)理一樣，用激光尺、鋼筋掃描儀（形式化邏輯規(guī)則）分毫不差地檢查一遍。只要發(fā)現(xiàn)缺了一根釘子、少了一塊磚，它馬上紅燈報警，并要求返工。一旦全部綠燈，Lean 會把整個證明自動“3D 打印”出來——生成一個機器可檢驗、不可篡改的完整證明檔案。
Harmonic的產(chǎn)品，正是基于Lean的工具，以減少AI在數(shù)學上的幻覺。這條路線，需要大量已被人工標注或是驗證好的Lean的數(shù)據(jù)。Harmonic聲稱他們可以通過數(shù)據(jù)自動形式化的方式，解決人工和數(shù)據(jù)收集方面的問題。當然，這背后有極其復雜的技術(shù)建構(gòu)。
簡單理解就是，在數(shù)學里，一句簡單的“顯然成立”，在Lean的代碼邏輯下，可能要拆成50條邏輯規(guī)則，少一條都不行，就像是給樂高城堡補上每一塊1*1的小磚。每一條都要具備極強的準確性、細節(jié)性（保證每個逗號都有出處）和一致性，就像在給一篇維基百科做逐條公證。
至于Harmonic究竟用了什么技術(shù)細節(jié)，在可公開的信息中，獲取有限。一年前，模型Aristotle剛問世時，就有人質(zhì)疑道：無法在網(wǎng)站上找到任何ArXiv預印本論文得以證明他們的方法。
目前的公開信息幾乎只有融資和測試成績，很難找到技術(shù)細節(jié)、模型架構(gòu)或開放API信息。官方幾乎沒公開接口文檔、模型API或詳細的開發(fā)指南，技術(shù)社區(qū)也沒見到廣泛實測或開源樣例。
雖然他們強調(diào)未來將應用于軟件驗證、數(shù)學研究等，但目前沒有公眾可驗證的落地案例。對外能查到創(chuàng)始人背景和投資機構(gòu)，但在核心算法、工程團隊、研究人員、具體解決方案方面完全"閉口不談"。
即便在AI聊天機器人應用程序發(fā)布后，Harmonic 也仍然表示，目前不會發(fā)布Aristotle的其他基準測試結(jié)果，全程觀看直播過后的網(wǎng)友們也紛紛提出疑惑。
看起來，Harmonic所采取的零幻覺的方法，很難說是否真正突破了現(xiàn)有模型的能力，因為目前似乎并沒能證據(jù)證明其模型已經(jīng)完全沒有幻覺了，Harmonic通過直接生產(chǎn)Lean代碼的方式控制幻覺的產(chǎn)生，因此或許模型本身或許仍然存在幻覺，但因為幻覺錯誤的代碼會被Lean代碼檢查出來，予以排除，故而能夠使結(jié)果零幻覺。
Harmonic的對手都是“業(yè)界第一”
在這個用Lean 4技術(shù)生成完整數(shù)學證明，從根本上杜絕AI"瞎編亂造"的技術(shù)路線上，已經(jīng)聚集了不少實力強勁的競爭對手。
從官方數(shù)據(jù)來看，Aristotle的成績確實很亮眼。 在MiniF2F這個包含488道從高中到競賽級數(shù)學題的測試中，Aristotle表現(xiàn)相當出色：2024年6月左右，它的成功率達到83%（可以用計算器等工具輔助）；僅僅一個月后，成功率就提升到了90%，創(chuàng)下了當時的新紀錄。
2024年6月，Harmonic放出來的信息展現(xiàn)其測試水平
作為對比，之前那些最SOTA的模型（比如OpenAI的GPT-4）在同樣條件下的成功率大約只有20-35%，Aristotle實現(xiàn)了幾倍的跨越。這說明Aristotle的數(shù)學解題能力已經(jīng)遠超普通的AI模型。
不過話說回來，現(xiàn)在那些SOTA模型的文采、想象力很大程度上都依靠"適度的幻覺"，拿一個專門做數(shù)學的模型和通用AI比較，似乎有點"不太公平"。
并且，在讓AI零幻覺的領(lǐng)域，有錢有技術(shù)還努力的“富二代”并不只有Harmonic一家。
DeepSeek在兩個月前發(fā)布了Prover-V2模型，在MiniF2F測試中達到了88.9%的通過率，在其他數(shù)學競賽上也有不錯的表現(xiàn)。
技術(shù)架構(gòu)上，DeepSeek Prover先用DeepSeek-V3把復雜問題拆解成一堆小目標，每解決一個小目標就把這些證明串成"思維鏈"，然后用這些數(shù)據(jù)來訓練模型。
除了MiniF2F，PutnamBench評測集中收集了640道Putnam數(shù)學競賽題，代表了本科生高難度數(shù)學題，對AI來說極具挑戰(zhàn)性。最終，DeepSeek-Prover-V2在這658道題中成功解決了49道，也算是不錯的成績。
谷歌DeepMind也是這個賽道的老手，其走的技術(shù)路線和Harmonic類似，谷歌DeepMind的Alphaproof，它在2024年可謂是數(shù)學AI領(lǐng)域的超級明星，賺足了眼球。它的成名之戰(zhàn)就是2024年的國際數(shù)學奧林匹克競賽（IMO）的測試得分。
DeepMind團隊的AlphaProof和AlphaGeometry 2在這場比賽中拿到了銀牌成績——六道題解出了四道，這是一個里程碑式的存在。
《紐約時報》甚至用"數(shù)學家們讓路，AlphaProof來了"這樣的標題來突出它的重要性。
AlphaProof的工作原理是，一個用Lean語言來證明數(shù)學結(jié)論的"自我訓練"系統(tǒng)，結(jié)合了預訓練語言模型和AlphaZero強化學習算法。Lean這種形式化語言的最大優(yōu)勢是能夠嚴格驗證數(shù)學推理的正確性。在此之前，這種方法在機器學習中用得不多，因為人工編寫的數(shù)據(jù)太少了。相比之下，基于自然語言的方法雖然可以使用更多數(shù)據(jù)，但經(jīng)常會產(chǎn)生看起來合理實際上錯誤的推理步驟。
DeepMind當然也意識到這個問題，他們的做法是，通過調(diào)整Gemini模型，讓它自動把自然語言的數(shù)學題翻譯成形式化語言，在這兩個領(lǐng)域之間架起了一座橋梁，從而建立了一個包含各種難度數(shù)學題的大型題庫。
就在前幾天，OpenAI研究科學家Alex Wei在X上發(fā)布推文，稱一種全新的神秘推理模型斬獲了IMO2025年金牌，6道題解出了5道。值得注意的是，該模型是在沒有任何工具或網(wǎng)絡輔助的狀態(tài)下，自行閱讀題目并撰寫自然語言證明的。
結(jié)語
盡管在解決AI幻覺上，技術(shù)尚未收斂，但對于剛發(fā)布產(chǎn)品和融資后的Harmonic來說，這場與時間的賽跑正式開始了。
與Harmonic不同的是，這些基礎模型大廠有自己多年的模型和海量數(shù)據(jù)作為基礎，比如DeepSeek的Prover系列，直接讓自家的DeepSeek-V3當"教學者"，先教它學會怎么把復雜問題拆解成簡單步驟，再用這些經(jīng)驗去訓練專門的數(shù)學推理模型。谷歌的AlphaProof 背后有Gemini模型幫忙把日常語言翻譯成數(shù)學證明語言。
相比之下，Harmonic公司的Aristotle 并沒有像DeepSeek和谷歌那樣擁有完整的大模型"生態(tài)圈"做后盾。
但這也許是硅谷創(chuàng)新的獨特所在——收購的文化以及良好的投資退出環(huán)境，Harmonic的目標可能并非IPO一條路走到黑，他們可以在擁有足夠技術(shù)積累和實力時，選擇一條被大廠收購的路線，成為這些基礎模型廠商技術(shù)生態(tài)中的一環(huán)，對于Harmonic與其投資者來說，也是一個不錯的選擇。