在AI技术的快速迭代中，一家名为Harmonic的初创公司正试图挑战AI模型的边界，开发一种无幻觉的AI模型。Harmonic的首席执行官兼联合创始人Tudor Achim表示，他们的最新产品Aristotle是首个能够进行推理并通过正式验证的AI模型，特别是在定量推理领域，Aristotle的表现堪称完美。
近日，Harmonic推出了面向iOS和Android的聊天机器人应用程序测试版，用户可以通过这款应用访问Aristotle模型。公司还计划发布一个API，让企业也能利用Aristotle的能力。Harmonic宣称，Aristotle在第66届国际数学奥林匹克竞赛中获得了金牌，这被视为AI在数学和推理能力上的重要里程碑。
尽管谷歌和OpenAI也在该竞赛中取得了优异成绩，但Harmonic认为它们并非通过形式化验证手段取得结果。形式化（Formal）和非形式化（Informal）两种路径在AI领域的发展中各有优势，但Harmonic选择了一条更加严谨的道路。
Harmonic的两位联合创始人背景独特，Vlad Tenev拥有深厚的数学背景，曾在斯坦福大学和加州大学洛杉矶分校学习数学，并师从数学大师陶哲轩。Tudor Achim则是计算机科学的专家，拥有丰富的AI算法开发经验。两位创始人的共同理念是“让AI会思考、讲真话，不撒谎”，他们的目标是探索人工智能的前沿应用。
Aristotle模型通过Lean证明系统解决了AI模型中的幻觉问题。Lean是一个由微软研究院开发的交互式定理证明系统，能够精确表达并验证复杂的数学理论。Aristotle在每一步推导中都需要得到系统的认可，不允许凭空编造，从而确保了输出的准确性和可靠性。
自2024年成立以来，Harmonic在短时间内完成了多轮大额融资，估值迅速攀升至接近9亿美元。A轮融资由红杉资本领投，B轮融资则由Kleiner Perkins领投，吸引了众多顶级投资机构的关注。Harmonic的融资成功不仅反映了市场对AI技术的热情，也证明了其在AI推理领域的独特优势。
Harmonic的技术路线依赖于Lean系统，这需要大量经过人工标注或验证的数据。尽管Harmonic声称可以通过数据自动形式化的方式解决人工和数据收集问题，但具体的技术细节尚未公开。然而，Aristotle在MiniF2F测试集上的表现已经证明了其强大的数学解题能力，成功率远超其他SOTA模型。
在让AI零幻觉的领域，Harmonic并非孤军奋战。DeepSeek、谷歌DeepMind等公司也在探索类似的技术路线。DeepSeek的Prover-V2模型在MiniF2F测试中达到了88.9%的通过率，而谷歌DeepMind的AlphaProof则在国际数学奥林匹克竞赛中获得了银牌。这些竞争对手的存在证明了AI推理领域的竞争激烈和潜力巨大。
尽管Harmonic在技术和融资上取得了显著进展，但面对基础模型大厂如DeepMind和OpenAI的竞争，它仍需不断努力。然而，硅谷的创新文化和良好的投资退出环境为Harmonic提供了多种可能性。在拥有足够技术积累和实力时，Harmonic可以选择被大厂收购，成为其技术生态中的一环。
Harmonic的故事展示了AI技术在不断突破边界的过程中所面临的挑战和机遇。随着技术的不断进步和市场的日益成熟，Harmonic有望在AI推理领域取得更加显著的成就。
