据透社报道，Harmonic正在7月国际数学奥林匹克竞赛的亮眼成就吸引了投资者的关心，本钱市场对提拔AI精确性和靠得住性的手艺乐趣稠密。

　　本年7月，Harmonic正在社交平台X上官，Aristotle模子正在国际数学奥林匹克竞赛（IMO）中取得了金牌级此外成就，成为首个正在该角逐中，对六道题中的五道题给出可被形式化验证解答的模子，相关证明公开辟布正在了Github上。

　　Aristotle能把用天然言语输入的数学题为数学公式、计较机代码等形式化言语，并用编程言语Lean4输出推理过程，这些推理过程能够被机械验证。Harmonic认为，这种“可机械验证”的逻辑有帮于消弭和现实错误。

　　该公司由图多尔·阿希姆（Tudor Achim）和弗拉德·特涅夫（Vlad Tenev）结合开办。

　　Harmonic成立于2023年，次要产物是用于数学推理的AI模子Aristotle。该公司此前完成两轮融资：2024年9月，Harmonic完成由红杉本钱领投的7500万美元（约合人平易近币5。31亿元）A轮融资；本年7月，该公司再次完成1亿美元（约合人平易近币7。08亿元）B轮融资。

　　Harmonic通过Aristotle模子及其配套系统的持续升级，提拔了AI正在数学推理取形式化验证范畴的能力，其取得的一系列，也验证了从动化数学推理和形式化验证的手艺无效性。特涅夫称：“Harmonic的进展表白，MSI正加快数学及其他定量范畴的成长，我们曾经可以或许预见AI推理取形式化验证全面融合的将来。”？。

　　智工具11月26日动静，今日，美国AI数学推理创企Harmonic颁布发表完成了1。2亿美元（约合人平易近币8。5亿元）的C轮融资，估值达到14。5亿美元（约合人平易近币102。7亿元），跃升独角列，目前尚未发生收入。红杉本钱、Kleiner Perkins以及爱默生基金会参投。以鞭策下一阶段研发。

　　外媒BusinessWire报道，上周，新增对天然英语输入的支撑、从动引理生成功能，以及愈加简化的终端界面。

　　结合创始人兼首席施行官阿希姆博士结业于斯坦福大学，专攻计较机科学手艺，曾结合开办美国从动驾驶创企Helm。ai，并担任其首席手艺官。

　　Aristotle背后的支持系统次要包罗Yuclid和Newclid 3。0。Yuclid是Harmonic内部开辟的AI几何证明系统，为Aristotle的数学推理能力供给焦点支持。