"別擋在AI基礎(chǔ)模型廠商進(jìn)化的路上做創(chuàng)業(yè)生意。"

OpenAI創(chuàng)始人山姆·奧爾特曼的這句話含金量還在上升。

其中一個(gè)原因是，在模型進(jìn)化的路上，即使是在一個(gè)窄小的領(lǐng)域，實(shí)現(xiàn)AI的無(wú)幻覺(jué)性能，都是一項(xiàng)困難的任務(wù)，初創(chuàng)公司很難有資源與模型大廠抗衡。

一家名叫Harmonic的初創(chuàng)公司偏不信邪，其正試圖解決這個(gè)問(wèn)題——開(kāi)發(fā)完美無(wú)缺的零幻覺(jué)AI。

近日，這家公司推出了面向IOS和Android的聊天機(jī)器人應(yīng)用程序測(cè)試版，普通用戶可以通過(guò)這款程序，訪問(wèn)其人工智能模型Aristotle。其首席執(zhí)行官兼聯(lián)合創(chuàng)始人Tudor Achim表示，Aristotle是人類可以進(jìn)行推理并正式驗(yàn)證產(chǎn)出的第一款產(chǎn)品，在Aristotle支持的領(lǐng)域——定量推理，可以保證沒(méi)有幻覺(jué)。同時(shí)，Harmonic還表示計(jì)劃發(fā)布一個(gè)API，讓企業(yè)訪問(wèn)Aristotle。在Harmonic的官網(wǎng)中宣稱，其正在Github上公開(kāi)發(fā)布Aristotle的完整證明，由于其經(jīng)過(guò)正式驗(yàn)證，無(wú)需人工檢查，這使得Aristotle在前沿人工智能模型中，處于高級(jí)數(shù)學(xué)推理性能的最前沿。

Harmonic在新產(chǎn)品的宣傳攻勢(shì)中表示，Aristotle在第 66 屆國(guó)際數(shù)學(xué)奧林匹克IMO2025中取得了金牌。這場(chǎng)比賽也被視為AI數(shù)學(xué)能力和AI推理能力的“成人禮”。

雖然這一成績(jī)也同樣被谷歌和OpenAI斬獲，但Harmonic認(rèn)為這兩家大廠“并非通過(guò)形式化驗(yàn)證手段取得結(jié)果”。從目前AI領(lǐng)域發(fā)展的整體來(lái)看，形式化（Formal）和非形式化（Informal）兩種路徑，到底哪種更有優(yōu)勢(shì)仍難以說(shuō)清。

“如果從數(shù)學(xué)的角度，Scaling Law這條路跑到最后，一定會(huì)收斂。”一位頭部基金合伙人告訴虎嗅，即便已經(jīng)具備極高的行業(yè)地位，他仍然會(huì)每天閱讀最新的論文，尋找突破AI邊界的新的理論創(chuàng)新，這將是如今最具潛力和價(jià)值的地方。

也正因如此，Harmonic，這個(gè)成立僅兩年，專注解決AI邊界問(wèn)題的初創(chuàng)企業(yè)，吸引了幾乎所有頂級(jí)投資機(jī)構(gòu)的目光，估值從零飆升到接近9億美元。

不久之前，它就像一塊磁石般吸引了近2億美元的投資——從紅杉資本到凱鵬華盈，從Index Ventures到Paradigm。這對(duì)于一家初創(chuàng)公司來(lái)說(shuō)，都是一個(gè)不小的數(shù)字。

不過(guò)，針對(duì)基礎(chǔ)模型的技術(shù)創(chuàng)新和創(chuàng)業(yè)，從來(lái)是一項(xiàng)燒錢的生意，一位硅谷投資人表示，如今基于基礎(chǔ)模型的創(chuàng)業(yè)，早已是“富二代”的游戲，要么足夠天才，要么足夠有錢。

如果回溯Harmonic兩位創(chuàng)始人的經(jīng)歷，這兩個(gè)條件，Harmonic都具備。

