美國人工智能數學推理領域迎來新突破——專注于數學超級智能（MSI）開發的初創企業Harmonic宣布完成1.2億美元C輪融資，公司估值躍升至14.5億美元，正式躋身獨角獸行列。值得注意的是，這家成立僅兩年的企業尚未產生任何收入，卻憑借技術實力獲得資本市場的高度認可。
本輪融資由Ribbit Capital領投，紅杉資本、Kleiner Perkins及愛默生基金會參與投資。資金將主要用于構建超大規模算力基礎設施，以支撐其核心AI模型Aristotle的持續迭代。該模型通過將自然語言描述的數學問題轉化為可驗證的形式化語言，并使用編程語言Lean4輸出推理過程，開創了"機器可驗證"的數學解題新范式。據公司介紹，這種技術路徑能有效消除傳統AI模型常見的邏輯錯誤和事實偏差。
技術突破帶來顯著成果：今年7月，Aristotle在國際數學奧林匹克競賽（IMO）中創造歷史，成為首個對六道賽題中的五道給出形式化驗證解答的AI模型。相關證明文檔已公開上傳至GitHub平臺，供全球數學界審閱。公司聯合創始人弗拉德·特涅夫透露，升級后的模型新增自然英語輸入支持、自動引理生成功能，并優化了終端交互界面，開發者可通過API直接調用模型能力，移動端測試版應用也已同步上線。
支撐Aristotle的底層技術體系包含兩大核心組件：內部研發的AI幾何證明系統Yuclid，以及基于開源項目升級的自動化定理系統Newclid 3.0。前者專注于生成可驗證的幾何證明，后者則提供平面幾何問題的求解能力。這種軟硬協同的技術架構，使模型在處理復雜數學問題時展現出超越傳統AI的可靠性。
資本市場的熱情源于技術突破帶來的想象空間。路透社分析指出，Harmonic在IMO競賽中的表現，驗證了自動化數學推理與形式化驗證結合的技術路徑可行性。公司另一位聯合創始人圖多爾·阿希姆強調，當前進展表明MSI技術正在加速數學及定量領域的發展，AI推理與形式化驗證的深度融合將成為未來趨勢。這位斯坦福計算機博士出身的技術領袖，此前曾創立自動駕駛企業Helm.ai并擔任CTO。
值得注意的是，Harmonic的創始團隊兼具學術深度與商業經驗。特涅夫在創立Harmonic的同時，還擔任金融科技公司Robinhood Markets的董事長兼CEO，而阿希姆則擁有豐富的AI系統開發經驗。這種跨界組合為技術商業化提供了雙重保障，或許正是資本愿意為尚未盈利的初創企業投入重金的關鍵因素。
