編譯 | 王欣逸

編輯 | 程茜

智東西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推理與形式化驗證全面融合的未來。」