我們?cè)噲D拆解這家在數(shù)學(xué)領(lǐng)域，和Open AI同臺(tái)競(jìng)賽的初創(chuàng)公司，其背后的技術(shù)路線和厲害之處，回答Harmonic這將近9億美金的估值，憑什么？其究竟如何實(shí)現(xiàn)數(shù)學(xué)推理中的AI零幻覺(jué)？

Harmonic的兩位聯(lián)合創(chuàng)始人——Vlad Tenev和Tudor Achim背景獨(dú)特，一位在數(shù)學(xué)天賦上得天獨(dú)厚，而另一位則在AI領(lǐng)域積累了深厚的經(jīng)驗(yàn)，還有一個(gè)關(guān)鍵因素是，Vlad Tenev很有錢。

左為Vlad Tenev，右為Tudor Achim

Vlad Tenev數(shù)學(xué)出身，他在斯坦福大學(xué)學(xué)數(shù)學(xué)，還曾在加州大學(xué)洛杉磯分校讀過(guò)數(shù)學(xué)碩士，甚至還師從數(shù)學(xué)大師陶哲軒。

后來(lái)他投身金融科技創(chuàng)業(yè)，創(chuàng)立并擔(dān)任Robinhood首席執(zhí)行官，如果要更形象地比喻，Robinhood，是一個(gè)用手機(jī) App 把股票、期權(quán)、加密貨幣甚至 IPO 打新都變成零傭金、低門檻、游戲化交易的互聯(lián)網(wǎng)券商平臺(tái)。2021年，Robinhood在納斯達(dá)克上市，這家公司在Forbes 的實(shí)時(shí)估值已經(jīng)達(dá)到約 55 億美元。

Vlad Tenev的公司Robinhood的Forbes實(shí)時(shí)估值

這也是為何Harmonic和Vlad Tenev被稱為“美國(guó)版DeepSeek”和“梁文鋒”的原因，創(chuàng)始人資金非常雄厚，在最一開(kāi)始可以以非常純粹的態(tài)度進(jìn)行技術(shù)研究。Harmonic成立之初，用的一部分，就是Vlad Tenev的個(gè)人資金。

Tudor Achim則是計(jì)算機(jī)科學(xué)的專家，他從卡耐基梅隆大學(xué)計(jì)算機(jī)科學(xué)系畢業(yè)，后來(lái)在斯坦福讀博士，后來(lái)因?yàn)閯?chuàng)業(yè)中途離開(kāi)。

2016年，他和別人一起創(chuàng)立了自動(dòng)駕駛公司Helm.ai并擔(dān)任技術(shù)總監(jiān)。在那里，他積累了豐富的AI算法開(kāi)發(fā)經(jīng)驗(yàn)，深知如何把AI技術(shù)應(yīng)用到復(fù)雜的現(xiàn)實(shí)問(wèn)題中。Helm.ai至今已經(jīng)融資1.02億美元，還得到了本田的支持。

Tudor Achim創(chuàng)立和自動(dòng)駕駛公司的產(chǎn)品演示

兩位創(chuàng)始人有個(gè)共同理念，就是"讓AI會(huì)思考、講真話，不撒謊"。他們的想法可以歸納為四點(diǎn)，首先，AI必須說(shuō)實(shí)話：AI的輸出必須經(jīng)過(guò)嚴(yán)格檢驗(yàn)，確保結(jié)論準(zhǔn)確無(wú)誤；其次，AI不能胡說(shuō)八道，模型不能編造不存在的事實(shí)，寧可說(shuō)"我不知道"也不要亂猜，通過(guò)嚴(yán)格的邏輯約束避免無(wú)根據(jù)的回答；第三，讓AI像科學(xué)家一樣思考：把假設(shè)-推理-驗(yàn)證的科學(xué)方法植入AI，讓它能夠自動(dòng)探索和證明新結(jié)論；第四，人機(jī)合作而非替代，Harmonic認(rèn)為AI數(shù)學(xué)助手應(yīng)該幫助人類，而不是讓用戶沒(méi)事可做。他們希望AI負(fù)責(zé)處理繁瑣的證明工作，人類負(fù)責(zé)提出有創(chuàng)意的想法。

