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