来源|多知

作者|王上

3月12日，致力于构建能够对软件和科学推理进行数学验证的AI初创公司Axiom(axiommath.ai)宣布完成A轮融资，本轮融资由Menlo Ventures 领投，筹集了2亿美元的新资金，公司估值超过16亿美元。

此轮融资代表着对其所称的“可信人工智能”(verified AI)这一新范式的押注，该技术旨在一劳永逸地消除人工智能“幻觉”的风险。

创始人洪乐潼(Carina Hong)说：“此轮融资将我们在形式数学领域的领先优势拓展至可信人工智能领域。”

洪乐潼说：“数学家和理论科学家构想理论，提出假设。然后他们提出证明，这是一个包含两个步骤的发现过程。我们创建Axiom，是为了将好奇的火花转化为已知的真理，并压缩取得突破的时间线。”

尽管像Claude Code和CodeRabbit这样的现有工具能够生成一些确实令人印象深刻且通常运行良好的代码，但其概率性的本质是一个主要的担忧原因。

这类工具旨在产生看起来正确的输出，而非那些可被证明是正确的输出。

Menlo Ventures 公司的合伙人马特·克兰宁(Matt Kraning)和C.C. 龚(C.C. Gong)认为，这是一个大问题。在宣布本轮融资的博客文章中，他们写道，当代码将被用于关键基础设施系统时，“能频繁工作”是一个“可怕的标准”。

Axiom 通过训练人工智能系统生成用Lean语言编写的、经过形式化验证的输出来规避这一问题。Lean是一种专为数学证明设计的编程语言。通过使用Lean，公理量化可以确保人工智能模型推理过程的每一步都是“可机器检查的”并且在逻辑上得到保证。

洪乐潼说：“我们创建 Axiom 的初衷是相信，从梦想的假设到最终的证明，只需几个小时，而非漫长的一生。经过验证的人工智能将猜想-证明的循环推广开来：任何已定义的事物都可以执行;任何已指定的事物都可以证明。这适用于数学、硬件和软件等各个领域。”

“我们相信，一旦验证能力突破关键阈值，将引发智能领域的范式转变。我们相信，实现已验证人工智能的速度和质量决定了超级智能的速度和质量。”洪乐潼说。

洪乐潼出生于广州，现年24岁，是一位学术成就卓越的斯坦福数学博士。她本科就读于麻省理工学院，获得数学和物理双学位，随后考取斯坦福大学数学博士，研究方向为数论、组合学和概率学。在校期间，她的论文已发表在《美国数学会会报》、《拉马努金期刊》等权威刊物，并于2021年获得牛津大学罗德奖学金，成为仅有的4名中国获奖者之一。

洪乐潼组建了一个超级团队，Axiom 的创始数学家肯·小野(Ken Ono)是古根海姆、帕卡德和斯隆奖学者，曾任美国数学学会副主席，也是世界顶尖的拉马努金数学权威之一。

Axiom 的首席技术官是前Facebook人工智能研究总监舒博·森古普塔(Shubho Sengupta)，他曾帮助英伟达公司编写了基础性的图形处理器库。团队还包括弗朗索瓦·沙尔东(François Charton)，他因率先应用Transformer模型解决了一个困扰专家130多年的数学难题而闻名。

Axiom 在去年10月已经完成了6400万美元的种子轮融资，此后取得了显著进展。去年12月，其确定性人工智能在普特南数学竞赛(Putnam Competition)中取得了完美成绩，该竞赛被数学家们认为是世界上最具挑战性的本科生数学考试。

Axiom 可验证地证明了一个已有20年历史的数论猜想，该猜想涉及用于测量曲面距离的微积分元素。这是一个挑战，肯·小野多年来屡次尝试都未能解决。

对于人工智能的每一个输出Axiom 都会生成一个由海量经过验证的数据组成的“可信数据飞轮”。这些数据随后被反馈回训练循环中，以增强其模型的能力，同时避免引入“模型崩溃”的风险。“模型崩溃”指的是数据污染给未经验证的人工智能模型带来的问题。通过这种方式，Axiom 形成了一个递归的自我改进循环。

研究公司Constellation Research的霍尔格·穆勒(Holger Mueller)表示，对于日益依赖“氛围编码”工具的开发者来说，一个能解决其风险的可行方案备受追捧。他认为，如果公理量化成功，将赢得大量拥趸。“大语言模型产生幻觉的风险并不‘可爱’;当涉及到它们编写的代码时，这是完全错误的，而且往往非常危险，”该分析师说。“Axiom 采取了正确的方法，利用数学来验证和核实人工智能生成的代码是安全可靠的。”

此轮融资的领投方Menlo Ventures 是一家成立于1976年的美国知名风险投资机构，专注于对消费科技和生命科学领域的早期至扩张期初创企业进行投资。