正如他們?cè)诠倬W(wǎng)中寫道，驗(yàn)證問(wèn)題，是拓展人工智能工具效用的主要瓶頸，他們的使命是，探索人類理解的前沿。

Harmonic做了什么？

通用語(yǔ)言大模型的幻覺(jué)率長(zhǎng)期居高不下，已成為制約其深入 AI下半場(chǎng)——“應(yīng)用”的最大阻礙，也正因?yàn)槿绱耍?ldquo;幻覺(jué)”同時(shí)也是業(yè)界眼中的“最美的一塊肥肉”。哪家初創(chuàng)企業(yè)在這塊陣地將幻覺(jué)率限制到一個(gè)較低的水平，同時(shí)保持AI的智能水平，誰(shuí)就能撬動(dòng)更加龐大的市場(chǎng)。

比如，我們看到各類 AI 應(yīng)用在 C 端紛紛強(qiáng)調(diào)“實(shí)用性”與“可交付性”，努力用工具鏈與插件系統(tǒng)來(lái)彌補(bǔ)模型輸出不穩(wěn)定的問(wèn)題，但在追求極低容錯(cuò)率的B端精密場(chǎng)景——像是金融建模、自動(dòng)化編程、科學(xué)推理、法律合規(guī)等“不允許幻覺(jué)出現(xiàn)”的領(lǐng)域，通用大模型仍然舉步維艱。

2024年，Harmonic的當(dāng)家產(chǎn)品誕生了，一個(gè)叫Aristotle（亞里士多德）的數(shù)學(xué)推理AI模型。

Aristotle的特別之處在于，它是個(gè)一站式數(shù)學(xué)AI：從理解普通話的數(shù)學(xué)問(wèn)題，到生成嚴(yán)格的數(shù)學(xué)證明，再到用人話解釋答案，一個(gè)模型全包了。雖然還沒(méi)有關(guān)于Aristotle底層技術(shù)架構(gòu)的豐富信息，但Harmonic已經(jīng)通過(guò)官網(wǎng)公開(kāi)了不少信息和成果。

主要解決了三個(gè)問(wèn)題：

首先是幻覺(jué)問(wèn)題。通用大模型經(jīng)常無(wú)中生有，編造不存在的內(nèi)容。Aristotle通過(guò)Lean證明這個(gè)"硬約束"徹底解決了這個(gè)問(wèn)題：每一步推導(dǎo)都需要得到系統(tǒng)認(rèn)可，不允許憑空編造。一旦模型想輸出錯(cuò)誤結(jié)論，Lean立即報(bào)錯(cuò)拒絕。

其次，推理過(guò)程不清楚。傳統(tǒng)AI即使能給出正確結(jié)論，推理步驟往往混亂或不完整。Aristotle通過(guò)詳細(xì)展示每一步推理來(lái)解決這個(gè)問(wèn)題。由于有Lean檢查，整個(gè)推理鏈上的每個(gè)環(huán)節(jié)都必須邏輯清晰，讓最終證明既正確又透明。這就像給出了"答案的答案"——不僅告訴使用者結(jié)論，還展示如何一步步得到它。

最后，傳統(tǒng)大模型往往不夠嚴(yán)謹(jǐn)。普通AI對(duì)問(wèn)題的回答可能對(duì)錯(cuò)不分、過(guò)于自信，而Aristotle因?yàn)閮?nèi)置了數(shù)學(xué)邏輯，回答風(fēng)格更謹(jǐn)慎客觀。任何定理未經(jīng)證明就不能用于下一步推導(dǎo)，這種嚴(yán)謹(jǐn)性確保了Aristotle非常適合高風(fēng)險(xiǎn)場(chǎng)景（如金融模型檢查、醫(yī)療推理），因?yàn)樗粫?huì)"差不多就下結(jié)論"。

2024年中，Harmonic宣布Aristotle在評(píng)估AI是否能讀懂、建模并證明數(shù)學(xué)題的一項(xiàng)測(cè)試集——MiniF2F中創(chuàng)下了新紀(jì)錄，領(lǐng)先了一眾大模型，這個(gè)測(cè)試集包含 488 道形式化數(shù)學(xué)題目，涵蓋數(shù)學(xué)核心領(lǐng)域（如代數(shù)、數(shù)論）。

