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