微软研究院解决悬置31年的KLS数学猜想
Solving a 31-year-old grand challenge in mathematics – the KLS conjecture
微软研究院学者证明KLS猜想,解决这一自1995年提出、悬置31年的高维几何核心问题。他们通过人类指导AI智能体并行探索超100种候选思路并递归精炼完成证明,多个独立证明与Lean 4形式化验证了该结果。
该研究结合人类指导的AI智能体搜索与数学判断证明KLS猜想,为凸几何与理论计算机科学提供无条件基础。
微软研究人员与合作者结合新的数学思想与人类指导的 AI,解决了高维几何与概率论中的一个核心问题

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

自 1995 年以来,数学家们积累了猜想为真的证据,但完整的证明一直难以捉摸。现在,包括微软研究院机器学习与优化组的 Xinzhi Zhang 在内的两名研究人员证明了 KLS 猜想(在新标签页中打开)。他们表明,无论形状有多少维度,该关系都成立且有一个固定界限。在这项工作之前,已知最佳结果(在新标签页中打开)(于 2026 年 7 月确立)允许该界限随着维度数量的增加而缓慢增长。这项工作确立了一个基本的几何原理:高维空间比之前已知的更规整,且导航它们的障碍不会随着维度的增加而无限增长。
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 中验证了简化后的论证;他们计划在最终审查后发布两者。总体而言,这些进展提供了互补形式的确认。
人类-AI 指导
在证明 KLS 的过程中,这项研究还展示了研究人员指导 AI 而非仅仅要求 AI 通过前沿模型或智能体的单次端到端运行来解决复杂问题的力量。作者使用了一种带有迭代、人类辅助“修剪”的智能体搜索过程:当多个智能体并行探索一个想法的变体时,研究人员检查它们的中间结果,消除没有前景的方向,并将最有希望的结果传递给下一轮。在关键突破出现之前,大约探索了一百条研究轨迹。
在项目的另一条轨道中,作者使用几个领先的 AI 模型对同一问题进行了多次无指导的尝试,使用的总令牌预算与主过程大致相同。该努力未能达到目标。最终的成功既依赖于 AI 系统的能力,也依赖于研究人员的数学判断。
结论
综合来看,解决 KLS 解决了高维几何中的一个核心问题。以前依赖于该猜想作为假设的一系列结果现在可以无条件地陈述。因此,该证明为凸几何、概率和理论计算机科学的研究提供了更坚实的基础。
这项工作还展示了精心指导的人类-AI 协作如何有助于真正的科学发现,同时强化而非取代人类洞察力。它强调了科学判断在识别有前景的方向、识别概念联系以及看到部分洞察指向更深层次结果时的持续重要性。作者目前正在简化证明并扩展其形式化验证,以便数学和理论计算机科学社区更容易地检查该结果并在此基础上构建。
致谢
感谢我们的合著者 Zhao Song 对这项工作的贡献,以及 Victor Reis(在新标签页中打开) 和 Ishai Menache 在整个项目过程中的有益讨论。
在新标签页中打开
文章 解决数学中 31 年的重大挑战 – KLS 猜想 首先出现在 Microsoft Research 上。
来源:Microsoft Research · microsoft.com