比如，其官網(wǎng)展示了一道2001年國(guó)際數(shù)學(xué)奧林匹克的難題：給出題目和人類證明草稿后，Aristotle能自動(dòng)生成完整的嚴(yán)格數(shù)學(xué)證明。這個(gè)例子顯示了Aristotle如何把人類的自然語(yǔ)言證明翻譯成機(jī)器能檢查的嚴(yán)格代碼。

來(lái)源：Harmonic官網(wǎng)

在最近，Harmonic最新推出的Chatbot式應(yīng)用程序的一波宣傳攻勢(shì)中，兩位創(chuàng)始人聲稱 Aristotle做數(shù)學(xué)推理問(wèn)題時(shí)給出的答案完全“無(wú)幻覺(jué)”。 此外，Harmonic還計(jì)劃發(fā)布一個(gè)to B的 API以讓企業(yè)可以訪問(wèn)，以及一個(gè)面向消費(fèi)者的網(wǎng)絡(luò)應(yīng)用程序。

兩年估值接近9億美元

Harmonic自成立以來(lái)，就受到了投資界的熱烈追捧，短短兩年內(nèi)就完成了多輪大額融資。

從融資時(shí)機(jī)來(lái)看，Harmonic踩得很準(zhǔn)， 2024年，OpenAI推出了新模型，雖然展現(xiàn)了一定的數(shù)學(xué)能力，但還是會(huì)犯錯(cuò)，幻覺(jué)率仍居高不下。

這讓整個(gè)行業(yè)開(kāi)始意識(shí)到"AI需要更嚴(yán)謹(jǐn)?shù)耐评砟芰?，正好給Harmonic這樣的公司創(chuàng)造了機(jī)會(huì)。

A輪融資時(shí)，投資方大多有學(xué)術(shù)或技術(shù)背景，他們看好Harmonic在學(xué)術(shù)上的突破。

進(jìn)入2025年，AI行業(yè)競(jìng)爭(zhēng)越來(lái)越激烈，各大公司都在搶著布局更強(qiáng)的多模態(tài)和推理AI。特別是DeepMind在2024年底推出的AlphaProof取得成功，更是引發(fā)了市場(chǎng)對(duì)"AI證明"這個(gè)領(lǐng)域的關(guān)注。

Harmonic在此時(shí)又適時(shí)開(kāi)始融資B輪，正值整個(gè)行業(yè)尋求將AI從“能用”到“可用”的節(jié)點(diǎn)。

根據(jù)公開(kāi)信息，Harmonic的種子階段由聯(lián)合創(chuàng)始人Vlad Tenev 個(gè)人和天使投資人提供啟動(dòng)資金，主要用來(lái)組建團(tuán)隊(duì)和開(kāi)展基礎(chǔ)研究。

A輪融資在2024年9月完成，拿到7500萬(wàn)美元，公司估值達(dá)到3.25億美元。B輪融資于2025年7月宣布，又融了1億美元，公司估值接近9億美元，離10億美元大關(guān)僅差一小步。

Harmonic的融資圖

Harmonic的投資人陣容相當(dāng)亮眼，既有頂級(jí)硅谷投資機(jī)構(gòu)，也有行業(yè)基金和學(xué)術(shù)背景的資本，不僅有傳統(tǒng)的頂級(jí)風(fēng)投，還有新興的科技基金。

例如其A輪由硅谷知名的紅杉資本（Sequoia Capital）領(lǐng)投，歐洲著名的Index Ventures緊跟其后。

同時(shí)，多家國(guó)際基金和知名個(gè)人也參與投資。B輪融資則由老牌投資機(jī)構(gòu)Kleiner Perkins領(lǐng)投，專注加密和前沿科技的Paradigm大手筆跟投。紅杉和Index作為老投資者繼續(xù)投錢，金融科技投資機(jī)構(gòu)Ribbit Capital新加入。此外，Quora聯(lián)合創(chuàng)始人查理·切沃（Charlie Cheever）也以個(gè)人身份參與了B輪。

