美國人工智能數(shù)學(xué)推理領(lǐng)域迎來新突破——專注于數(shù)學(xué)超級智能（MSI）開發(fā)的初創(chuàng)企業(yè)Harmonic宣布完成1.2億美元C輪融資，公司估值躍升至14.5億美元，正式躋身獨(dú)角獸行列。值得注意的是，這家成立僅兩年的企業(yè)尚未產(chǎn)生任何收入，卻憑借技術(shù)實(shí)力獲得資本市場的高度認(rèn)可。

本輪融資由Ribbit Capital領(lǐng)投，紅杉資本、Kleiner Perkins及愛默生基金會參與投資。資金將主要用于構(gòu)建超大規(guī)模算力基礎(chǔ)設(shè)施，以支撐其核心AI模型Aristotle的持續(xù)迭代。該模型通過將自然語言描述的數(shù)學(xué)問題轉(zhuǎn)化為可驗(yàn)證的形式化語言，并使用編程語言Lean4輸出推理過程，開創(chuàng)了"機(jī)器可驗(yàn)證"的數(shù)學(xué)解題新范式。據(jù)公司介紹，這種技術(shù)路徑能有效消除傳統(tǒng)AI模型常見的邏輯錯誤和事實(shí)偏差。

技術(shù)突破帶來顯著成果：今年7月，Aristotle在國際數(shù)學(xué)奧林匹克競賽（IMO）中創(chuàng)造歷史，成為首個對六道賽題中的五道給出形式化驗(yàn)證解答的AI模型。相關(guān)證明文檔已公開上傳至GitHub平臺，供全球數(shù)學(xué)界審閱。公司聯(lián)合創(chuàng)始人弗拉德·特涅夫透露，升級后的模型新增自然英語輸入支持、自動引理生成功能，并優(yōu)化了終端交互界面，開發(fā)者可通過API直接調(diào)用模型能力，移動端測試版應(yīng)用也已同步上線。

支撐Aristotle的底層技術(shù)體系包含兩大核心組件：內(nèi)部研發(fā)的AI幾何證明系統(tǒng)Yuclid，以及基于開源項(xiàng)目升級的自動化定理系統(tǒng)Newclid 3.0。前者專注于生成可驗(yàn)證的幾何證明，后者則提供平面幾何問題的求解能力。這種軟硬協(xié)同的技術(shù)架構(gòu)，使模型在處理復(fù)雜數(shù)學(xué)問題時展現(xiàn)出超越傳統(tǒng)AI的可靠性。

資本市場的熱情源于技術(shù)突破帶來的想象空間。路透社分析指出，Harmonic在IMO競賽中的表現(xiàn)，驗(yàn)證了自動化數(shù)學(xué)推理與形式化驗(yàn)證結(jié)合的技術(shù)路徑可行性。公司另一位聯(lián)合創(chuàng)始人圖多爾·阿希姆強(qiáng)調(diào)，當(dāng)前進(jìn)展表明MSI技術(shù)正在加速數(shù)學(xué)及定量領(lǐng)域的發(fā)展，AI推理與形式化驗(yàn)證的深度融合將成為未來趨勢。這位斯坦福計(jì)算機(jī)博士出身的技術(shù)領(lǐng)袖，此前曾創(chuàng)立自動駕駛企業(yè)Helm.ai并擔(dān)任CTO。

值得注意的是，Harmonic的創(chuàng)始團(tuán)隊(duì)兼具學(xué)術(shù)深度與商業(yè)經(jīng)驗(yàn)。特涅夫在創(chuàng)立Harmonic的同時，還擔(dān)任金融科技公司Robinhood Markets的董事長兼CEO，而阿希姆則擁有豐富的AI系統(tǒng)開發(fā)經(jīng)驗(yàn)。這種跨界組合為技術(shù)商業(yè)化提供了雙重保障，或許正是資本愿意為尚未盈利的初創(chuàng)企業(yè)投入重金的關(guān)鍵因素。