25岁的洪乐潼，最近在硅谷火了。
这个来自广东的女孩，17岁考入MIT，用三年时间修完了数学和物理双学位，之后又进入斯坦福深造。如果按照硅谷最熟悉的叙事模板，她无疑是“天才少女创业者”的典型。然而，真正让她被记住的，并非是这份华丽的履历，而是她所做的选择——一个在当下显得格外“反常识”的方向。
当整个行业都在追逐更大的模型参数、更强的生成能力与更拟人的表达时，洪乐潼却转身投入了一个最不“性感”、商业化也极具挑战的领域：用数学验证AI。
她创立的公司名为Axiom，成立不足两年，团队仅20余人。但就是这样一家初创公司，近期完成了2亿美元的A轮融资，投后估值高达16亿美元，折合人民币超过110亿元。Axiom不开发聊天机器人，不跟风文生图，也不卷入大语言模型的混战。它的核心业务是 “形式化验证”。
简单来说，这项技术旨在运用数学和逻辑，将AI的每一步推理都转化为可检查、可证明、甚至可以追责的过程。这听起来有些冷门，但它瞄准的正是当前大模型最棘手的问题——幻觉。
如今AI面临的主要矛盾，或许不再是能力不足，而是可靠性堪忧。模型可以给出看似正确、甚至结果正确的答案，但你永远无法确认，它究竟是真正通过推理得出了结论，还是仅仅“蒙对了”。Axiom试图做的，就是将这层不确定性剥离，将模糊的概率输出转变为确定性的、可验证的逻辑过程。
这也解释了为何洪乐潼最初带着这个想法寻求融资时，首先遭遇的并非掌声，而是一个极其现实的质问：“数学怎么赚钱？”
迎难而上的天才少女
洪乐潼的办公室位于硅谷帕洛阿尔托的大学大道，步行至斯坦福大学仅需半小时。斯坦福是她博士生涯的起点，但学位尚未完成，她便选择了退学创业。
实际上，在读博期间，洪乐潼就已经注册了公司。她将公司命名为Axiom，源自数学术语“公理”（Axiom）。她的愿景是：“从公理出发，打造一个能够自我改进的超级智能推理器。”
一个24岁的博士生，没钱、没人、没成型产品，仅凭一个构想，她就成功获得了960万美元的种子轮投资。
凭什么呢？关键在于她所瞄准的问题本质。现有的大模型本质上是基于海量数据训练出的概率黑盒，它们通过学习统计规律来生成答案，但其内部的推理过程无法被量化检视，这正是其会“胡说八道”、产生错误的根源。
洪乐潼想做的，正是利用数学公理和形式化验证，让AI的每一步推理都变得可证明。这项技术可以直接服务于金融、军工、芯片设计和自动驾驶等对可靠性要求极高的领域。显然，她触及了当前AI发展中最痛的痛点——幻觉与可靠性问题。
洪乐潼本人就是一位跨学科的学霸。她从小展现出惊人的数学天赋，高中时期已在多项全国性数学竞赛中屡获佳绩。2018年，17岁的她被MIT录取，三年内完成双学位并发表了9篇学术论文。此后，她获得牛津大学罗德奖学金，却出人意料地转向神经科学领域，目的是“构建跨越科学领域的认知体系”。
在此期间，她于由“深度学习之父”杰弗里·辛顿联合创立的盖茨比计算神经科学中心从事深度学习研究，正式踏入AI领域。随后，她进入斯坦福大学攻读数学与法律的跨学科博士。
2024年，当ChatGPT o3被曝光在数学测试中可能存在“作弊”嫌疑时，作为斯坦福数学博士的洪乐潼在社交媒体上评论道：“OpenAI大模型在数学测试中表现优秀，大概率是因为训练数据中提前泄题了。在一些测试中，大模型答案准确率虽高达96%，但一旦要求展示推理过程，得分率就骤降至5%。”
面对行业痛点，一种名为Lean的语言进入了她的视野，也让她嗅到了创业的契机。
与自然语言不同，Lean是一种可以自验证的数学编程语言。洪乐潼打了个比方：“如果用英语写出长达5000行的数学证明，我无法自行判断其正确性，必须寻求高水平专家验证。但Lean是自验证的，只要程序能跑通，证明就是对的。”
Lean的核心逻辑在于，将用自然语言或非形式化方法描述的证明，转化为机器可检查的形式化验证代码。那么，究竟什么是形式化验证？
你可以这样理解：面对一个普通的AI，你只能通过其最终答案来判断它是否“理解”了问题，但无从知晓中间过程是否有“瞎蒙”的成分。而形式化验证要求你将整个推理过程，一步步写成机器能够严格检查的逻辑链条。只要其中有任何一步跳跃、模糊或取巧，验证就无法通过。
形式化验证之所以能治理大模型的“幻觉”，是因为它不关心答案看起来如何，只关注结论是否从前提中通过合法的推理步骤一步步得出。只要过程经得起检验，结论就是可靠的，从而从根本上避免了模型凭空捏造事实。
因此，Axiom构建的系统，其工作模式是让大模型负责提出猜想和搜索解决方案，然后交由Lean进行严格的验算和判断。如果Lean检查发现推理过程有误，系统就会回溯，让模型重新调整。
但这无疑是一条窄路。这条赛道冷门到什么程度？在整个喧嚣的AI产业版图中，形式化验证几乎是边缘中的边缘，全球实现商业化的玩家屈指可数。
洪乐潼选择这条路，显然并非因为它是什么“风口”。这与她对“困难”的独特定义有关。她曾这样解释自己对数学的痴迷：“奥赛解题带来的是持续释放多巴胺的快感，而研究型数学更像是在不断撞墙，充满痛苦与煎熬。但我其实特别享受这种挑战感。”
正是这种刻在骨子里的挑战欲，推动她走出学术研究的舒适区，渴望在更广阔的战场上攻克AI领域的硬骨头。
2024年深秋，在斯坦福附近的一家咖啡馆里，洪乐潼与当时的Meta AI研究总监Shubho Sengupta进行了长达数小时的深入探讨，核心议题只有一个：AI能否真正学会数学推理？
两人理念高度契合，随即决定共同创业。一个从斯坦福退学，一个从Meta辞职。
一支“草根”工程师军团
Axiom团队目前只有20多名成员，洪乐潼用“草根工程师精神”来形容团队气质。
但实际上，这支团队的背景堪称豪华，一点也不“草根”。
公司的第一位成员，正是那位在咖啡馆长谈的Shubho Sengupta，他现在担任Axiom的CTO。核心科学家François Charton，是将Transformer架构引入数学推理领域的先驱人物。他的工作是将数学算式视为一种“语言”输入给Transformer，探索其能否像处理自然语言一样进行数学翻译。
团队中约半数成员来自Meta AI，另一半则是世界级的数学家与形式化验证专家。最让外界感到震惊的成员，是57岁的数学泰斗小野健（Ken Ono）。他是模形式领域的顶尖学者，曾担任美国数学学会副会长，获得过古根海姆奖、斯隆奖等众多荣誉。
这位弗吉尼亚大学的终身教授与洪乐潼的缘分始于麻省理工学院。当时，刚入学的洪乐潼参与了他的数论研究项目。这份师生情谊延续至今，但角色已然转变。2025年底，小野健辞去教职，全职加入Axiom，成为公司的第15号员工。
曾拒绝过Google和Meta邀请的小野健，为何愿意为一个24岁的学生“打工”？
他公开表示：“如果我的猜想能被机器在3天内推广到10个维度，我愿意当一个‘标注工’。”他选择加入，不仅因为洪乐潼提供了“不设教学、不设行政、100%投入科研”的合约，更关键的是，AI对他所从事的数学研究可能带来的“降维打击”，让他感到无比兴奋。
那么，一群顶级学者和前Meta精英，何来“草根”之说？
洪乐潼的解释是，“草根”代表的是始终“空杯”的心态和坚韧的品性。在创业这条全新道路上，即便是资深的“牛人”，也需要从头学起，不断自我革新。她自己也更倾向于做“nobody”（小人物），认为这样学习的坡度最陡、速度最快。
在领导风格上，洪乐潼说：“我其实不太喜欢用‘带领’这个词。我希望自己是一个‘独立贡献者’，团队中的每个人都是。这是一群志同道合的人在一起共同做事。”
“我们创立Axiom，就是要无限压缩把好奇心转化为真理的时间。”在资本驱动的硅谷，洪乐潼所展现出的这种纯粹性，对于顶尖研究者而言，或许比一份高薪合约更具吸引力。
这支不到20人的团队，在成立后不到一年便交出了一份令人瞩目的成绩单。
2025年12月3日，Axiom宣布其核心系统AxiomProver在无人干预的情况下，攻克了困扰数学界数十年的两道埃尔德什难题。同一天，洪乐潼收到了入选“福布斯30岁以下30人”榜单的消息。同月，AxiomProver又在以超高难度著称的普特南大学生数学竞赛中斩获满分，12道题全部正确。过去近百年间，仅有5位人类选手达成过这一成就。
AxiomProver的成功，为“通过形式化验证构建可靠、可核验、无幻觉的AI”这一技术路径提供了可复现、高难度的实证。
赛道升温，但挑战刚刚开始
从行业演进的角度看，洪乐潼的选择恰好踩在了一个技术转折点上。
2024年底，Meta FAIR实验室、斯坦福大学等多所机构联合发布了一篇立场论文《Formal Mathematical Reasoning: A New Frontier in AI》。论文指出，过去AI解决数学问题的方式，主要是灌输大量题目并让模型输出答案。这导致了数据污染、过程胡编乱造、AI无法自判对错且难以复现推理过程等问题。
论文认为，这显然是方向走偏了。真正的下一步，是将证明助手、形式化系统、自动验证等工具深度集成到模型中，让AI真正“懂得”数学推理。
这也意味着，这条曾经的“窄路”正在变得拥挤。
过去十年，AI赛道的主流叙事是“更大参数、更多数据、更快生成”，所有巨头都在此狂奔。洪乐潼最初选择的形式化验证，曾是其中冷门到几乎没有竞争的角落。如今，形势正在变化。今年初，Meta发布了半形式化推理技术，让大语言模型能够在不执行代码的情况下验证代码补丁，准确率达93%。竞品公司Harmonic在今年1月获得了英伟达的投资，估值达14.5亿美元，其产品已扩展到代码编写和芯片设计领域。此外，Theorem、Axiomatic AI、Cajal等一批初创公司也在近两年纷纷涌入这条赛道。
对于Axiom而言，挑战远不止于行业竞争。
最大的挑战在于商业模式。 洪乐潼最初的设想是将产品服务于对冲基金和量化交易公司，快速解决资产定价、股市预测等复杂的数学问题。但这个蓝图至今仍停留在构想阶段。对于高频交易而言，比“绝对正确”更重要的是“足够快”，毫秒级的延迟所带来的损失，可能远大于一次罕见的计算错误。Axiom所保证的绝对正确性，在追求极致速度的金融场景中，其实际价值目前仍需打一个问号。
另一个现实问题是：除了航空航天、国防军工等对价格极不敏感的少数领域，绝大多数企业是否愿意为“绝对正确”支付高昂的溢价？
洪乐潼自己也承认这一点：“数学怎么赚钱？我们从一开始就面临这个挑战。”但她坚信，“现在，商业信号已经清晰很多。数学能创造价值，正是因为它能自我验证、自我检查。”
另一方面，高达16亿美元的A轮估值本身也是一把双刃剑。这意味著投资人期待的是超高速的增长和明确的退出路径。Axiom必须在未来一到两年内证明其技术具备规模化商业化的潜力，否则下一轮融资将面临巨大压力。与此同时，它需要在行业巨头和众多强劲对手的夹击中，用更少的资源跑出更快的速度。
Axiom的未来，更像是一场理想主义的压力测试。从“绝对正确”的技术理想，到“相对经济”的商业世界，这家年轻公司真正的挑战，或许才刚刚开始。
技术的探索永无止境，关于AI可靠性、形式化验证等前沿话题的讨论，也欢迎你在云栈社区的相关板块与更多开发者交流碰撞。
发表于 5 小时前
|
查看: 5|
回复: 0