一個(gè)叫做“Lean”的超級(jí)“數(shù)學(xué)監(jiān)理”

Harmonic究竟做了什么解決AI在數(shù)學(xué)推理上的瓶頸？

這要從數(shù)學(xué)界正在發(fā)生一些有趣的變化說(shuō)起。

越來(lái)越多的數(shù)學(xué)家開(kāi)始使用一種叫Lean的工具來(lái)寫數(shù)學(xué)證明，這是一個(gè)由微軟研究院開(kāi)發(fā)的交互式定理證明系統(tǒng)，它能結(jié)合數(shù)學(xué)證明和編程的系統(tǒng)，能用代碼形式精確地表達(dá)并驗(yàn)證復(fù)雜的數(shù)學(xué)理論，這成為了Harmonic的技術(shù)核心。

在Lean之前，大模型寫數(shù)學(xué)證明的時(shí)候，幻覺(jué)往往表現(xiàn)在，看起來(lái)似乎說(shuō)得頭頭是道，但往往會(huì)出現(xiàn)中間某一步是“AI覺(jué)得對(duì)”。

Lean則相當(dāng)于一個(gè)數(shù)字化的超級(jí)監(jiān)理和3D打印機(jī)器人。

每寫下一行代碼，它就立刻像監(jiān)理一樣，用激光尺、鋼筋掃描儀（形式化邏輯規(guī)則）分毫不差地檢查一遍。只要發(fā)現(xiàn)缺了一根釘子、少了一塊磚，它馬上紅燈報(bào)警，并要求返工。一旦全部綠燈，Lean 會(huì)把整個(gè)證明自動(dòng)“3D 打印”出來(lái)——生成一個(gè)機(jī)器可檢驗(yàn)、不可篡改的完整證明檔案。

Harmonic的產(chǎn)品，正是基于Lean的工具，以減少AI在數(shù)學(xué)上的幻覺(jué)。這條路線，需要大量已被人工標(biāo)注或是驗(yàn)證好的Lean的數(shù)據(jù)。Harmonic聲稱他們可以通過(guò)數(shù)據(jù)自動(dòng)形式化的方式，解決人工和數(shù)據(jù)收集方面的問(wèn)題。當(dāng)然，這背后有極其復(fù)雜的技術(shù)建構(gòu)。

簡(jiǎn)單理解就是，在數(shù)學(xué)里，一句簡(jiǎn)單的“顯然成立”，在Lean的代碼邏輯下，可能要拆成50條邏輯規(guī)則，少一條都不行，就像是給樂(lè)高城堡補(bǔ)上每一塊1*1的小磚。每一條都要具備極強(qiáng)的準(zhǔn)確性、細(xì)節(jié)性（保證每個(gè)逗號(hào)都有出處）和一致性，就像在給一篇維基百科做逐條公證。

至于Harmonic究竟用了什么技術(shù)細(xì)節(jié)，在可公開(kāi)的信息中，獲取有限。一年前，模型Aristotle剛問(wèn)世時(shí)，就有人質(zhì)疑道：無(wú)法在網(wǎng)站上找到任何ArXiv預(yù)印本論文得以證明他們的方法。

目前的公開(kāi)信息幾乎只有融資和測(cè)試成績(jī)，很難找到技術(shù)細(xì)節(jié)、模型架構(gòu)或開(kāi)放API信息。官方幾乎沒(méi)公開(kāi)接口文檔、模型API或詳細(xì)的開(kāi)發(fā)指南，技術(shù)社區(qū)也沒(méi)見(jiàn)到廣泛實(shí)測(cè)或開(kāi)源樣例。

雖然他們強(qiáng)調(diào)未來(lái)將應(yīng)用于軟件驗(yàn)證、數(shù)學(xué)研究等，但目前沒(méi)有公眾可驗(yàn)證的落地案例。對(duì)外能查到創(chuàng)始人背景和投資機(jī)構(gòu)，但在核心算法、工程團(tuán)隊(duì)、研究人員、具體解決方案方面完全"閉口不談"。

