LLM猜想生成与证明检查：谁更胜一筹

第二杯和第三杯咖啡之间，最近不少计算复杂性理论研究者读到了一句他们从没想过会看到的话：一个确定性算法能在大约 2^(n/√(log n)) 的时间内，统计任意布尔公式的可满足赋值数量。这是次指数级的，恰好符合推翻指数时间假设（ETH）的技术定义，而ETH正是这个领域的承重假设之一。这个结论并非出自某个大学团队发布在arXiv上的论文，而是来自一家AI实验室，证明是与一个大语言模型协作完成的。不管你如何看待这次发布，它标志着猜想生成（机器提出新数学，而不只是给数学打分）已经走出了演示阶段。

该实验室一次放出了三项成果：上面那个复杂性理论的重磅结果；一个声称对所有维度都成立的Kakeya猜想证明；以及一项被描述为“标准模型的统一补全”的物理学成果，但在完成形式化验证之前暂不公布。反应呈现出熟悉的分裂：内容本身让人惊叹，包装方式却让人反感。有人把这事比作自行车制造商宣布自己赢得了自行车赛。很贴切，不过成果本身值得放慢脚步看看，因为这则公告背后藏着一个真正的启示：语言模型接触数学的方式有两种截然不同的路径，而你究竟该信哪一种，值得细想。

AI数学公告究竟声称了什么

先从复杂性结果说起，因为它的利害关系最清晰。指数时间假设大致说的是：3-SAT 不可能在 2^o(n) 的时间内求解，也就是说，没有任何算法能在变量数量上做到有意义的次指数级。参数化复杂性和细粒度复杂性领域有数百篇论文依赖ETH来证明下界，它是那种你可以把整个职业生涯的“以ETH为条件”的定理一层层堆在上面的假设。新预印本描述了一个针对k-CNF公式的确定性计数算法，它使用多项式空间，运行时间为 2^(n/(log n)^(1/2+o(1))) 乘以一个多项式因子。这个指数是o(n)，恰好是ETH所禁止的。这个算法依然慢得离谱，没人会真的拿它去跑实际实例，但从渐近意义上看，它是决定性的。如果证明成立，那么一个支撑了二十年下界研究的假设，就将不复存在。

第二项声明针对的是Kakeya猜想，这是几何测度论中的一个问题，关心的是包含每个方向单位线段的最小集合。三维情形直到2025年才被攻克，Hong Wang和Joshua Zahl的这项著名证明被许多人视为职业生涯的巅峰之作。此次公告声称在所有维度上都给出了证明，这将完全涵盖那项突破。第三项成果属于量子场论，是三者中最模糊的一个：被描述为“标准模型的统一补全”，却尚未发布，据称正在等待机器可检验的形式化。读过预告的物理学家怀疑，它更像是某类大统一式构造，而不是字面意义上的万物理论，措辞也确实值得打个问号。

这次发布有两点值得肯定。实验室在公开之前就邀请了职业数学家和物理学家参与，这是对此前一次更笨拙的数学公告引发的反弹的直接回应，Terence Tao等人之后也公开呼吁过这类协作。另外，物理成果在形式化完成之前被扣留，这才是正确的优先级排序。但仍有不少硬问题没有答案：外界不知道算力成本有多高，也不知道如果同样的经费投入人类研究者，能否产出同样的定理，更不知道一家以营利为目的的实验室，在股东投票之后还会不会继续资助出于好奇心的研究。批评者还立刻指出了一个令人不适的循环：这些模型的部分训练数据，正是来自那些如今被要求为其成果鼓掌的研究社区的问题、草稿和论坛帖子。

证明检查与猜想生成：两种不同的工作

撇开炒作不谈，所有AI数学系统做的其实只有两件事之一。第一件是证明检查：给定一个候选论证，判断它是否有效。第二件是猜想生成：给定一个问题领域，提出值得尝试的方向，比如一个引理、一种构造、一个算法或一个反例。两者听起来像是同一种技能的两半，其实不然。它们是不同的计算问题，有不同的“神谕”，不同的失败模式，也有截然不同的可信度特征。把两者混为一谈，结果要么是过度相信新闻稿，要么是无视真正的进展。

