2024年5月，OpenAI的一个内部模型找到了Erdős单位距离猜想的一个反例。这个猜想自1946年提出以来一直悬而未决，许多专家都试图证明它，而OpenAI找到的却是一个反例。一个月后，OpenAI发表了对循环双覆盖（Cycle Double Cover，CDC）问题的证明，到7月又给出了另外十个开放问题的解答；9月，它又发表了对纳维-斯托克斯（Navier-Stokes）方程的证明。与此同时，Anthropic发表了费马大定理的形式化工作，并给出了黎曼猜想上的改进界。这些模型突然变得擅长数学了。
我感兴趣的问题是：我们能否预测这类模型会解决哪类问题？是什么让一个问题对LLM而言变得可处理，这些解答又有哪些共同点？如果AI解决问题的路径与人类不同，找出这种差异应当能帮助我们决定把AI朝哪个方向引导。关于单位距离反例的评论最为丰富，所以我们从这里开始。
问题复杂度
这里有一个简单的心智模型。要解决任何给定问题，你都需要一串提示或洞见，以及它们之间的工作。这个模型出人意料地贴合日常的简单问题，也贴合广义相对论这样的复杂思想。序列大致是这样的：洞见 → 时间／工作 → 洞见 → 时间／工作 → 解答。
专家需要的提示比新手少，因为他们有更多背景知识。在关于单位距离证明的评论中，WT Gowers使用了类似的想法：证明的难度，就是让专家能够重建该证明的最短提示序列。他称之为“模去专家的柯尔莫哥洛夫复杂度”。对单位距离问题，他的提示序列包含三部分：第一，寻找反例；第二，取已知最好的构造并将其推广；第三，尝试一系列次数递增的数域，但使用有界范数的素理想。
Gowers提出的复杂度公式是2^k + t，其中k是最短提示序列的长度，t是展开它所需的工作量。这是一个看起来很严格、直到你试图代入具体数字的公式，而这差不多正是重点所在。复杂度随着解决问题所需洞见数量的增加而呈指数增长。
大部分解题过程都是这些洞见之间的工作。你有一个顿悟时刻，然后花几个月把这条提示发展下去，直到下一次概念跳跃成为可能。对专家而言，花费的时间是这类工作的有用代理指标，这就是t。把第一条单位距离提示交给某人，他们仍然要做足够多的工作才能到达那个推广构造。
这个模型很有用，但它是事后性的。你无法看着一个问题就预测它需要x条提示。因此，问题的年龄、尝试次数以及附带的奖金，常被用来作为难度的代理指标。
给定提示的特征
典型的洞见会改变问题的表述方式，也就是问题被表示和理解的方式发生变化。有两点决定一条提示有多大价值：其一，它在被给出之前看起来有多不可能，而在给出之后看起来又有多显然——这比人们意识到的更难。在单位距离问题中，许多专家并不认为反例是可能的。其二，它在序列中的位置：提示是有序的。只有在对前两条提示的工作已经取得足够进展、使第三条提示变得可操作之后，第三条提示才有用。这也就否定了那种朴素的暴力思路：列出一千种数学技巧并尝试所有组合。提示序列遍历的是一棵树：最初的洞见改变问题，并揭示后续的选择。
人类以广度优先的方式解题
把k和t结合起来，你就得到了人类的搜索模式：生成候选方向，浅层探索，放弃大部分，再投入到少数几个上。如果一个有前景的方向没有尽早给出足够的鼓励，它就会被放弃。这是人类的一个约束：发展一个想法可能需要数月。在投入之前，研究者需要相信它会通向某处的理由：概念上的前景、早期结果，或在类似问题上的经验。发现这一点所需的时间越长，尝试这个想法的门槛就越高。
大多数研究软件的存在，就是为了通过自动化那些乏味、机械、可重复的工作来缩短这段时间。AI把这段时间缩短到了足以让搜索模式本身发生翻转的程度，而下游的一切都由此而来。
AI与复杂度
首先是t。模型相当于“努力”的东西是算力和token，它们花在单条轨迹上（测试时计算），或分散到并行智能体上（并行测试时计算）。预训练还提供了人类研究者必须自行查找或重建的知识。没有哪个专家知道此前每一项进展，所以偶尔会重复已经做过的事情。
更大的差异在于模型如何搜索：LLM是深度优先的。
给模型一个提示，它就会给出一个解答，可能正确，也可能不正确。要求它给出证明，它就会给出某种接近好证明的东西。这些模型的思维链也以贪心的深度优先方式运行，而且这个过程可以扩展。给并行智能体十种方法，你就会得到十个朝结论推进的尝试，它们也许彼此不同，也许有所重叠。每一个要么撞上路障，要么产出一个看起来正确的论证。放任不管，你就会得到漂亮的假证明。
这看起来像是在浪费算力和资源，直到你加入一个自动验证器，它可以剪除已完成的轨迹并识别出正确的那些。有了这个检查器，把巨额算力花在不确定的想法上就变得理性了：你几分钟内就能知道某个想法是否行得通。问题在于，验证器只能判断已完成的论证，它无法告诉你一个只发展了一半的想法是否有前途。
对比
如果你能在五分钟内知道一条提示是否有效，那么这条提示需要有多好？对人类来说，质量门槛很高，因为追求一条提示可能要花数月。对模型来说，这个门槛几乎消失了。提示可以是普通的、不太可信的，甚至是几乎不成形的。沿着它走下去，就能确定它是否通向某处。LLM让我们得以用时间换算力，并帮助我们在更短的时间内攻克更多问题。
失败的尝试对LLM而言也是提示
模型不需要一个确定的方向才能开始。预训练已经给了它关于问题历史和既往尝试的先验。每一个错误的解答都可以作为负向提示回传给模型，供下一轮迭代使用。系统会积累关于哪些做法已经失败、以及为何失败的指令。粗略地说，一个执行框架是这样的：起草器负责写出给求解模型的提示，这些提示基于模型先验、用于缓解此前运行的错误，并考虑到所有走进死胡同的有希望路径（这些是负向提示）；求解器接收提示，给出一个或多个候选解答，它可以运行多个子智能体，用并行测试时计算走不同路径；验证器／检查器则检查论证是否有效，是否确立了所要求的结果。
以CDC的提示为例：它先假设本任务存在一个完整的肯定性证明，从而防止模型把预训练中学到的该问题尚未解决这一状况当作停下来的理由。接着它列出若干不足以解决问题的替代品：特殊图类的证明、某些边被覆盖次数不是两次的循环覆盖构造、有界长度或指定循环的变体、归约到另一个未证明的猜想、对任何固定图规模的计算机验证，以及没有完整不存在性证书的候选反例。它还要求全程使用对抗性智能体：每个候选证明都必须检查是否恰好两次重数、是否有伪装成循环的重复边闭迹、平行边2-循环、不连通图、割点、归约引入的桥，以及是否循环使用了等价的CDC陈述。此外还有一句针对习得性懒惰的话：“不要仅仅因为当前方法失败或智能体报告了定理级别的缺口就返回。”
OpenAI很可能进行了多轮尝试，起草器收集错误和失败的想法，引导下一轮迭代避开它们。这里的每一行都是一条失败路径，被写成了指令。
重建单位距离证明与Tsimerman的工作
让我们通过这个执行框架的视角重读Gowers的三条提示。第一条，寻找反例：这真的很难，因为学界和模型的预训练先验都认为该猜想为真。起草器最可能是由于求解器在追求证明时不断失败才得出了这条提示。这个框架阻止模型把公认观点当作它必须追求的方向。每一次失败尝试都让反例显得不那么不可能。第二条，取已知最好的构造并将其推广：这最接近学界先验，是标准动作。实质性的工作是把推广发展到足以发现它允许什么，这是t很大的那一步。但请注意，这是一个反例的推广，而几乎没人在找反例。第三条，尝试次数递增的数域：一旦前两条提示建立了它适用的空间，这就是标准工具。
顺序很重要。从第三条开始，你甚至不知道这项练习是要做反证。跳过推广构造，第三条就没有作用对象。而即便三条提示齐全，工作量依然巨大。反例这条提示事后看来很明显，这让人不禁要问为什么没人试过。事实上，有人试过。
最近被OpenAI聘用的Jacob Tsimerman研究过这个反例。他懂数论，甚至考虑过提高次数，然后他停下了。寻找反例是第一个洞见，但那只是开始。阻止他的不是缺乏技能，而是一种恰如其分的清醒感受：一个人已经在沼泽里走了好几周，却没有任何证据表明另一边还有岸。用他自己的话说：“这是一种非常可怕的动态，很难想清楚解析区域并保持引导性直觉，耗费大量时间，而且经常不成功。”
心理学早在几十年前就发现了问题解决的这一人类侧面：Metcalfe和Wiebe每隔十五秒询问解题者觉得自己离解答有多近，在普通问题上，他们报告出的进展感会上升；在顿悟型问题上，这种感觉一直平缓，直到他们找到答案。他们报告不出任何能支撑搜索的进展感。顿悟型问题没有梯度。在解决之前，你不知道自己离答案有多近。
因此，专家面临的问题有两重：是否有人真的进入这个分支（即提示），以及进入之后，他们是否停留足够久，让普通的胜任能力完成工作。停留的代价是工作记忆、士气和职业生涯。而在一条所有已知专家都认为错误的路线上停留，会把这三者叠加放大。对LLM来说，这是一个巨大优势。用Arul Shankar的话说：“模型很快过了一遍各种想法，但当它到达那个关键想法时（在以‘乐观地假设……’开头的那段里），它相当有条不紊地锁定到了证明上。”
这可以压缩成两个问题：一个问题需要多少洞见，以及在你能判断一个方向是否值得之前，这些洞见之间有多少工作。Tsimerman这样描述AI这一侧：“这也许指出了AI系统拥有优势的一种方式：不仅仅是它们能尝试所有已知方法，还在于它们能比数学家玩得更久、在更险恶的水域中前行而不被压垮。当然，这一点目前还不稳健地成立，但这也许是一个预示性事件。”
其他证明
OpenAI对纳维-斯托克斯方程的证明展示了同样的过程。根据粗略阅读，它把已完成的工作推进到了完成……（原文在此处截断）。这一点值得作为警示保留：关于这些模型在数学上能力的叙述仍在展开，其中一些说法来自近期、尚未经过完整同行评审的材料，因此应当审慎对待，而不是当作定论。不过，那种逐渐显现的模式——深度优先的搜索、廉价的验证、由失败尝试构成的负向提示，以及把时间换成算力——确实有助于解释为什么某些开放问题如今对AI而言变得可处理，以及接下来应当把AI指向哪里。