编辑 | 程茜
今日，美国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推理与形式化验证全面融合的未来。”