即便在AI聊天機(jī)器人應(yīng)用程序發(fā)布后，Harmonic 也仍然表示，目前不會(huì)發(fā)布Aristotle的其他基準(zhǔn)測(cè)試結(jié)果，全程觀看直播過(guò)后的網(wǎng)友們也紛紛提出疑惑。

看起來(lái)，Harmonic所采取的零幻覺(jué)的方法，很難說(shuō)是否真正突破了現(xiàn)有模型的能力，因?yàn)槟壳八坪醪](méi)能證據(jù)證明其模型已經(jīng)完全沒(méi)有幻覺(jué)了，Harmonic通過(guò)直接生產(chǎn)Lean代碼的方式控制幻覺(jué)的產(chǎn)生，因此或許模型本身或許仍然存在幻覺(jué)，但因?yàn)榛糜X(jué)錯(cuò)誤的代碼會(huì)被Lean代碼檢查出來(lái)，予以排除，故而能夠使結(jié)果零幻覺(jué)。

Harmonic的對(duì)手都是“業(yè)界第一”

在這個(gè)用Lean 4技術(shù)生成完整數(shù)學(xué)證明，從根本上杜絕AI"瞎編亂造"的技術(shù)路線上，已經(jīng)聚集了不少實(shí)力強(qiáng)勁的競(jìng)爭(zhēng)對(duì)手。

從官方數(shù)據(jù)來(lái)看，Aristotle的成績(jī)確實(shí)很亮眼。 在MiniF2F這個(gè)包含488道從高中到競(jìng)賽級(jí)數(shù)學(xué)題的測(cè)試中，Aristotle表現(xiàn)相當(dāng)出色：2024年6月左右，它的成功率達(dá)到83%（可以用計(jì)算器等工具輔助）；僅僅一個(gè)月后，成功率就提升到了90%，創(chuàng)下了當(dāng)時(shí)的新紀(jì)錄。

2024年6月，Harmonic放出來(lái)的信息展現(xiàn)其測(cè)試水平

作為對(duì)比，之前那些最SOTA的模型（比如OpenAI的GPT-4）在同樣條件下的成功率大約只有20-35%，Aristotle實(shí)現(xiàn)了幾倍的跨越。這說(shuō)明Aristotle的數(shù)學(xué)解題能力已經(jīng)遠(yuǎn)超普通的AI模型。

不過(guò)話說(shuō)回來(lái)，現(xiàn)在那些SOTA模型的文采、想象力很大程度上都依靠"適度的幻覺(jué)"，拿一個(gè)專門做數(shù)學(xué)的模型和通用AI比較，似乎有點(diǎn)"不太公平"。

并且，在讓AI零幻覺(jué)的領(lǐng)域，有錢有技術(shù)還努力的“富二代”并不只有Harmonic一家。

DeepSeek在兩個(gè)月前發(fā)布了Prover-V2模型，在MiniF2F測(cè)試中達(dá)到了88.9%的通過(guò)率，在其他數(shù)學(xué)競(jìng)賽上也有不錯(cuò)的表現(xiàn)。

技術(shù)架構(gòu)上，DeepSeek Prover先用DeepSeek-V3把復(fù)雜問(wèn)題拆解成一堆小目標(biāo)，每解決一個(gè)小目標(biāo)就把這些證明串成"思維鏈"，然后用這些數(shù)據(jù)來(lái)訓(xùn)練模型。

除了MiniF2F，PutnamBench評(píng)測(cè)集中收集了640道Putnam數(shù)學(xué)競(jìng)賽題，代表了本科生高難度數(shù)學(xué)題，對(duì)AI來(lái)說(shuō)極具挑戰(zhàn)性。最終，DeepSeek-Prover-V2在這658道題中成功解決了49道，也算是不錯(cuò)的成績(jī)。

