在最近，Harmonic最新推出的Chatbot式应用程序的一波宣传攻势中，两位创始人声称Aristotle做数学推理问题时给出的答案完全“无幻觉”。 此外，Harmonic还计划发布一个to B的API以让企业可以访问，以及一个面向消费者的网络应用程序。

两年估值接近9亿美元

Harmonic自成立以来，就受到了投资界的热烈追捧，短短两年内就完成了多轮大额融资。

从融资时机来看，Harmonic踩得很准，2024年，OpenAI推出了新模型，虽然展现了一定的数学能力，但还是会犯错，幻觉率仍居高不下。

这让整个行业开始意识到"AI需要更严谨的推理能力"，正好给Harmonic这样的公司创造了机会。

A轮融资时，投资方大多有学术或技术背景，他们看好Harmonic在学术上的突破。

进入2025年，AI行业竞争越来越激烈，各大公司都在抢着布局更强的多模态和推理AI。特别是DeepMind在2024年底推出的AlphaProof取得成功，更是引发了市场对"AI证明"这个领域的关注。

Harmonic在此时又适时开始融资B轮，正值整个行业寻求将AI从“能用”到“可用”的节点。

根据公开信息，Harmonic的种子阶段由联合创始人Vlad Tenev个人和天使投资人提供启动资金，主要用来组建团队和开展基础研究。

A轮融资在2024年9月完成，拿到7500万美元，公司估值达到3.25亿美元。B轮融资于2025年7月宣布，又融了1亿美元，公司估值接近9亿美元，离10亿美元大关仅差一小步。

Harmonic的融资图

Harmonic的投资人阵容相当亮眼，既有顶级硅谷投资机构，也有行业基金和学术背景的资本，不仅有传统的顶级风投，还有新兴的科技基金。

例如其A轮由硅谷知名的红杉资本（Sequoia Capital）领投，欧洲著名的Index Ventures紧跟其后。

同时，多家国际基金和知名个人也参与投资。B轮融资则由老牌投资机构Kleiner Perkins领投，专注加密和前沿科技的Paradigm大手笔跟投。红杉和Index作为老投资者继续投钱，金融科技投资机构Ribbit Capital新加入。此外，Quora联合创始人查理·切沃（Charlie Cheever）也以个人身份参与了B轮。

一个叫做“Lean”的超级“数学监理”

Harmonic究竟做了什么解决AI在数学推理上的瓶颈？

这要从数学界正在发生一些有趣的变化说起。

越来越多的数学家开始使用一种叫Lean的工具来写数学证明，这是一个由微软研究院开发的交互式定理证明系统，它能结合数学证明和编程的系统，能用代码形式精确地表达并验证复杂的数学理论，这成为了Harmonic的技术核心。

在Lean之前，大模型写数学证明的时候，幻觉往往表现在，看起来似乎说得头头是道，但往往会出现中间某一步是“AI觉得对”。

Lean则相当于一个数字化的超级监理和3D打印机器人。

每写下一行代码，它就立刻像监理一样，用激光尺、钢筋扫描仪（形式化逻辑规则）分毫不差地检查一遍。只要发现缺了一根钉子、少了一块砖，它马上红灯报警，并要求返工。一旦全部绿灯，Lean会把整个证明自动“3D打印”出来——生成一个机器可检验、不可篡改的完整证明档案。

Harmonic的产品，正是基于Lean的工具，以减少AI在数学上的幻觉。这条路线，需要大量已被人工标注或是验证好的Lean的数据。Harmonic声称他们可以通过数据自动形式化的方式，解决人工和数据收集方面的问题。当然，这背后有极其复杂的技术建构。

简单理解就是，在数学里，一句简单的“显然成立”，在Lean的代码逻辑下，可能要拆成50条逻辑规则，少一条都不行，就像是给乐高城堡补上每一块1*1的小砖。每一条都要具备极强的准确性、细节性（保证每个逗号都有出处）和一致性，就像在给一篇维基百科做逐条公证。

至于Harmonic究竟用了什么技术细节，在可公开的信息中，获取有限。一年前，模型Aristotle刚问世时，就有人质疑道：无法在网站上找到任何ArXiv预印本论文得以证明他们的方法。

目前的公开信息几乎只有融资和测试成绩，很难找到技术细节、模型架构或开放API信息。官方几乎没公开接口文档、模型API或详细的开发指南，技术社区也没见到广泛实测或开源样例。

虽然他们强调未来将应用于软件验证、数学研究等，但目前没有公众可验证的落地案例。对外能查到创始人背景和投资机构，但在核心算法、工程团队、研究人员、具体解决方案方面完全"闭口不谈"。

即便在AI聊天机器人应用程序发布后，Harmonic也仍然表示，目前不会发布Aristotle的其他基准测试结果，全程观看直播过后的网友们也纷纷提出疑惑。

