跳至内容
JIROLOGY/ DAILY
JIROLOGY DAILY · LONGFORM

人类掌舵、AI探路:KLS猜想获证,关键判断仍在研究者手里

· Xinzhi Zhang · 约 8 分钟

阅读原始内容 ↗ · 飞书归档 ↗

JIROLOGY / LONGFORM10.22READ DEEPER / 8 MIN
精读编辑封面 · 非新闻摄影

核心观点

想让AI攻克一道数学难题,最好的办法是让它从头跑到尾吗?微软研究院近日的一篇博客给出了一个不同的案例。文章介绍,微软研究院机器学习与优化组的Xinzhi Zhang与合作者证明了1995年提出的KLS猜想:对一大类高维概率分布,用平面切割找到的“瓶颈”,与任意形状的最佳切割相差不超过一个通用常数,而且这个常数不随维度增长。此前最好的结果,仍允许这个界随维度缓慢变大。切割的几何决定随机游走探索分布的快慢,因此这个问题牵动着大量高维随机算法的效率。

证明过程中,多个AI智能体并行探索了一百多种候选思路,研究者检查中间结果、剪掉没有希望的方向;作者强调,递归判据、反复细化和误差有界的证明是研究者的原创,AI负责探索、推导与检查;关键一步是把递归细化反复执行,并证明累积误差有常数上界。作为对照,用大致相同的预算让领先模型无引导地反复尝试,没有达到目标。另有专家同日独立发表了完整证明,随后还出现了形式化验证。需要记住,这是一篇成果介绍,证明细节要以论文为准;那次对照也只是同一项目里的一次比较。

重点观点

  1. KLS猜想于1995年提出,预测在高维分布上,平面切割与任意形状的最佳切割之差不超过一个通用常数,与维度无关。
  2. 切割的几何决定随机游走探索一个分布的快慢,所以这个猜想处在高维采样理论的中心。
  3. 文章称新证明给出了固定的界;此前最好的结果仍让界随维度缓慢增长。
  4. 作者先在人主导的流程里与AI智能体探索了100多种候选方法,得到新判据;把判据递归使用后,维度依赖降到迭代对数,但当时还没有彻底解决。
  5. 决定性的一步,是把整套递归细化反复执行,并证明累积误差始终被一个常数所界;思路来自作者此前的线性规划快速算法工作。
  6. 作者把递归方法与误差有界的证明列为研究者原创,AI协助探索、推导、写稿和内部检查,方向选择与最终验证由人完成。
  7. 另一组专家同日独立发表完整证明,称微软论文第一版的成果是“证明中的关键一步”;还有第三份相近思路的证明和一份Lean 4形式化。
  8. 用大致相同的总token预算让几种领先模型无引导地反复尝试,没有成功。
  9. 许多原本以KLS为前提的结果,现在可以无条件成立。

一道悬了三十年的几何难题

KLS猜想由Kannan、Lovász与Simonovits在1995年提出。它关心的是:把一个高维概率分布切成两块时,最窄的“瓶颈”在哪里。猜想认为,只用平面(超平面)去切,效果总能接近任意形状的最佳切法,二者相差不超过一个通用常数,而且这个常数不会因为维度增加而变大。如果成立,就意味着高维空间里存在一条与维度无关的几何规律。

在这次工作之前,已知最好的结果允许这个界随着维度增加而缓慢增长。文章称,新证明表明这一关系在一个固定的界内成立,不论形状有多少维。差别看似只是“缓慢增长”和“固定”,却正是猜想成立与否的分界。

这个问题的分量,来自它和计算的联系:切割的几何决定了随机游走探索一个分布有多快。很多科学计算依赖在高维空间中随机采样,KLS因而一直处在高维采样理论的中心。换句话说,它回答的是这些随机算法在维度很高时会不会越来越慢。

证明怎样一步步把维度挤出去

文章介绍,作者先想把此前最好的结果改得更精确。在一个结构化、由人主导的流程里,他们与AI智能体一起探索了100多种候选方法,其中不少涉及高阶张量的冗长计算,由此得到一个新的数学判据,它成了最终证明的基础。

接着他们发现,这个判据可以递归使用:每得到一个更好的界,就把它送回同一个论证,换来更紧的界。这样做把对维度的依赖降到了迭代对数。这个函数增长得极其缓慢,但终究还在随维度增长,所以猜想当时仍未完全解决。

最后一步,是把整个递归细化过程反复执行,而不只做一次。作者证明,每一轮引入的小误差收缩得足够快,加总起来仍被一个与维度无关的常数所界,维度依赖由此被彻底消除,论文的十月四日版本完成了证明。文章说,这一想法来自作者此前在线性规划快速算法上的工作。

AI做了什么,人做了什么

这篇文章对分工写得很明确:递归方法、它的反复应用,以及累积误差有界的证明,被列为研究者的原创贡献;AI工具帮助探索候选方法、完成细节推导、准备稿件并做内部证明检查。决定数学方向、挑选有希望的想法、把它们组装成最终论证并验证证明的,是研究者本人。

具体的工作方式是一种带人工“剪枝”的智能体搜索:多个智能体并行探索同一想法的不同变体,研究者查看中间结果,淘汰没有前途的方向,再把最有希望的结果交给下一轮。文章说,关键突破出现之前,大约探索了一百条研究轨迹。

项目里还有一条对照线:作者用几种领先AI模型,在大致相同的总token预算下,反复无引导地尝试解决同一问题,结果没有达到目标。文章据此认为,成功同时依赖AI系统的能力和研究者的数学判断。这个比较出自作者自己的项目,预算只是“大致相同”,能说明这一次任务里引导的作用,却不足以推出无引导的AI做不了数学研究。

这个证明有多可靠

数学界很看重独立证明。文章介绍,作者发布完整证明的同一天,另一组专家也发布了他们并行完成的完整证明,并称微软论文第一版是“证明中的关键一步”;同一天还有第三份依靠相近思路的证明。之后又有人发布了Lean 4形式化,把微软第一篇论文的关键判据与其他研究结合了起来。

不过,这些确认都来自博客的转述,本文没有读到其他组的证明本身。作者说已经缩短了证明并在Lean中验证了精简版,但计划在最终审阅后才一并发布;他们目前仍在简化证明、扩展形式化验证,好让数学和理论计算机科学的同行更容易检查并在此基础上继续研究。

证明之后改变了什么

对研究本身而言,最直接的变化是:许多以前把KLS当作假设的结果,现在可以无条件陈述,凸几何、概率和理论计算机科学由此有了更牢固的基础。

对关心AI的读者,这个案例更值得看的是流程,而不是“AI证明了猜想”这样的说法。按文章的描述,AI承担了大量探索与推导,但判断哪条路值得走、由谁来组装并验证最终论证,仍落在研究者身上。这种方式能否用到其他数学问题,文章没有给出证据;它提供的是一个有独立证明佐证的成功样本,以及一次预算相近、却没有成功的无引导对照。

原始资料

  • 原题:Solving a 31-year-old grand challenge in mathematics – the KLS conjecture
  • 作者/书面归属:Xinzhi Zhang
  • 发布日期:2026-10-21T16:00:00+00:00(来源页面或 Feed 日期,详见证据包)
  • 原始链接:Solving a 31-year-old grand challenge in mathematics – the KLS conjecture
  • 本文依据完整公开正文;内部证据采用保存快照行号,不虚构页码或时间戳。

查看飞书归档 ↗