智東西（公眾號：zhidxcom）
編譯 | ?王欣逸
編輯 | ?程茜
智東西11月26日消息，今日，美國AI數(shù)學推理創(chuàng)企Harmonic宣布完成了1.2億美元（約合人民幣8.5億元）的C輪融資，估值達到14.5億美元（約合人民幣102.7億元），躍升獨角獸行列，目前尚未產(chǎn)生收入。
本輪融資由Ribbit Capital領(lǐng)投，紅杉資本、Kleiner Perkins以及愛默生基金會參投。新融資的大部分資金將用于支持其模型訓練所需的巨大算力，以推動下一階段研發(fā)。
Harmonic成立于2023年，主要產(chǎn)品是用于數(shù)學推理的AI模型Aristotle。該公司此前完成兩輪融資：2024年9月，Harmonic完成由紅杉資本領(lǐng)投的7500萬美元（約合人民幣5.31億元）A輪融資；今年7月，該公司再次完成1億美元（約合人民幣7.08億元）B輪融資，公司估值達到8.75億美元（約合人民幣72億元）。
該公司由圖多爾·阿希姆（Tudor Achim）和弗拉德·特涅夫（Vlad Tenev）聯(lián)合創(chuàng)辦。
聯(lián)合創(chuàng)始人兼首席執(zhí)行官阿希姆博士畢業(yè)于斯坦福大學，專攻計算機科學技術(shù)，曾聯(lián)合創(chuàng)辦美國自動駕駛創(chuàng)企Helm.ai，并擔任其首席技術(shù)官。
另一位聯(lián)合創(chuàng)始人特涅夫現(xiàn)任Harmonic執(zhí)行主席，本碩先后就讀于斯坦福大學和加州大學洛杉磯分校，他兼任美國金融科技公司Robinhood Markets聯(lián)合創(chuàng)始人、董事長兼首席執(zhí)行官。
▲特涅夫（左）和阿希姆（右）（圖源：Harmonic）
Harmonic自稱正在建立世界上最先進的數(shù)學推理引擎，目標是打造數(shù)學超級智能（Mathematical Superintelligence，MSI），該公司推出了其旗艦AI數(shù)學推理模型Aristotle。
Aristotle能把用自然語言輸入的數(shù)學題轉(zhuǎn)化為數(shù)學公式、計算機代碼等形式化語言，并用編程語言Lean4輸出推理過程，這些推理過程可以被機器驗證。Harmonic認為，這種“可機器驗證”的邏輯有助于消除幻覺和事實錯誤。
今年7月，Harmonic在社交平臺X上官宣稱，Aristotle模型在國際數(shù)學奧林匹克競賽（IMO）中取得了金牌級別的成績，成為首個在該比賽中，對六道題中的五道題給出可被形式化驗證解答的模型，相關(guān)證明公開發(fā)布在了Github上。
Aristotle背后的支撐系統(tǒng)主要包括Yuclid和Newclid 3.0。Yuclid是Harmonic內(nèi)部開發(fā)的AI幾何證明系統(tǒng)，用于生成可形式化驗證的幾何證明；Newclid 3.0是在平面幾何問題求解開源項目Newclid的基礎(chǔ)上升級的自動化幾何定理系統(tǒng)，為Aristotle的數(shù)學推理能力提供核心支撐。
外媒BusinessWire報道，上周，Harmonic還對Aristotle模型及其交互平臺進行了升級，新增對自然英語輸入的支持、自動引理生成功能，以及更加簡化的終端界面。
Aristotle模型已通過API向開發(fā)者開放，Harmonic還宣布推出了iOS和Android的測試版本App。
結(jié)語：資本看好提升AI準確性和可靠性技術(shù)
據(jù)路透社報道，Harmonic在7月國際數(shù)學奧林匹克競賽的亮眼成績吸引了投資者的關(guān)注，資本市場對提升AI準確性和可靠性的技術(shù)興趣濃厚。
Harmonic通過Aristotle模型及其配套系統(tǒng)的持續(xù)升級，提升了AI在數(shù)學推理與形式化驗證領(lǐng)域的能力，其取得的一系列成果，也驗證了自動化數(shù)學推理和形式化驗證的技術(shù)有效性。特涅夫稱：“Harmonic的進展表明，MSI正加速數(shù)學及其他定量領(lǐng)域的發(fā)展，我們已經(jīng)能夠預見AI推理與形式化驗證全面融合的未來?！?/p>
來源：BusinessWire、路透社、Harmonic
