微软研究者证明 31 年悬而未决的 KLS 猜想
Solving a 31-year-old grand challenge in mathematics – the KLS conjecture
微软研究者 Xinzhi Zhang 与合作者证明了 1995 年提出的 Kannan-Lovász-Simonovits(KLS)猜想,给出与维度无关的固定界。研究通过人工引导的智能体流程探索了 100 多条候选路径,由研究者筛选和确定方向,最终证明在 2026 年 10 月 4 日版本中完成。同期另有独立团队给出完整证明,并出现 Lean 4 形式化验证。
微软研究者用人工引导的智能体搜索证明 KLS 猜想,可看人机协作如何探索上百条研究路径。
微软研究员与协作者将新的数学思想与人类引导的 AI 相结合,解决了高维几何与概率论中的一个核心问题

概览
- 基础性科学突破:研究人员解决了 Kannan-Lovász-Simonovits(KLS)猜想,这一提出已有 31 年的问题被广泛视为高维几何领域的核心未解问题之一,对统计学、优化、算法和计算机科学均有影响。
- 一条普适的几何原理:该结果确立了 log-concave 分布的一条普适几何原理,表明简单的平坦切割就能在一个固定因子内捕捉到这些分布最窄的瓶颈,与维数无关。
- 人机协作:这一突破源自一个由人类主导的智能体研究过程,其间 AI 系统探索各种数学可能性,而研究人员负责评估、剪枝并重新引导搜索。
- 独立验证:多位独立研究人员已验证这项研究,认定其核心判据为关键突破,随后还进行了机器校验的形式化验证。
数十年来,一个关于高维空间计算难度的根本性问题一直未能得到证明。新研究解决了这一问题,消除了理解科学与计算领域所用随机算法效率的一大理论障碍。
Kannan–Lovász–Simonovits(KLS)猜想于 1995 年提出。它追问的是:对于一大类高维概率分布,最佳的平坦切割或超平面切割是否总是几乎与任意形状的最佳切割同样有效。更准确地说,KLS 预测两者之差不超过一个普适常数,与维数无关。这将确立一条与维数无关的几何原理,对高维几何、概率论和理论计算机科学具有重要影响。由于这些切割的几何性质决定了随机游走探索分布的快慢,KLS 在高维采样理论中也居于核心地位。

自 1995 年以来,数学家们积累了大量证据表明该猜想成立,但完整证明始终难以企及。如今,包括微软研究院机器学习和优化组的 Xinzhi Zhang 在内的两位研究人员证明了 KLS 猜想(在新标签页中打开)。他们证明,无论形状有多少维,这种关系都成立,且界限固定。在此项工作之前,已知最佳结果(在新标签页中打开)(2026 年 7 月确立)只允许该界限随维数增加而缓慢增长。这项研究确立了一条基础性几何原理:高维空间的表现比此前所知更为良好,且穿越它们的障碍不会随维数增加而无界增长。
KLS 猜想在被解决之前,其重要性就已被整个领域所认识。在其 2017-18 年度报告中,数学科学研究所(MSRI) (opens in new tab)称其为“高维凸几何中的一个核心未解问题”。西蒙斯研究所 (opens in new tab)将其描述为“凸几何中最重要的未解问题之一”。在2022 年国际数学家大会(ICM) (opens in new tab)的会议录中,Ronen Eldan 指出了它对高维凸几何与计算几何的广泛影响。Quanta Magazine (opens in new tab)写道,KLS“处于统计学和计算机科学中许多问题的核心”。
技术细节
作者们首先改进了 2026 年 7 月的结果,以使数学界更精确。在与 AI 智能体协作的结构化、由人类主导的流程中,他们探索了 100 多种候选方法,其中许多涉及使用高阶张量的冗长计算。这产生了一个新的数学判据,成为最终证明的基础。
随后,作者们发现这个新判据可以被递归地应用。每一个改进后的界都可以反馈到同样的论证中,从而产生一个更紧的界。在 2026 年 10 月 1 日的论文版本中,这将对方维的依赖降低到了迭代对数。这个函数增长得极其缓慢,但它仍然随维数增长,因此尚未完全解决该猜想。
最后一步是重复整个递归细化过程,而不是只应用一次。这一想法受到作者们此前关于线性规划快速算法工作的启发。作者们证明了每一阶段引入的小误差收缩得足够快,使得它们的总和被一个与维数无关的通用常数所界定。这消除了对维数的依赖,并在 2026 年 10 月 4 日的论文版本中完成了证明。
递归方法、其重复应用,以及累积误差保持有界的证明,都是研究者的原创贡献。AI 工具帮助探索候选方法、进行详细推导、准备手稿并执行内部证明检查。研究者确定了数学方向,选出了有前景的想法,将它们组织成最终论证,并验证了证明。
独立确认
在作者们发布完整证明的同一天,另一组顶尖专家发布了一份完整证明 (opens in new tab),是他们平行开发的。他们的工作建立在微软论文第一版 (opens in new tab)的发现之上,称其为“证明中的关键一步”。同一天单独出现的第三份证明 (opens in new tab)依赖于一个密切相关的想法。此外,随后发布了一个Lean 4 形式化 (opens in new tab),将微软第一篇论文中的关键判据与额外研究结合起来。
独立证明是数学中最有力的验证形式之一,因为它表明一个结果并不依赖于单一的推理链条。随后出现的替代方法和形式化验证进一步增强了人们的信心,即该领域发现了一个真正的底层原理,而非一个脆弱的技术论证。作者还缩短了他们的证明,并在 Lean 中验证了精简后的论证;他们计划在最终审查后发布两者。这些进展共同提供了互补形式的确认。
人机引导
在证明 KLS 的过程中,这项研究还展示了让研究人员指导 AI 的力量,而不是简单地要求 AI 通过前沿模型或智能体的单次端到端运行来解决一个复杂问题。作者使用了带有迭代、人工辅助“剪枝”的智能体搜索过程:当多个智能体并行探索一个想法的变体时,研究人员检查其中间结果,剔除没有前景的方向,并将最有希望的结果传递到下一轮。在大约探索了一百条研究轨迹之后,关键突破才出现。
在项目的另一条独立路线中,作者使用几个领先的 AI 模型,以与主流程大致相同的总 token 预算,对同一问题进行了多次无引导的尝试。那项努力未能达到目标。最终的成功既取决于 AI 系统的能力,也取决于研究人员的数学判断力。
结论
综观全局,解决 KLS 解决了高维几何中的一个核心问题。许多此前将该猜想作为假设依赖的结果,现在可以无条件地陈述。因此,该证明为凸几何、概率论和理论计算机科学的研究提供了更坚实的基础。
这项工作还展示了经过仔细引导的人机协作如何能够为真正的科学发现作出贡献,同时增强而非取代人类的洞察力。它突显了科学判断力在识别有前景的方向、认识概念联系以及判断何时部分洞察指向更深层结果方面的持续重要性。作者现在正在简化证明并扩展其形式化验证,以便数学和理论计算机科学界能够更容易地审视这一结果并在此基础上继续发展。
致谢
感谢我们的合著者 Zhao Song 对本工作的贡献,以及 Victor Reis(在新标签页中打开) 和 Ishai Menache 在整个项目过程中的有益讨论。
在新标签页中打开
来源:Microsoft Research · microsoft.com