检查有神谕可依。用Lean写的证明，要么能通过内核编译，要么不能，内核才不管作者说话多有底气。检查的失败是响亮的，被拒绝的战术块毫无歧义。生成则没有神谕。一个提出的猜想可能是真的、假的、平凡为真，或者是“真的，但1987年就以不同记号发表过”。生成的失败是悄无声息的，而且其失败模式带有社会属性：听起来很像那么回事的胡说八道，或者把真正的成果包装成新奇发现。这里的质量由重要性和原创性衡量，而这两个属性是由人类的品味定义的，而非任何可判定的标准。

为什么生成能力突然好到值得关注了？因为现代推理模型是通过训练获得长链思维的，而不只是靠提示引导出来的。在可验证奖励上做强化学习，主要使用数学和代码这类答案可以机械检验的领域，让这些系统真正学会在步骤空间中搜索，而不只是逐字自动补全。我建议你记住这个类比：证明检查器像编译器，猜想生成器像设计师。两者都有价值。但你绝不应该让设计师自己给自己的作品盖章。

无法检验的证明是布道，无法检验的猜想只是传言。

自动证明检查的优势领域

只要存在形式化的基准真相，而被审查的产物又太长或太繁琐、人无法逐行审计，检查器就占优。Lean 4及其社区数学库Mathlib已经成为这一领域事实上的竞技场：你用一门编程语言写下定义和证明，一个小巧且可以单独审计的内核来判定每一步推理是否合法。可信计算基相对于其上构建的庞大数学体系而言极其微小，而这正是你想要的那种不对称。

实践中的闭环大致是这样的：模型起草战术级的证明步骤，内核逐条接受或拒绝，拒绝信息又作为上下文反馈给下一次尝试。这正是把模型输出约束到严格语法能立刻见效的场景。你采样出来的战术永远语法有效，因此整类幻觉在构造上就被排除了。下面是一个最简单的例子，就是模型现在几秒钟就能搞定的那种引理：

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

注意这个例子展示了分工的哪些方面。创造性的一步是选择见证项 k + l；检查的一步是由 ring 验证代数运算。人和模型在第一步上都还不错。只有内核在第二步上是可信的，而且它从不疲倦、从不跳读，也从不凭感觉打分。整个公告中最可信的部分恰恰就是这道关卡：据称物理论文是在Lean形式化完成之后才被暂时扣留的。如果这个说法属实，那就说明工作流程正按设计运转，机器提出，机器裁决，新闻稿则排队等候。

猜想生成的优势领域

只要搜索空间是组合式的，而评估又很便宜，生成就占优。DeepMind的FunSearch在2023年确立了这一范式：语言模型提出程序形式的假设，快速评估器为其打分，进化循环保留最优者。这套方法为cap set问题找到了新构造，也得到了比几十年手工调优更好的装箱启发式算法。AlphaEvolve将同一思路推得更远，其中一项成果是把一个自Strassen时代起就保持不变的4×4矩阵乘法算法减少了一次乘法。没人声称这些系统理解几何。它们并不需要理解。它们只需要提出方案，而评估器必须诚实。

ETH算法的情况几乎异常地符合这一模式。“算法思路”的空间极其庞大，而人类研究者探索它时带着很强的先验，这是说得客气些的“盲区”。一个需要将某种特定表示技巧与某种特定递归结构组合起来的构造，可能会沉睡三十年，仅仅因为没有人的搜索路径曾经经过它附近。穷举的、不带先验的、有点“笨”的搜索，正是机器带来的东西。同样的逻辑也支撑着“生成-反驳”循环：提出一个猜想，立刻尝试用计算搜索在小规模案例中寻找反例来推翻它。大多数猜想几分钟内就会被推翻，这完全没问题。每次反驳都让下一次提议更加精准，而幸存下来的，才值得人类花一个下午去研究。

还有一种心理上的不对称值得尊重。Wang和Zahl的三维Kakeya证明耗费了顶尖研究者多年的专注投入。如果模型辅助的搜索真的产出了一个适用于所有维度的论证，那它几乎肯定走了一条不同的路径穿越这片领域，不一定更深，但确实不同。而“不同”正是搜索的意义所在。真正的危险不在于机器生成猜想，而在于有人在没有配套验证机制的情况下，把生成的猜想直接发表了出来。这就引出了你真正需要搭建的那部分流水线。

