Microsoft Research 证明 31 年数学难题 KLS 猜想,人类引导 AI 协作完成证明
Solving a 31-year-old grand challenge in mathematics – the KLS conjecture
Microsoft Research 的 Xinzhi Zhang 与 Zhao Song 证明了 1995 年提出的 Kannan-Lovász-Simonovits(KLS)猜想,表明对数凸分布而言,最平坦的超平面切口与任意形状最优切口之差被一个与维度无关的通用常数界定。
作者亲述 KLS 猜想证明过程与人类引导 AI 的探索方法,读者可以了解递归精化证明思路和协作研究模式。
微软研究员与合作者将新的数学思想与人类主导的 AI 相结合,解决了高维几何与概率中的一个核心问题

概览
- 基础科学突破:研究人员解决了 Kannan-Lovász-Simonovits (KLS) 猜想——一个已有 31 年历史、被广泛视为高维几何中最核心的未解问题之一,其影响涉及统计学、优化、算法与计算机科学。
- 一个普适的几何原理:该结果为对数凹分布确立了一个普适的几何原理,表明简单的平面切割总能以固定倍数捕捉到它们最窄的瓶颈,无论维度多少。
- 人机协作:这一突破源于一个人类主导的智能体研究过程:AI 系统探索数学上的可能性,而研究人员则对搜索进行评估、筛选和重新定向。
- 独立确认:多位独立研究人员已验证这项研究,确认其核心判据是关键突破,随后还进行了机器校验的形式化验证。
几十年来,一个关于高维空间中计算难度的基本问题一直无法得到证明。新的研究解决了这一问题,扫清了理解科学与计算领域广泛使用的随机化算法效率的一大理论障碍。
Kannan–Lovász–Simonovits (KLS) 猜想于 1995 年提出。它询问的是:对于一大类高维概率分布,最佳的平面或超平面切割是否总是几乎与任何形状的最佳切割同样有效。更准确地说,KLS 预测两者之差不超过一个普适常数,无论维数是多少。这将确立一个与维度无关的几何原理,对高维几何、概率论和理论计算机科学都具有重要影响。由于这些切割的几何性质决定了随机游走探索分布的速度,KLS 也在高维采样理论中扮演着核心角色。

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