看起来，Harmonic所采取的零幻觉的方法，很难说是否真正突破了现有模型的能力，因为目前似乎并没能证据证明其模型已经完全没有幻觉了，Harmonic通过直接生产Lean代码的方式控制幻觉的产生，因此或许模型本身或许仍然存在幻觉，但因为幻觉错误的代码会被Lean代码检查出来，予以排除，故而能够使结果零幻觉。

Harmonic的对手都是“业界第一”

在这个用Lean 4技术生成完整数学证明，从根本上杜绝AI"瞎编乱造"的技术路线上，已经聚集了不少实力强劲的竞争对手。

从官方数据来看，Aristotle的成绩确实很亮眼。 在MiniF2F这个包含488道从高中到竞赛级数学题的测试中，Aristotle表现相当出色：2024年6月左右，它的成功率达到83%（可以用计算器等工具辅助）；仅仅一个月后，成功率就提升到了90%，创下了当时的新纪录。

2024年6月，Harmonic放出来的信息展现其测试水平

作为对比，之前那些最SOTA的模型（比如OpenAI的GPT-4）在同样条件下的成功率大约只有20-35%，Aristotle实现了几倍的跨越。这说明Aristotle的数学解题能力已经远超普通的AI模型。

不过话说回来，现在那些SOTA模型的文采、想象力很大程度上都依靠"适度的幻觉"，拿一个专门做数学的模型和通用AI比较，似乎有点"不太公平"。

并且，在让AI零幻觉的领域，有钱有技术还努力的“富二代”并不只有Harmonic一家。

DeepSeek在两个月前发布了Prover-V2模型，在MiniF2F测试中达到了88.9%的通过率，在其他数学竞赛上也有不错的表现。

技术架构上，DeepSeek Prover先用DeepSeek-V3把复杂问题拆解成一堆小目标，每解决一个小目标就把这些证明串成"思维链"，然后用这些数据来训练模型。

除了MiniF2F，PutnamBench评测集中收集了640道Putnam数学竞赛题，代表了本科生高难度数学题，对AI来说极具挑战性。最终，DeepSeek-Prover-V2在这658道题中成功解决了49道，也算是不错的成绩。

谷歌DeepMind也是这个赛道的老手，其走的技术路线和Harmonic类似，谷歌DeepMind的Alphaproof，它在2024年可谓是数学AI领域的超级明星，赚足了眼球。它的成名之战就是2024年的国际数学奥林匹克竞赛（IMO）的测试得分。

DeepMind团队的AlphaProof和AlphaGeometry 2在这场比赛中拿到了银牌成绩——六道题解出了四道，这是一个里程碑式的存在。

《纽约时报》甚至用"数学家们让路，AlphaProof来了"这样的标题来突出它的重要性。

AlphaProof的工作原理是，一个用Lean语言来证明数学结论的"自我训练"系统，结合了预训练语言模型和AlphaZero强化学习算法。Lean这种形式化语言的最大优势是能够严格验证数学推理的正确性。在此之前，这种方法在机器学习中用得不多，因为人工编写的数据太少了。相比之下，基于自然语言的方法虽然可以使用更多数据，但经常会产生看起来合理实际上错误的推理步骤。

DeepMind当然也意识到这个问题，他们的做法是，通过调整Gemini模型，让它自动把自然语言的数学题翻译成形式化语言，在这两个领域之间架起了一座桥梁，从而建立了一个包含各种难度数学题的大型题库。

就在前几天，OpenAI研究科学家Alex Wei在X上发布推文，称一种全新的神秘推理模型斩获了IMO2025年金牌，6道题解出了5道。值得注意的是，该模型是在没有任何工具或网络辅助的状态下，自行阅读题目并撰写自然语言证明的。

结语

尽管在解决AI幻觉上，技术尚未收敛，但对于刚发布产品和融资后的Harmonic来说，这场与时间的赛跑正式开始了。

与Harmonic不同的是，这些基础模型大厂有自己多年的模型和海量数据作为基础，比如DeepSeek的Prover系列，直接让自家的DeepSeek-V3当"教学者"，先教它学会怎么把复杂问题拆解成简单步骤，再用这些经验去训练专门的数学推理模型。谷歌的AlphaProof背后有Gemini模型帮忙把日常语言翻译成数学证明语言。

相比之下，Harmonic公司的Aristotle并没有像DeepSeek和谷歌那样拥有完整的大模型"生态圈"做后盾。

但这也许是硅谷创新的独特所在——收购的文化以及良好的投资退出环境，Harmonic的目标可能并非IPO一条路走到黑，他们可以在拥有足够技术积累和实力时，选择一条被大厂收购的路线，成为这些基础模型厂商技术生态中的一环，对于Harmonic与其投资者来说，也是一个不错的选择。

本文来自虎嗅，原文链接：https://www.huxiu.com/article/4639590.html?f=wyxwapp