英伟达投的AI公司，要入局芯片验证

由 Robinhood 首席执行官 Vlad Tenev 联合创立的人工智能初创公司 Harmonic 周二表示，随着人工智能在检测软件缺陷方面的应用日益广泛，该公司正在将其 Aristotle 模型从数学证明扩展到软件和芯片设计验证，这引起了越来越多的关注。

研究人员最近利用这项技术发现了 PHP 中的严重漏洞，引发了全球范围内修复这些漏洞的行动。

在英伟达旗下风险投资机构NVentures、红杉资本和Ribbit Capital的支持下，Harmonic去年11月完成了一轮1.2亿美元的融资，公司估值达到14.5亿美元。

Harmonic公司正在开发一种名为“数学超级智能”的技术，这是一种以推理为中心的AI系统，旨在减少幻觉和事实错误。

该公司表示，Aristotle 现在可以验证用 C 语言编写的软件和用 Verilog 语言编写的芯片设计。

数学超级智能初创公司 Harmonic AI Inc.在今年年初透露，英伟达公司的风险投资部门 NVentures 是其11 月份完成的 1.2 亿美元 C 轮融资的投资者之一，该轮融资的估值为 14.5 亿美元。

这笔资金将用于加速 Harmonic 公司开发 Aristotle 的进程。该公司声称 Aristotle 是世界上最先进的数学推理引擎，可以消除幻觉。

Aristotle 是一款专门用于形式化数学推理的人工智能引擎。该引擎使用 Lean 4 证明助手，允许用户以计算机可检查正确性的方式编写数学定义、定理和证明，从而将自然语言数学问题转换为形式化可验证的证明。

数学超级智能是该公司方法的核心，其人工智能提供的推理能力可以媲美甚至超越人类。该方法利用合成数据生成进行训练，而非依赖网络抓取的数据，而是自主生成形式化的问题证明对，从而实现递归式自我改进。

亚里士多德模型已经引起了轰动：该模型在 2025 年国际数学奥林匹克竞赛中获得了金牌。

最近，Harmonic 进一步扩展了 Aristotle 的功能，在人工智能编码领域取得了新的突破——在可验证代码生成竞技场 (VERINA) 基准测试中取得了 96.8% 的领先成绩。VERINA 基准测试由加州大学伯克利分校和 Meta Platforms Inc. 的研究人员开发，是衡量可验证代码生成的高质量基准测试方法。

Harmonic认为，代码生成已迅速成为大型语言模型最强大的应用场景之一。然而，使用非正式方法验证正确性成本高昂且需要人工操作，这导致了与亚里士多德在数学领域已经开始着手解决的验证瓶颈相同的问题。

“Aristotle 在解决重大数学难题方面的成功，以及其在完全自主定理证明方面的突破，都表明 Harmonic 在实现数学超级智能方面取得了快速进展，”首席执行官 Tudor Achim 表示。“这项支持将帮助我们提升 Aristotle 的能力，加快数学领域的发现步伐，并使各行各业能够利用数学人工智能的力量来解决关键的高风险问题。”

此次新融资是在此前完成的 B 轮融资（估值 9 亿美元，融资额 1 亿美元） 和2024 年 9 月 的 A 轮融资（融资额 7500 万美元） 之后进行的。

除了英伟达旗下的 NVentures 之外，C 轮融资的其他投资者还包括 Kleiner Perkins Caufield & Byers、Paradigm Management、Ribbit Capital Management、Sequoia Capital Operations、Index Ventures Management 和 Charlie Cheever。

（来源：内容来自半导体芯闻综合）