近日，AI初创公司Axiom宣布完成2亿美元A轮融资，公司估值飙升至16亿美元。此次融资由硅谷顶级风投MenloVentures领投，Greycroft、MadronaVenture、BCapital、ToyotaVentures等老股东全部跟投。Axiom的创始人是25岁的洪乐潼（Carina Hong），她让大模型的推理过程像数学证明一样严格，每一步都可验证。洪乐潼17岁进入MIT，3年修完双学位，本科期间发表了9篇学术论文，研究方向涵盖模椭圆曲线、K3曲面上的L函数、"月光猜想"等基础数学领域。

Axiom采用"数学即服务"模式，通过训练AI系统生成用Lean语言编写的、经过形式化验证的输出。Lean是一种专为数学证明设计的编程语言，通过使用Lean，Axiom可以确保AI模型推理过程的每一步都是可机器检查的并且在逻辑上得到保证。去年12月，Axiom的核心系统在普特南竞赛中斩获满分，12题全对。普特南竞赛是北美地区最负盛名的大学生数学竞赛，成绩的中位数常常为零（满分120分）。过去近百年，仅有5人达成过满分成就。Axiom的AI做到了。