专攻数学超级智能的Harmonic获7500万美元投资，红杉领投，CEO：将是下一个AI前沿

　　来源|多知

　　作者|王上

　　今天，致力于创造数学超级智能(MSI)的人工智能初创公司Harmonic在其官网宣布，已经完成了7500万美元的A轮融资。本轮融资由红杉资本领投，Index Ventures、Jasper Lau的Era Funds、GreatPoint Ventures、DTS Global Partners、Palo Alto Networks Inc.等公司参投。当前，公司估值达到3.25亿美元。

　　Harmonic成立于2023年，其目标是创造数学超级智能（MSI），MSI是一种数学能力优于人类的人工智能，在Harmonic看来，由于推理的语言是数学，而数学是人类发现关于宇宙的许多基本真理的手段，因此，具有MSI的人工智能系统应该能够极大提高人类在科学和工程等领域的知识和理解。

　　在Harmonic的官方博客文章中，Harmonic解释说，数学超级智能(MSI)是实现逻辑推理的关键，这有助于确保人工智能模型的反应始终是正确和真实的。它补充说，人工智能系统必须具有“强大和可验证的推理能力”。

　　也就是说，Harmonic认为，数学超级智能(MSI)能克服传统上“幻觉”的限制，即消除AI模型无法正确回答的问题编造答案的情况。

　　可以看到，越来越多人工智能公司聚焦数学领域，希望攻克大模型的推理能力。

　　在Harmonic 看来，带有数学超级智能(MSI)的技术将应用于特别需要准确性的行业，包括软件工程、工业设计和医疗技术等。

　　Harmonic联合创始人兼首席执行官Tudor Achim表示，数学超级智能（MSI）将是下一个人工智能前沿。

　　01

　　用新方法解决幻觉问题，在形式数学基准中达到了90%的水平

　　Harmonic的大模型致力于解决高难度数学问题，并采用了和自然语言不一样的训练方式。

　　对于自然语言大模型来说，一个致命的缺点是总产生幻觉问题，Harmonic希望能解决这个问题。

　　今年8月，Harmonic宣布了正在开发的第一个模型Aristotle(亚里士多德)，这是以希腊哲学家和数学家的名字命名的大模型。

　　当遇到自然语言数学问题时，Aristotle有能力用Lean 4(一种基于微积分的函数编程语言)将这些问题形式化。以形式化验证的方式解决问题，并以自然语言和 Lean 输出答案。“这是朝着我们‘解决研究数学中的高级问题和验证世界上所有推理’的长期目标迈出的重要一步。”Harmonic团队提到。

　　在博客中，Harmonic团队提到，现有的大型语言模型在遇到问题时时常会产生幻觉。幻觉可能很危险，因为它们会导致人工智能系统以不可预测的方式行事。更重要的是，随着人工智能在人们的生活中扮演越来越重要的角色，幻觉的风险也在增加。

　　Harmonic表示，如果它能为人工智能模型提供进行数学推理的能力，就应该能够保证它们的反应永远是正确的，因此不会产生幻觉。Harmonic认为，与目前的模型不同，这种具有透明和可验证的“推理痕迹”的模型将“从根本上是安全的”。

　　今年9月，Harmonic 在数学超级智能方面取得最新进展，比如：

　　1)MiniF2F 基准测试中达到 90% 的最新水平(8月份的成绩为83%);

　　2)对 MiniF2F 内部更新的公开发布;

　　3)全新的自然语言界面。

　　MiniF2F是标准的形式数学基准，它将形式定理证明问题与自然语言和形式数学之间的转换分离开来。这些问题来自国内和国际高中数学竞赛，以及高中和本科数学课程。这些问题涵盖了从简单计算到极具挑战性的证明等一系列难度：三道验证集问题来自国际数学奥林匹克 (IMO)，即使对于训练有素的参赛者来说，这些问题也普遍被认为极其困难。

　　未来，Harmonic 计划在关键的数学基准上跟踪系统不断增长的能力。

　　Harmonic 在官方博客中提到：“MiniF2F 衡量了我们模型在面对形式化问题时的核心问题解决能力。这让我们能够将Aristotle与人类表现和先前的研究进行对比。展望未来，我们将继续公开跟踪 MiniF2F 等形式化基准测试以及涉及自然语言理解的任务的进展。”

　　02

　　数学超级智能可应用于多个行业，“是人工智能的下一个前沿”

　　Harmonic 声称，带有MSI的人工智能模型将立即在目前无法依赖人工智能的一系列行业中发挥作用，包括航空航天、计算机芯片设计、工业系统和医疗保健，这些行业对软件的可靠性至关重要。

　　此外，Harmonic 将帮助推动人工智能研究本身的边界，使创建更强大的系统，甚至可以创建自己的合成数据，以增强他们的知识和学习。

　　2023 年，Tudor Achim与Vlad Tenev共同创立了 Harmonic，旨在打造世界上最先进的推理引擎。

　　Tudor Achim与Vlad Tenev都是连续创业者：

　　udor Achim还是Helm.ai的联合创始人兼前首席技术官，Helm.ai为高级驾驶辅助系统(ADAS)、自动驾驶(AV)和机器人自动化提供先进人工智能(AI)软件的供应商。Tudor Achim拥有卡内基梅隆大学计算机科学学士学位，曾是斯坦福大学计算机科学博士候选人。

　　Vlad Tenev还是 Robinhood Markets (美国在线股票交易平台)的联合创始人兼首席执行官，Vlad Tenev拥有斯坦福大学数学学士学位和加州大学洛杉矶分校数学硕士学位。

　　Harmonic联合创始人兼首席执行官Tudor Achim表示，人工智能行业已经意识到数学是构建真正的超级智能所需的缺失环节。他说：“Harmonic正在引领这些发展，同时解决了其他人工智能模型中常见的局限性。”

　　这家初创公司表示，今天这轮融资的资金将帮助它加速Aristotle的开发，并创建第一个数学技能优于人类的人工智能系统。

　　红杉资本的合伙人安德鲁·里德(Andrew Reed)表示，他之所以投资Harmonic，是因为他相信人工智能可以加速人类的数学能力，为新的人工智能应用铺平道路。

　　Vlad Tenev 表示：“我们相信数学超级智能是人工智能的下一个前沿。我们很高兴与 Sequoia、Index 和许多其他伟大的投资者合作，加速准确且寻求真相的人工智能模型的出现。”

　　END

　　作者：王上