跳到正文
Latent Space· Ankit Maloo·· 3 小时前精选AI 评分78

AI 为何突然擅长数学:从 OpenAI 反例证明看人类与模型的搜索差异

AI Is Getting Good at Math. Here’s Why.

AI 导读

Latent Space 作者 Ankit Maloo 分析 OpenAI 与 Anthropic 今年公布的一系列开放数学问题成果,包括 OpenAI 内部模型对 1946 年提出的 Erdős 单位距离猜想的反例、Cycle Double Cover 证明、166 页 Navier-Stokes 证明(88 小时内动用 10。

推荐理由

作者用提示序列和分支因子框架解释为何模型能解开放数学题,读者可据此判断哪些问题适合交给 AI。

正文 · AI 翻译

今年5月,OpenAI的一个内部模型找到了埃尔德什单位距离猜想的反例。该猜想自1946年起悬而未决。许多专家曾试图证明它。OpenAI却找到了一个反例。一个月后,OpenAI发表了循环双覆盖(CDC)问题的证明,到7月又解决了另外十个开放问题。9月则给出了纳维-斯托克斯方程的证明。Anthropic发表了费马大定理的形式化,以及黎曼假设的改进界限。这些模型突然擅长数学了。

我感兴趣的问题是,我们能否预测这些模型会解决哪类问题。是什么让一个问题对LLM来说变得可解,这些解法有什么共同点?如果AI解决问题的方式与人类不同,找出这种差异应能帮助我们决定该把AI指向何处。单位距离反证获得的评论最为丰富,所以我们就从那里开始。

问题复杂度

这里有一个简单的心智模型。要解决任何给定的问题,你需要一系列提示或洞见,其间穿插着工作。这出人意料地适用于简单的日常问题,也适用于像广义相对论这样复杂的思想1(见附赠部分)。这个序列大致是这样的:

洞见 -> 时间/努力 -> 洞见 -> 时间/努力 -> 解决。

专家需要的提示比新手少,因为他们拥有更多背景知识。在对单位距离证明的评论中,WT Gowers使用了类似的想法:证明的难度,就是能让专家重建该证明的最短提示序列。他称之为模专家后的柯尔莫哥洛夫复杂度2。对于单位距离问题,他的提示序列包含三部分:

  1. 寻找一个反例。

  2. 取已知的最佳构造并将其推广。

  3. 尝试一列次数递增的数域,但使用有界范数的素理想。

Gowers提出的复杂度公式是2^k + t,其中k是最短提示序列的长度,t是展开它所需的工作量。这种公式看似严谨,直到你试图往里代入具体数字,而这差不多正是要点所在。复杂度随解决问题所需洞见数量呈指数增长。

大多数问题解决都发生在这些洞见之间的工作里。你有了一个顿悟时刻,然后花数月时间发展提示,直到另一次概念飞跃成为可能。对专家而言,花费的时间是衡量这种工作的有用代理,因此有了t。把第一个单位距离提示交给某人,他们仍然必须做足够的工作才能达到那个推广构造。

有用,但属于事后分析。你无法看着问题就预测它需要x个提示。因此,问题的年龄、尝试次数以及附带的奖金是描述难度的常见代理。

给定提示的特征

一个典型的洞见会改变问题的表述。问题的表示和理解会发生变化。两件事决定了一个提示有多大价值:

  • 在提供提示之前它看起来有多不可能,与提供提示之后它看起来有多显然 → 这比人们意识到的更难。在单位距离问题中,许多专家并不认为反例有很高可能性。

  • 它在序列中应有的位置:提示是有顺序的。只有在对前两个提示的工作取得足够进展、使第三个提示变得可操作之后,它才有用。这挫败了那种天真的暴力思路:列出一千种数学技巧并尝试每一种组合3。提示序列遍历一棵树。最初的洞见会改变问题,并揭示后续的选择。

人类以广度优先的方式解决问题

把 k 和 t 结合起来,就得到了人类的搜索模式。生成候选方向,浅尝辄止地探索它们,放弃大部分,并坚定投入少数几个。如果一个有希望的方向在早期没有给出足够的鼓励,它就会被放弃4。这是人类的一种约束:发展一个想法可能需要数月。在投入之前,研究者需要有理由相信它会通向某处:概念上的前景、早期结果,或对类似问题的经验。找出答案所需的时间越长,尝试这个想法的门槛就越高。

大多数研究软件的存在,就是为了通过自动化那些枯燥、机械、可重复的工作来缩短这段时间。AI 把它缩短到了足以让搜索模式本身发生翻转的程度,而下游的一切都由此而来。

AI 与复杂度

首先是 t。模型相当于努力的,是计算量和 token,花费在单条轨迹上(测试时计算)或分散在并行 agent 上(并行测试时计算)。预训练还提供了人类研究者必须去查找或重建的知识。没有哪个专家了解此前的每一项进展,所以偶尔他们会重做已经做过的事情。

更大的区别在于模型如何搜索:

LLM 是深度优先的

给模型一个单独的提示,它就会给你一个解答。也许正确,也许不正确。要求一个证明,它就会给你一个接近良好证明的东西。这类模型的 CoT 也以贪心的深度优先方式运行。而且这个过程可以扩展。给并行 agent 十种方法,你就会得到十个朝着结论发展的尝试。也许全都不同,也许有些重叠。每一个要么撞上障碍,要么产生一个看起来正确的论证。放任不管,这会让你得到漂亮的错误证明。

这看起来像是在浪费计算量和资源,直到你加入一个自动验证器5,它可以修剪已完成的轨迹并识别出正确的那些。有了这个检查器,把巨量计算花在不确定的想法上就变得合理了。你可以在几分钟内弄清楚某个想法是否可行。问题在于,验证器只能评判已完成的论证。它无法告诉你一个只发展了一半的想法是否会通向某处。

对比

如果你能在五分钟内弄清楚一个提示是否有效,那它需要有多好?对人类来说,质量标准很高,因为追求一个提示可能需要数月的工作。对模型来说,这个门槛几乎消失了。提示可以是普通的、不太可信的,或者几乎还没成形的。跟着它走就能确定它是否通向某处。LLM 使我们能够用时间换计算量,并帮助我们在更短的时间内研究更多问题。

失败的尝试对 LLM 来说是提示

模型不需要一个确定的方向就能开始。预训练已经赋予了它对问题历史和过往尝试的先验。每一个错误的解法都可以作为负面提示返回给模型,用于下一次迭代。系统会不断积累关于哪些做法已经失败以及失败原因的指令。大致上,一个执行框架看起来是这样的:

  • 起草器:编写给求解器模型的提示。这些提示基于模型的先验,规避此前运行中的错误,并考虑到所有最终无果的有希望的路径(这些是负面提示)。

  • 求解器:接收提示并给出一个或多个候选解。它可以运行多个子代理,并利用并行测试时计算探索不同的路径。

  • 验证器/检查器:检查论证是否有效,并确认所要求的结果成立。

例如,考虑这个CDC 提示:

为本任务的目的,假定存在一个完整的肯定性证明。 → 这阻止模型把预训练中学到的问题的未解决状态当作停止的理由。

特别地,针对特殊图类的证明、某些边覆盖次数非两次的圈覆盖构造、有界长度或指定圈的变体、归约到另一个未证明的猜想、对任何固定图规模的计算验证,以及没有完整不存在性证书的候选反例,都是不充分的 → 这排除了一系列代替解决实际问题的替代品。

全程使用对抗性代理:每一个候选证明都必须检查是否恰好两次重数、伪装成圈的重边闭合迹、平行边 2-圈、非连通图、割点、归约引入的桥,以及循环使用等价的 CDC 陈述 → 将已编目的失败模式提升为常规检查。

再加一行针对习得性懒惰6 的话:不要仅仅因为当前方法失败或代理报告了定理级别的缺口就返回

OpenAI 很可能进行了多轮尝试,起草器把错误和失败的想法拿来,引导下一次迭代避开它们。这里的每一行都是一条失败路径,被写成了一条指令。

重建单位距离证明与 Tsimerman 的工作

让我们通过执行框架的视角重新审视高尔斯的三条提示:

提示 1:寻找反例:这确实很难,因为学界和模型的预训练先验都认为该猜想为真。起草器最可能得出这一点,是因为求解器在寻求证明时不断失败。这种表述阻止模型把公认观点当作它必须追寻的方向。每一次失败的尝试都让反例的可能性略微增加。

提示 2:取已知最佳构造并推广它。最接近学界先验;这是标准做法。大量工作在于将推广推进到足以发现它允许什么。这是大 t 步。但请注意,这是对一个反例的推广,而几乎没人在寻找反例。

提示 3:尝试次数递增的数域。一旦前两条提示构建出适用空间,这就是标准工具。

顺序很重要。从提示三开始,你甚至不知道这道题是反证法。跳过广义构造,提示三就无从下手。即使三个提示都有,工作量仍然巨大。反例提示事后看来显而易见,这让你不禁要问为什么没人试过。事实上,有人试过。

最近被 OpenAI 聘用的 Jacob Tsimerman 研究过这个反例。他懂数论。甚至考虑过提高次数。然后他停下来了。寻找反例是第一个洞见。但这仍然只是开始。拦住他的不是技巧不足。而是一种恰如其分的清醒感受——一个在沼泽里跋涉数周、却没有任何证据表明对岸存在的人所拥有的感受。用他自己的话说:

“一种非常可怕的动态,很难在解析区域中思考并保持直觉引导,耗费大量时间且常常无果。”

Jacob Tsimerman,OpenAI 数学家

心理学早在几十年前就发现了问题解决中人的这一面:Metcalfe 和 Wiebe 每十五秒问一次解题者觉得自己离答案有多近,在普通问题上7他们报告的进展感会上升。在洞见问题上,这种感觉一直持平,直到他们找到答案。他们报告说没有任何进展感来支撑搜索。洞见问题没有梯度。在解出来之前,你不知道自己离答案有多近。

所以专家问题有两层:究竟有没有人进入这个分支(提示),以及进入之后,他们是否停留足够久,让普通能力完成这项工作?停留的代价是工作记忆、士气和职业生涯。而停留在一条所有已知专家都认为错误的路径上,会同时放大这三者。对 LLM 来说,这是一个巨大的优势。Arul Shankar 说:

“模型很快就过了一遍想法,但当它到达关键想法时(在以‘乐观地假设……’开头的那一段),它相当有条不紊地瞄准了证明。”

这可以压缩成两个问题:一个问题需要多少洞见,以及在你能判断一个方向是否值得之前,这些洞见之间有多少工作?Tsimerman 给出了 AI 这一侧的看法:

“这可能表明 AI 系统拥有优势的一种方式:不仅仅是它们能尝试所有已知方法,还在于它们能比数学家坚持更久、在更险恶的水域中游弋,而不会不堪重负。当然,这一点目前还不能稳健成立,但这可能是一个预示性事件。”

其他证明

OpenAI 对 Navier-Stokes 的证明展示了同样的过程。粗略读来,它把 Córdoba 和 Martínez-Zoroa 的工作推进到了完成。证明长达 166 页,包含许多修正和大量复杂数学,但就概念跳跃而言,它提供的并没有那么多。8  Anthropic 在 Fermat 和 Riemann 上的工作附有丰富的评论,它展示了同样的骨架:数百个失败的想法、一个编排器下的多个代理、到处是脚本和检查器。以及少量承担重任的概念跳跃。

今年模型发生了什么变化?

三种具体能力叠加在一起。它们帮助推动了这些证明。

  • 模型现在擅长串联原语。最近的训练目标专注于在步骤 1 创建可用于长视野任务第 n 步的产物。=> 这降低了 t。

  • 自我验证:模型现在能在人类甚至验证器看到输出之前,捕捉轨迹中错误的步骤(不是那些语法上有效但无结果的步骤)。OpenAI 专门在数学验证上训练模型,使用大规模真实世界示例和一个识别证明中错误的验证层。=> 这使得轨迹内的剪枝更便宜。

  • 编排。模型可以指挥子代理,使用记忆等工具能力进行引导和消除错误路径,以及代理之间的协调。=> 这就是负面提示积累的方式。

分支因子

重新审视 Gowers 的公式。他指出该公式遗漏了一件事:探索潜在提示树所需的时间。将在每一步可能的下一步提示的数量称为分支因子 b。在每一步有 b 个可能的提示时,k 个提示意味着 b^k 条路径。对于人类,品味和判断使有效的 b 保持较小,大多数分支默认被丢弃。9  

AI 必须在每个中间步骤追求几乎每一个可能的分支,但它可以快速完成。这预测模型会在 b^k x 计算成本(其中 k 是提示数量)较小的地方表现良好。这回答了我们开始的问题。网络安全看似复杂,但它首先被攻克,因为中间步骤的分支因子10大约是 1-2。

专业人士需要很多技能,但解决方案的样子是事先已知的。这也解释了为什么寻找反例如此强大。那收缩了解决方案空间和 b。同样的模式反映在一个社区努力中,即引导代理寻找所有开放问题的反例。

验证器修剪已完成的分支。起草者修剪未来的分支,通过告诉求解器哪些路径已经失败来缩小搜索空间。在中间时,你没有任何修剪信号。自我验证捕捉错误的步骤,而不是那些语法正确但无结果的步骤。没有梯度,你必须探索所有分支。Tsimerman 在士气上付出了代价,AI 公司会在计算上付出代价。实验室会选择解决方案空间狭窄的问题来展示他们的模型有效。11

从中得出的一个直觉:预计 AI 模型将非常擅长将想法完成到终点,当概念飞跃已经完成,剩下的是繁琐、复杂的数学时。也就是说,当 k 和 b 不是高得离谱时。最近发表的许多其他证明符合这一点。Navier-Stokes 的证明完成了 Córdoba 和 Martínez-Zoroa 的程序,即使那也用了 10,000 个代理,在 88 小时内总共使用了 300B 个 token。

如果人类在任何地方保持优势,Gowers 预计会在“搜索树很深且分支量很大,以至于没有严格修剪搜索甚至对计算机都不可行”的问题上。换句话说,高 b 和/或高 k 在人类直觉仍然重要的地方。

一个有趣的分歧

人类会谨慎选择自己的方法,然后花费数月时间投入其中。一个失败的方法之所以富有洞见,恰恰是因为有人足够确信,愿意为之投入数月。专家断然拒绝的方法也是如此。拒绝之中蕴含着他们的判断和洞见。无论哪种情况,追随一个想法都会改变我们对问题的理解。即便是死胡同,也能给专家留下有用的思考工具。

有了AI,解决方案之所以出现,是因为模型会走完每一条看似可行的路径。失败的代价很低。大多数失败都很幼稚,有些可能很有意思。失败中所含的信息量,与其背后的确信程度成正比。不过我们很少有机会看到这些失败,更不用说理解某次尝试为何失败了。CDC提示词大概是我们最接近的一次——所有失败都列在提示词本身里。

这种差异有助于形成一种良性的互补。人类擅长缩减分支。模型擅长缩短修剪单个分支所需的时间。专家可以先让模型把一个想法从头到尾探索一遍,再决定它是否值得花三个月。需要大量洞见的问题,也就是k值很大的问题,对两者来说都很难。专家可以利用模型的失败尝试以及自己建立确信的过程来缩小范围。

不过,许多开放问题的提出,是因为解决它们能增进我们对这一领域的理解。其中一部分来自直接攻关,另一部分来自了解为何那些高确信度的方法失败了。模型最终可以生成证明。12失败中蕴含着大量洞见。只有我们能看到这些失败,这种互补才能成立。

Terence Tao 描述解决问题是数学更深层目的——发展我们的理解——的一种代理。一个结果或一个证明是一场社群事件,促使人们去解释新想法、把它们与已有想法联系起来,并推动我们 collective intuition 向前。只宣布最终答案,是把目的地误当成了旅程。 

附加问题:LLM能否提出广义相对论?

人们曾提出(Demis、又一次、Zahavy、Adam Brown),检验AI是否跨过门槛的一个方法是用截至1901年的数据训练模型,看它能否提出广义相对论。我现在认为,如果研究者在这件事上古德哈特,那会很快。这个飞跃并不需要很多提示。

第一个有效的提示是把引力视为几何,这足以缩小解空间。之后的数学极其困难,而这正是模型擅长的领域。这个提示极其反直觉,我认为CoT只有在穷尽其他一切可能之后才会落到它上面。试试把引力当作一种力,当作平直空间中的场,当作对牛顿平方反比定律的微调。每一次尝试都会与1901年已知的某些东西相矛盾,最著名的是水星近日点。

每一次失败都让几何解释变得稍微更有可能。它可能会提出数百个看似可行的理论,但我们会验证这一个,然后说:“对,它做到了。”

1

  1907年,爱因斯坦有了他所谓的“一生中最快乐的想法”:一个人从屋顶坠落时感觉不到自己的重量。之后他又花了八年时间,并且在一位真正懂几何的朋友的帮助下,才把它变成方程。这就是两个洞见之间那支箭的样子。广义相对论需要两到三个主要洞见。首先是,把引力当作几何来对待。爱因斯坦与之相伴多年,推进了这一点,然后大约八年后得到了最终理论。问题在于,当时人人都相信牛顿定律神圣不可侵犯,所以说牛顿错了需要巨大的信念和信仰。C.P.斯诺曾说,狭义相对论“是一个注定会出现的想法。但广义理论则完全是另一回事。”这就是一个不令人振奋的提示和一个非常令人惊讶的提示之间的区别。

2

  柯尔莫哥洛夫复杂度要求给出能产生给定输出的最短程序;在这里,专家提供背景知识。

3

  这比宇宙中的原子数量还多出更多的排列组合,也远远多于愿意苦熬下去的研究生人数。

4

  这也是为什么不同人类文化都非常强调坚持。Tsimerman如果再多坚持一点,本来可能解决这个问题。无意冒犯,但在这篇文章后面,他解释了自己在如此接近时是什么感受。题外话:对于三个月一个想法,一个研究者在其一生中最富产出的十年里也许会有二十次认真下注,而大多数人都很希望其中一次能成功。

5

  我有这样一个理论:无限只猴子在无限台打字机上可以打出莎士比亚和许多其他小说,外加一些原创作品。但是,要知道它们是否做到了,你需要一个验证器。而验证器也很可能会拒绝它们同时创作出的所有原创作品。道格拉斯·亚当斯对此有一句话:“福特,外面有无限只猴子想和我们谈谈它们写出的《哈姆雷特》剧本。”

6

  不得不对一台机器写下这样的话,本质上是一张写着“不,真的,继续”的便条,这本身就很奇怪;而更奇怪的是它居然有效。

7

  我不认为每15秒问一次有效。即使我觉得自己已经很接近了,我也会说不。

8

  这显然是一个早期结论,但我没有看到关于这些概念跳跃的丰富评论。

9

  和许多事情一样,品味和判断来自先验。而先验可能是错的。正如我们在单位距离反例本身中看到的那样。在Gowers自己的叙述中,“我从未想过要试图推翻它。”这一先验把正确的分支推向了低概率,许多专家没有选择那条路。

10

  文献中已经存在一条利用链。模型只需要填空即可。

11

  或者谁知道呢,他们可能会发布一个模型,花了四百亿亿美元发现一个问题很难,而且有太多方法无法解决它,于是转而满足于另一个结果。

12

  道格拉斯·亚当斯早就预言了这一点。“我非常彻底地检查过了,”计算机说,“那确实就是答案。老实说,我认为问题在于,你其实一直都不知道问题是什么。”

来源:Latent Space · latent.space