搭建AI生成证明的验证闭环

如果你想享受机器生成数学的好处，又不想丢人现眼，那么工作流程比模型本身更重要。以下是我会按顺序运行的流水线：

1. 广泛且廉价地生成。这一阶段多样性比深度更重要；你要的是覆盖整个思路空间，而不是一次精雕细琢的尝试。
2. 对照文献去重。检索arXiv和MathOverflow，可以抓住最常见的失败：一个“新”猜想其实是换了生僻记号的已知结果。
3. 应用廉价的经验过滤。对小规模案例做数值测试，用计算方法寻找反例，让那些明显错误的命题尽快被淘汰。
4. 将幸存者形式化。可以用Lean、Isabelle或Rocq，任你选择证明助手，但要明白，这是最昂贵的一步，而自然语言证明只是草图，不是结果。
5. 人工审查新颖性与表述。这真的重要吗？这个命题本身选对了吗？模型优化的是“什么可以被证明”，而人类决定“什么值得被证明”。

此次公布的合作大致遵循了这一结构：研究者在发布前就被请来，实际上承担了第五步的工作。这相比过去那种“扔出一篇预印本，让社交媒体来评判”的做法确实是进步。但注意流水线中的不对称：前三步便宜，且随算力扩展；第四步是瓶颈；第五步根本无法扩展。如果你要在这个领域构建工具，就把钱花在瓶颈上，比如更好的自动形式化、把错误反馈更好地回传给生成器，而不是去做一个更大、更自信的生成器。

为什么人类数学家仍然把关正确性

没有任何验证器能告诉你一个定理是否重要。问题选择靠的是品味，而品味是几十年间逐渐形成的社会性技术，包括研讨会、审稿意见，以及关于哪些问题能打开大门、哪些是死胡同的缓慢共识。研究社区对厂商公告的怀疑，并不只是为了守门，而更像一种免疫系统。免疫系统偶尔会过度反应，恰恰是因为反应不足是致命的。

再说说出处问题。这些模型是在社区自身的问题、草稿和论坛帖子上训练的，这就带来一种令人不安的可能性：一项备受赞誉的“发现”，可能只是其未来审稿人写过的东西的重组。担心自己的工具抢了自己的风头，这并非多疑，而是数据溯源问题。在实验室能证明溯源之前，人类审稿人仍是唯一有效的抄袭检测器。再加上署名的政治，比如谁被邀请参与验证、谁的名字出现在公告上、关于偏袒的指控，你就能明白，人类这道关卡为什么去不掉。挑选五位杰出科学家为一项结果背书，与其说是认识论上的行为，不如说同样是政治行为。

最后提醒一句：如果有人想把排行榜当成研究能力的证明，请注意，竞赛金牌衡量的是在为数小时内可解而精心设计的题目上的表现。研究的题目分布恰恰相反：题目之所以被选中，正是因为没人知道它们究竟能不能被解决。这也是为什么基准测试漏掉了软件工程中大部分真实工作的原因：指标奖励的是被塑造过的问题，而不是混乱的真实问题。一个能在奥赛题上拿满分的模型确实展示了某种真实能力，但它并没有展示判断力。

建议：信任闭环，而非模型

我的立场直说：猜想生成是真实的、有用的，并且只会越来越好；但未经验证的猜想生成毫无价值，没有形式化背书的自然语言证明，在被证明之前都应当当作营销来看待。当产物必须被相信时，证明检查每次都胜出；当瓶颈是想象力而非严谨性时，生成每次都胜出。真正重要的公告，是那些把两者牢牢焊接在一起的公告。

所以，请把模型当作一个高产、精力无穷、却毫无判断力的初级合作者：它交给你的任何东西，在进入论文之前都要先过证明助手，在进入引言之前都要经过一位有品味的人类审查。如果你是研究者，请认真学会一种证明助手，因为形式化是瓶颈，而能驾驭它的人很快就会变得非常忙碌。如果你在做工具，就去搭建闭环，而不是只做演示。下一次重磅公告出现时，别急着看新闻稿，打开预印本，看看Lean仓库是否存在。能经得起考验的声明，都是那些已经经过机器检验才到来的。