谷歌DeepMind也是這個(gè)賽道的老手，其走的技術(shù)路線和Harmonic類似，谷歌DeepMind的Alphaproof，它在2024年可謂是數(shù)學(xué)AI領(lǐng)域的超級(jí)明星，賺足了眼球。它的成名之戰(zhàn)就是2024年的國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽（IMO）的測(cè)試得分。

DeepMind團(tuán)隊(duì)的AlphaProof和AlphaGeometry 2在這場(chǎng)比賽中拿到了銀牌成績(jī)——六道題解出了四道，這是一個(gè)里程碑式的存在。

《紐約時(shí)報(bào)》甚至用"數(shù)學(xué)家們讓路，AlphaProof來(lái)了"這樣的標(biāo)題來(lái)突出它的重要性。

AlphaProof的工作原理是，一個(gè)用Lean語(yǔ)言來(lái)證明數(shù)學(xué)結(jié)論的"自我訓(xùn)練"系統(tǒng)，結(jié)合了預(yù)訓(xùn)練語(yǔ)言模型和AlphaZero強(qiáng)化學(xué)習(xí)算法。Lean這種形式化語(yǔ)言的最大優(yōu)勢(shì)是能夠嚴(yán)格驗(yàn)證數(shù)學(xué)推理的正確性。在此之前，這種方法在機(jī)器學(xué)習(xí)中用得不多，因?yàn)槿斯ぞ帉懙臄?shù)據(jù)太少了。相比之下，基于自然語(yǔ)言的方法雖然可以使用更多數(shù)據(jù)，但經(jīng)常會(huì)產(chǎn)生看起來(lái)合理實(shí)際上錯(cuò)誤的推理步驟。

DeepMind當(dāng)然也意識(shí)到這個(gè)問(wèn)題，他們的做法是，通過(guò)調(diào)整Gemini模型，讓它自動(dòng)把自然語(yǔ)言的數(shù)學(xué)題翻譯成形式化語(yǔ)言，在這兩個(gè)領(lǐng)域之間架起了一座橋梁，從而建立了一個(gè)包含各種難度數(shù)學(xué)題的大型題庫(kù)。

就在前幾天，OpenAI研究科學(xué)家Alex Wei在X上發(fā)布推文，稱一種全新的神秘推理模型斬獲了IMO2025年金牌，6道題解出了5道。值得注意的是，該模型是在沒(méi)有任何工具或網(wǎng)絡(luò)輔助的狀態(tài)下，自行閱讀題目并撰寫自然語(yǔ)言證明的。

結(jié)語(yǔ)

盡管在解決AI幻覺(jué)上，技術(shù)尚未收斂，但對(duì)于剛發(fā)布產(chǎn)品和融資后的Harmonic來(lái)說(shuō)，這場(chǎng)與時(shí)間的賽跑正式開(kāi)始了。

與Harmonic不同的是，這些基礎(chǔ)模型大廠有自己多年的模型和海量數(shù)據(jù)作為基礎(chǔ)，比如DeepSeek的Prover系列，直接讓自家的DeepSeek-V3當(dāng)"教學(xué)者"，先教它學(xué)會(huì)怎么把復(fù)雜問(wèn)題拆解成簡(jiǎn)單步驟，再用這些經(jīng)驗(yàn)去訓(xùn)練專門的數(shù)學(xué)推理模型。谷歌的AlphaProof 背后有Gemini模型幫忙把日常語(yǔ)言翻譯成數(shù)學(xué)證明語(yǔ)言。

相比之下，Harmonic公司的Aristotle 并沒(méi)有像DeepSeek和谷歌那樣擁有完整的大模型"生態(tài)圈"做后盾。

但這也許是硅谷創(chuàng)新的獨(dú)特所在——收購(gòu)的文化以及良好的投資退出環(huán)境，Harmonic的目標(biāo)可能并非IPO一條路走到黑，他們可以在擁有足夠技術(shù)積累和實(shí)力時(shí)，選擇一條被大廠收購(gòu)的路線，成為這些基礎(chǔ)模型廠商技術(shù)生態(tài)中的一環(huán)，對(duì)于Harmonic與其投資者來(lái)說(shuō)，也是一個(gè)不錯(cuò)的選擇。