其中一个原因是，在模型进化的路上，即使是在一个窄小的领域，实现AI的无幻觉性能，都是一项困难的任务，初创公司很难有资源与模型大厂抗衡。 近日，这家公司推出了面向IOS和Android的聊天机器人应用程序测试版，普通用户可以通过这款程序，访问其人工智能模型Aristotle。其首席执行官兼联合创始人Tudor Achim表示，Aristotle是人类可以进行推理并正式验证产出的第一款产物，在Aristotle支持的领域——定量推理，可以保证没有幻觉。同时，Harmonic还表示计划发布一个API，让公司访问Aristotle。在Harmonic的官网中宣称，其正在Github上公开发布Aristotle的完整证明，由于其经过正式验证，无需人工检查，这使得Aristotle在前沿人工智能模型中，处于高级数学推理性能的最前沿。 Harmonic在新产物的宣传攻势中表示，Aristotle在第66届国际数学奥林匹克IMO2025中取得了金牌。这场比赛也被视为AI数学能力和AI推理能力的“成人礼”。 虽然这一成绩也同样被谷歌和OpenAI斩获，但Harmonic认为这两家大厂“并非通过形式化验证手段取得结果”。从目前AI领域发展的整体来看，形式化（Formal）和非形式化（Informal）两种路径，到底哪种更有优势仍难以说清。 “如果从数学的角度，Scaling Law这条路跑到最后，一定会收敛。”一位头部基金合伙人告诉虎嗅，即便已经具备极高的行业地位，他仍然会每天阅读最新的论文，寻找突破AI边界的新的理论创新，这将是如今最具潜力和价值的地方。 也正因如此，Harmonic，这个成立仅两年，专注解决AI边界问题的初创公司，吸引了几乎所有顶级投资机构的目光，估值从零飙升到接近9亿美元。 不久之前，它就像一块磁石般吸引了近2亿美元的投资——从红杉资本到凯鹏华盈，从Index Ventures到Paradigm。这对于一家初创公司来说，都是一个不小的数字。 不过，针对基础模型的技术创新和创业，从来是一项烧钱的生意，一位硅谷投资人表示，如今基于基础模型的创业，早已是“富二代”的游戏，要么足够天才，要么足够有钱。 我们试图拆解这家在数学领域，和Open AI同台竞赛的初创公司，其背后的技术路线和厉害之处，回答Harmonic这将近9亿美金的估值，凭什么？其究竟如何实现数学推理中的AI零幻觉？ Harmonic的两位联合创始人——Vlad Tenev和Tudor Achim背景独特，一位在数学天赋上得天独厚，而另一位则在AI领域积累了深厚的经验，还有一个关键因素是，Vlad Tenev很有钱。 后来他投身金融科技创业，创立并担任Robinhood首席执行官，如果要更形象地比喻，Robinhood，是一个用手机App把股票、期权、加密货币甚至IPO打新都变成零佣金、低门槛、游戏化交易的互联网券商平台。2021年，Robinhood在纳斯达克上市，这家公司在Forbes的实时估值已经达到约55亿美元。 这也是为何Harmonic和Vlad Tenev被称为“美国版DeepSeek”和“梁文锋”的原因，创始人资金非常雄厚，在最一开始可以以非常纯粹的态度进行技术研究。Harmonic成立之初，用的一部分，就是Vlad Tenev的个人资金。 2016年，他和别人一起创立了自动驾驶公司Helm.ai并担任技术总监。在那里，他积累了丰富的AI算法开发经验，深知如何把AI技术应用到复杂的现实问题中。Helm.ai至今已经融资1.02亿美元，还得到了本田的支持。 两位创始人有个共同理念，就是"让AI会思考、讲真话，不撒谎"。他们的想法可以归纳为四点，首先，AI必须说实话：AI的输出必须经过严格检验，确保结论准确无误；其次，AI不能胡说八道，模型不能编造不存在的事实，宁可说"我不知道"也不要乱猜，通过严格的逻辑约束避免无根据的回答；第三，让AI像科学家一样思考：把假设-推理-验证的科学方法植入AI，让它能够自动探索和证明新结论；第四，人机合作而非替代，Harmonic认为AI数学助手应该帮助人类，而不是让用户没事可做。他们希望AI负责处理繁琐的证明工作，人类负责提出有创意的想法。 通用语言大模型的幻觉率长期居高不下，已成为制约其深入AI下半场——“应用”的最大阻碍，也正因为如此，“幻觉”同时也是业界眼中的“最美的一块肥肉”。哪家初创公司在这块阵地将幻觉率限制到一个较低的水平，同时保持AI的智能水平，谁就能撬动更加庞大的市场。 比如，我们看到各类AI应用在C端纷纷强调“实用性”与“可交付性”，努力用工具链与插件系统来弥补模型输出不稳定的问题，但在追求极低容错率的B端精密场景——像是金融建模、自动化编程、科学推理、法律合规等“不允许幻觉出现”的领域，通用大模型仍然举步维艰。 Aristotle的特别之处在于，它是个一站式数学AI：从理解普通话的数学问题，到生成严格的数学证明，再到用人话解释答案，一个模型全包了。虽然还没有对于Aristotle底层技术架构的丰富信息，但Harmonic已经通过官网公开了不少信息和成果。 首先是幻觉问题。通用大模型经常无中生有，编造不存在的内容。Aristotle通过Lean证明这个"硬约束"彻底解决了这个问题：每一步推导都需要得到系统认可，不允许凭空编造。一旦模型想输出错误结论，Lean立即报错拒绝。 其次，推理过程不清楚。传统AI即使能给出正确结论，推理步骤往往混乱或不完整。Aristotle通过详细展示每一步推理来解决这个问题。由于有Lean检查，整个推理链上的每个环节都必须逻辑清晰，让最终证明既正确又透明。这就像给出了"答案的答案"——不仅告诉使用者结论，还展示如何一步步得到它。 最后，传统大模型往往不够严谨。普通AI对问题的回答可能对错不分、过于自信，而Aristotle因为内置了数学逻辑，回答风格更谨慎客观。任何定理未经证明就不能用于下一步推导，这种严谨性确保了Aristotle非常适合高风险场景（如金融模型检查、医疗推理），因为它不会"差不多就下结论"。 2024年中，Harmonic宣布Aristotle在评估AI是否能读懂、建模并证明数学题的一项测试集——MiniF2F中创下了新纪录，领先了一众大模型，这个测试集包含488道形式化数学题目，涵盖数学核心领域（如代数、数论）。 比如，其官网展示了一道2001年国际数学奥林匹克的难题：给出题目和人类证明草稿后，Aristotle能自动生成完整的严格数学证明。这个例子显示了Aristotle如何把人类的自然语言证明翻译成机器能检查的严格代码。 在最近，Harmonic最新推出的Chatbot式应用程序的一波宣传攻势中，两位创始人声称Aristotle做数学推理问题时给出的答案完全“无幻觉”。 此外，Harmonic还计划发布一个to B的API以让公司可以访问，以及一个面向消费者的网络应用程序。 进入2025年，AI行业竞争越来越激烈，各大公司都在抢着布局更强的多模态和推理AI。特别是DeepMind在2024年底推出的AlphaProof取得成功，更是引发了市场对"AI证明"这个领域的关注。 A轮融资在2024年9月完成，拿到7500万美元，公司估值达到3.25亿美元。B轮融资于2025年7月宣布，又融了1亿美元，公司估值接近9亿美元，离10亿美元大关仅差一小步。 Harmonic的投资人阵容相当亮眼，既有顶级硅谷投资机构，也有行业基金和学术背景的资本，不仅有传统的顶级风投，还有新兴的科技基金。 同时，多家国际基金和知名个人也参与投资。B轮融资则由老牌投资机构Kleiner Perkins领投，专注加密和前沿科技的Paradigm大手笔跟投。红杉和Index作为老投资者继续投钱，金融科技投资机构Ribbit Capital新加入。此外，Quora联合创始人查理·切沃（Charlie Cheever）也以个人身份参与了B轮。 越来越多的数学家开始使用一种叫Lean的工具来写数学证明，这是一个由微软研究院开发的交互式定理证明系统，它能结合数学证明和编程的系统，能用代码形式精确地表达并验证复杂的数学理论，这成为了Harmonic的技术核心。 每写下一行代码，它就立刻像监理一样，用激光尺、钢筋扫描仪（形式化逻辑规则）分毫不差地检查一遍。只要发现缺了一根钉子、少了一块砖，它马上红灯报警，并要求返工。一旦全部绿灯，Lean会把整个证明自动“3D打印”出来——生成一个机器可检验、不可篡改的完整证明档案。 Harmonic的产物，正是基于Lean的工具，以减少AI在数学上的幻觉。这条路线，需要大量已被人工标注或是验证好的Lean的数据。Harmonic声称他们可以通过数据自动形式化的方式，解决人工和数据收集方面的问题。当然，这背后有极其复杂的技术建构。 简单理解就是，在数学里，一句简单的“显然成立”，在Lean的代码逻辑下，可能要拆成50条逻辑规则，少一条都不行，就像是给乐高城堡补上每一块1*1的小砖。每一条都要具备极强的准确性、细节性（保证每个逗号都有出处）和一致性，就像在给一篇维基百科做逐条公证。 至于Harmonic究竟用了什么技术细节，在可公开的信息中，获取有限。一年前，模型Aristotle刚问世时，就有人质疑道：无法在网站上找到任何ArXiv预印本论文得以证明他们的方法。 目前的公开信息几乎只有融资和测试成绩，很难找到技术细节、模型架构或开放API信息。官方几乎没公开接口文档、模型API或详细的开发指南，技术社区也没见到广泛实测或开源样例。 虽然他们强调未来将应用于软件验证、数学研究等，但目前没有公众可验证的落地案例。对外能查到创始人背景和投资机构，但在核心算法、工程团队、研究人员、具体解决方案方面完全"闭口不谈"。 即便在AI聊天机器人应用程序发布后，Harmonic也仍然表示，目前不会发布Aristotle的其他基准测试结果，全程观看直播过后的网友们也纷纷提出疑惑。 看起来，Harmonic所采取的零幻觉的方法，很难说是否真正突破了现有模型的能力，因为目前似乎并没能证据证明其模型已经完全没有幻觉了，Harmonic通过直接生产Lean代码的方式控制幻觉的产生，因此或许模型本身或许仍然存在幻觉，但因为幻觉错误的代码会被Lean代码检查出来，予以排除，故而能够使结果零幻觉。 从官方数据来看，Aristotle的成绩确实很亮眼。 在MiniF2F这个包含488道从高中到竞赛级数学题的测试中，Aristotle表现相当出色：2024年6月左右，它的成功率达到83%（可以用计算器等工具辅助）；仅仅一个月后，成功率就提升到了90%，创下了当时的新纪录。 作为对比，之前那些最SOTA的模型（比如OpenAI的GPT-4）在同样条件下的成功率大约只有20-35%，Aristotle实现了几倍的跨越。这说明Aristotle的数学解题能力已经远超普通的AI模型。 不过话说回来，现在那些SOTA模型的文采、想象力很大程度上都依靠"适度的幻觉"，拿一个专门做数学的模型和通用AI比较，似乎有点"不太公平"。 技术架构上，DeepSeek Prover先用DeepSeek-V3把复杂问题拆解成一堆小目标，每解决一个小目标就把这些证明串成"思维链"，然后用这些数据来训练模型。 除了MiniF2F，PutnamBench评测集中收集了640道Putnam数学竞赛题，代表了本科生高难度数学题，对AI来说极具挑战性。最终，DeepSeek-Prover-V2在这658道题中成功解决了49道，也算是不错的成绩。 谷歌DeepMind也是这个赛道的老手，其走的技术路线和Harmonic类似，谷歌DeepMind的Alphaproof，它在2024年可谓是数学AI领域的超级明星，赚足了眼球。它的成名之战就是2024年的国际数学奥林匹克竞赛（IMO）的测试得分。 AlphaProof的工作原理是，一个用Lean语言来证明数学结论的"自我训练"系统，结合了预训练语言模型和AlphaZero强化学习算法。Lean这种形式化语言的最大优势是能够严格验证数学推理的正确性。在此之前，这种方法在机器学习中用得不多，因为人工编写的数据太少了。相比之下，基于自然语言的方法虽然可以使用更多数据，但经常会产生看起来合理实际上错误的推理步骤。 DeepMind当然也意识到这个问题，他们的做法是，通过调整Gemini模型，让它自动把自然语言的数学题翻译成形式化语言，在这两个领域之间架起了一座桥梁，从而建立了一个包含各种难度数学题的大型题库。 就在前几天，OpenAI研究科学家Alex Wei在X上发布推文，称一种全新的神秘推理模型斩获了IMO2025年金牌，6道题解出了5道。值得注意的是，该模型是在没有任何工具或网络辅助的状态下，自行阅读题目并撰写自然语言证明的。 与Harmonic不同的是，这些基础模型大厂有自己多年的模型和海量数据作为基础，比如DeepSeek的Prover系列，直接让自家的DeepSeek-V3当"教学者"，先教它学会怎么把复杂问题拆解成简单步骤，再用这些经验去训练专门的数学推理模型。谷歌的AlphaProof背后有Gemini模型帮忙把日常语言翻译成数学证明语言。 但这也许是硅谷创新的独特所在——收购的文化以及良好的投资退出环境，Harmonic的目标可能并非IPO一条路走到黑，他们可以在拥有足够技术积累和实力时，选择一条被大厂收购的路线，成为这些基础模型厂商技术生态中的一环，对于Harmonic与其投资者来说，也是一个不错的选择。
