夜雨聆风每日学习：第221天
播客：Scaling Past Informal AI - Carina Hong, Axiom Math
上个月写陶哲轩那期的时候，我写过一句话：猜想廉价、验证昂贵。
当时的语境是，AI能生成无穷无尽的猜想，真正的瓶颈在于谁来判断哪个猜想像样。那篇文章主要说验证者比生成者更稀缺。最近听了Carina Hong这期播客，发现自己漏掉了另一个方向，验证比我想的更深一层。除了稀缺性之外，它本身还是一种学习机制。
Carina是Axiom Math的创始人，七个月的公司，三十个人，刚拿了A轮融资两亿美元，估值十六亿。这个数字本身就值得琢磨。什么赛道值得花两亿美元赌一个成立不到一年的团队？她把形式化验证从合规工具的位置上挪开了，放到了基础设施那一栏。一个让才华产生复利的基础设施。
棋谱为什么比天才更值钱
Carina讲了一个类比。拉马努金是数学史上直觉最强的人之一，没受过任何正规证明训练，凭空写出几千个公式。但在遇到哈代、学会写证明之前，那些公式只是他脑子里的直觉，别人用不上，后代继承不了。学会证明写作之后，直觉变成了定理，一百年后的数学家还能站在上面继续走。
棋谱的逻辑是一样的。聂卫平的天才在他脑子里的时候，只能他自己用。写成棋谱之后，柯洁可以打谱学他，AlphaGo可以吃掉他。一盘棋不再是"这个人那天下午在想什么"。它变成一份公开数据，所有人都可以复盘、分析、改进。这个过程本身就是才华的复合。
Carina的判断是，AI加上形式化验证，等于把棋谱化这个过程自动化了，从手工变成机器来做。现在的AI做数学，用的是非形式化方法。模型给出证明，人类来判断对不对，然后根据人类偏好调整模型。这个方法有个麻烦。不同评审对同一个证明给出不同的反馈，模型收到的信号永远不一致。人类偏好本身就在引入噪声。
她做的事情不一样。她把AI训练放在Lean这个形式化证明系统里。证明进去只有两种结果，编译通过或者编译失败。没有"这个证明大概百分之八十是对的"这回事。训练反馈从模模糊糊变成了非黑即白。她的系统在2024年普特南数学竞赛拿了满分一百二十分，人类冠军一百一十分，其他AI系统也没超过这个分数。用的训练数据比非形式化模型少了好几个数量级。
每一行代码，要写二十行证明
这件事听起来很美，但有一个现实的代价。主持人问Carina，对于一个正常大小的程序，Lean证明大概有多长。她说，每一行代码，大概要配二十行证明。
主持人愣了一下："这听着不怎么靠谱。"
这就是形式化方法几十年没做大的原因。理论上是对的。软件工程的人从七十年代就在说，我们应该用数学证明程序的正确性。现实里，没人有耐心为每一行代码写二十行证明。你写一个一万行的程序，证明就是二十万行。这谁受得了。
Carina想说的是，AI把这个等式改写了。以前写证明只能靠人，几百个人花几年时间验证一个局部问题。在芯片行业，设计和验证的人力比是一比三甚至一比四，时间和预算跟着平方涨。GPU验证没有"差不多对了"，只有"过了"或"没过"。你现在让一千个人去验一个GPU，他们也只能告诉你"大概没问题"。
AI改写了这件事。Carina的团队让AI自己去写那些证明。Lean证明的验证本来就是机器做的。AI生成证明，Lean编译器自动判定对错。验证不需要人的注意力。
她把整个系统拆成两个阶段。第一阶段是猜，提出猜想，跟出题没太大区别。猜想不需要百分之百精确，非形式化AI就够用。第二阶段是证，把猜想翻译成Lean可以验证的形式化证明。在这一步卡住的时候，AI把问题拆成几个更小的子问题，一个个做，卡住了就退回上一级换一条路再试。这跟你解一道难题差不多。试一个思路，卡住了，退回来，换条路继续试。
有一个坑暂时绕不过去。把"Alice和Bob去市场买东西"这种自然语言描述的问题，转化成Lean的形式化规范，这个自动形式化步骤本身，还没有好的自动验证方式。你写完了形式化规范，怎么知道它真的对应了原问题？目前答案是：还是得人看一眼。但只要熬过这一步，后面的证明生成和验证就全是机器的事了。
人最稀缺的东西，是注意力
Carina这期播客里有好几个碎片，串起来指向同一个东西。
数学论文的同行评审平均要两年。Frontier Math基准测试征集题目的时候，靠自己的专家池根本凑不齐，得去找Epoch AI合作。OpenAI做形式化数学的人，GPTF团队、miniF2F团队，都走了。在大公司里，一个数学问题没法等十年，VP的政治周期比问题本身的周期短得多。
人真正稀缺的，是注意力。聪明人到处都有。赫伯特·西蒙1971年就说过，信息的丰富创造了注意力的贫乏。数学界不缺聪明的大脑。缺的是时间，读别人的证明、验证别人的工作、在别人的基础上继续建。
每个数学家一辈子能认真验证的证明数量是有限的。这个天花板不在智力上，在注意力上。验证这件事，以前要耗掉一个人的全部注意力。AI把这一块接过去了。
芯片行业里的情况看得更清楚。在那个世界里，设计和验证的人力比是一比三甚至一比四。验证工程师原来的角色是挑刺，找出哪里不对。AI能写证明之后，他们从挑刺的人变成了定方向的人。工作不再是逐行检查代码，是告诉AI这一行规范需要证明，你来。
有一个问题不能跳过。验证能确认你的事是真的。它不告诉你这件事值不值得说。判断哪个证明有意义，机器暂时还做不到。人在这个回路里最后的位置，不是验证者，是评判者。
两个领域，同一件事
回到开头那句"猜想廉价、验证昂贵"。
Carina让我看到这句话只说了一半。验证贵，不是贵在验证本身需要多少资源。是贵在人的注意力太少了。一个数学证明要等两年才审完，不是因为审稿人笨，是因为他们手上还有几十篇别的证明等着审。
验证能被AI自动化之后，昂贵的部分就消失了。剩下的不是"谁来做验证"的问题，而是每一次被精确验证的成功都变成了下一步训练的干净数据。这个正反馈才是Carina真正在建的东西。
她的公司做的是数学，但她赌的是更底层的东西：数据质量比数据量更值钱。形式化数学是第一个能被干净验证的领域。下一个是代码。再下一个是芯片。再下一个是所有依赖精确规范的工程领域。
路还很长。现在一行代码要配二十行证明，这个比值得降到一比一甚至更低才能大规模商用。但方向是对的。用AI去写那二十行证明。
Carina把这件事说得很轻。她说她做数学做了很多年，最难受的就是问题刚好卡在够不到的地方。
当验证这件事可以被机器无限量地完成时，最难回答的问题大概变成了：你提的猜想，还值不值得被验证？
