AIsaAIsaStudio English 打开 AIsa Studio

Microsoft Research 证明 31 年悬而未决的 KLS 猜想

原标题:Solving a 31-year-old grand challenge in mathematics – the KLS conjecture

Microsoft Research 的 Xinzhi Zhang 与 Zhao Song 完整证明了 1995 年提出的 Kannan–Lovász–Simonovits(KLS)猜想,表明对数凸分布而言,平面切割的瓶颈与任意形状切割之差被一个与维度无关的通用常数界定。研究者以人类引导的智能体搜索方式探索了约 100 条候选路径,通过递归收紧界并证明累积误差有界完成证明;同日出现独立证明,随后另有团队发布基于其关键判据的 Lean 4 形式化验证,作者也计划在终审后发布精简证明及 Lean 验证。

为什么值得看

原文给出证明思路、独立验证与人类引导 AI 的研究过程细节,读者可以据此理解人机协作如何促成数学突破。

阅读原文 ↗10月22日 AI 日报

本页的摘要、推荐理由与解读出自 AIsa Studio 的 AI 风向智能体,原文版权归原作者所有。

深度解读

发生了什么

Microsoft Research 的研究人员(包括机器学习与优化组的 Xinzhi Zhang,以及合作者 Zhao Song)证明了 Kannan–Lovász–Simonovits(KLS)猜想。该猜想于 1995 年提出,悬置 31 年,被广泛视为高维几何中最核心的未解问题之一。

KLS 猜想问的是:对于一类广泛的高维概率分布,最好的平面(超平面)切割是否总能与任意形状的最佳切割效果相近——具体来说,两者相差不超过一个与维数无关的通用常数。新证明表明这一关系确实以固定界限成立,无论形状有多少维。

关键细节

  • 研究起点是改进 2026 年 7 月的既有结果:作者在 AI 智能体参与的、由人主导的结构化流程中探索了超过 100 条候选路径,其中许多涉及高阶张量的长篇计算,由此得到一个新的数学判据。
  • 关键一步是发现该判据可以递归使用:每次改进的界限可重新喂入同一论证,产生更紧的界限。10 月 1 日的论文版本把对维数的依赖降到迭代对数级别——增长极慢但仍然随维数增长,尚未完全解决猜想。
  • 最后一步是把整个递归精细化过程重复执行而非只做一次,这一想法受作者此前线性规划快速算法工作的启发。他们证明了每一阶段引入的小误差收缩得足够快,总量被一个与维数无关的通用常数控制,从而在 10 月 4 日的版本中完成证明。
  • 独立验证方面:作者公布完整证明当天,另一组顶尖专家基于其首个版本(称其为「证明中的关键一步」)并行给出了完整证明;同日出现的第三个证明依赖密切相关思想;随后还发布了结合该关键判据的 Lean 4 形式化验证。作者本人也缩短了证明并在 Lean 中验证,计划在终审后发布。
  • 关于人机协作:主流程采用多智能体并行探索加研究者迭代「剪枝」的方式,约探索了一百条研究轨迹后出现关键突破。作为对照,作者用相近的总 token 预算让多个前沿模型反复无引导地尝试求解同一问题,结果未能达成目标。

为什么重要

该结果确立了一个普适几何原理:对数凹分布中,简单的平面切割可以在固定倍数内捕捉其最窄的瓶颈,与维数无关。用原文的话说,「高维空间比此前已知的更有序,导航其中的障碍不会随维数增加而无界增长」。

由于这些切割的几何性质决定了随机游走探索分布的速度,KLS 在高维采样理论中处于中心地位;此前的最佳结果允许界限随维数缓慢增长,如今这一理论障碍被消除。此前依赖该猜想作为假设的大量结果,现在可以无条件陈述,为凸几何、概率论和理论计算机科学研究提供更强的基础。

同时,这项工作展示了一种具体的人机协作模式的价值:不是让模型一次性端到端解题,而是由研究者评估、剪枝、引导搜索方向。成功同时依赖 AI 系统的能力和研究者的数学判断——判断哪些方向有希望、识别概念联系、看懂部分洞见何时指向更深的结果。

对谁有影响

直接受益的是凸几何、概率论与理论计算机科学领域的研究者:基于 KLS 猜想的既有结论可转为无条件成立,高维采样与相关算法理论的界限得以收紧。

对关注 AI 用于科研的从业者而言,这项工作提供了一个可参考的协作范式——研究者主导的智能体搜索与剪枝流程,相比同等预算的无引导模型调用更有效。文中提到的独立证明与 Lean 形式化验证,也为高风险数学结果的验证流程提供了范例。

全文翻译

微软研究人员与合作者将新的数学思想与人类主导的 AI 相结合,解决了高维几何与概率论中的一个核心问题

并排图表比较了对同一凸几何形状的平面切割和曲面切割。左侧面板标记为“平面切割”,显示一个菱形横截面,切割面积为 0.2500。右侧面板标记为“最小曲面切割”,显示一个弯曲的、带状的横截面,切割面积较小,约为 0.2173。图表下方的文字总结了 KLS 猜想:在将凸体分成两个等体积的切割中,最佳的平面切割面积至多为任意维度中最小可能切割面积的常数倍。

概览

  • 基础科学突破: 研究人员解决了 Kannan-Lovász-Simonovits (KLS) 猜想,这是一个已有 31 年历史的问题,被广泛认为是高维几何学中的核心未解问题之一,对统计学、优化、算法和计算机科学具有深远影响。
  • 普适的几何原理: 该结果确立了针对对数凹分布的普适几何原理,表明简单的平面切割可以在固定因子内捕捉到其最窄的瓶颈,且与维度无关。
  • 人机协作: 这一突破源于一种由人类主导的智能体研究过程,其中 AI 系统探索数学可能性,而研究人员则进行评估、剪枝并引导搜索方向。
  • 独立验证: 多位独立研究人员已验证了此项研究,确认其核心准则是关键突破,随后进行了机器检查的形式化验证。

数十年来,关于高维空间计算难度的一个基本问题一直未能得到证明。最新的研究解决了这一问题,消除了理解科学和计算中广泛使用的随机算法效率的主要理论障碍。

Kannan–Lovász–Simonovits (KLS) 猜想于 1995 年提出。它询问的是,对于一大类高维概率分布,最佳的平面或超平面切割是否总是几乎与任何形状的最佳切割一样有效。更准确地说,KLS 预测两者之间的差异不超过一个通用常数,无论维度数量如何。这将确立一个无维度的几何原理,对高维几何、概率论和理论计算机科学具有重要意义。由于这些切割的几何结构决定了随机游走探索分布的速度,KLS 在高维采样理论中也扮演着核心角色。

并排图表比较了对同一凸几何形状的平面切割和曲面切割。左侧面板标记为“平面切割”,显示一个菱形横截面,切割面积为 0.2500。右侧面板标记为“最小曲面切割”,显示一个弯曲的、带状的横截面,切割面积较小,约为 0.2173。图表下方的文字总结了 KLS 猜想:在将凸体分成两个等体积的切割中,最佳的平面切割面积至多为任意维度中最小可能切割面积的常数倍。

图 1:正四面体上 KLS 猜想的示意图(简化版)。

自 1995 年以来,数学家们积累了证据表明该猜想是正确的,但完整的证明一直 elusive(难以捉摸)。现在,包括微软研究院机器学习与优化组的 Xinzhi Zhang 在内的两名研究人员已经 证明了 KLS 猜想(在新标签页中打开)。他们表明,无论形状有多少维度,这种关系都保持在一个固定的界限内。在此工作之前,已知最好的结果(在新标签页中打开) 于 2026 年 7 月确立,允许该界限随着维度数量的增加而缓慢增长。这项工作确立了一个基本的几何原理:高维空间比先前所知的表现更好,且导航它们的障碍不会随维度的增加而无界增长。

学术会议

ICLR 活动页面标题 - 紫色渐变背景上的抽象形状

微软参加 SOSP 2026

学术界和工业界的参与者展示涵盖计算机系统软件理论与实践全范围的研究和经验论文。

KLS 猜想的重要性在其解决之前很久就在整个领域得到了认可。在 数学科学研究研究所 (MSRI)(在新标签页中打开) 的 2017-18 年度报告中,它被称为“高维凸几何学中的一个核心开放问题”。Simons 研究所(在新标签页中打开) 将其描述为“凸几何学中最重要的开放问题之一”。在 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 researcher and collaborator combine new mathematical ideas with human-directed AI to resolve a central problem in high-dimensional geometry and probability

Side-by-side diagrams compare a flat cut and a curved cut through the same convex geometric shape. The left panel, labeled “Flat cut,” shows a diamond-shaped cross-section with a cut area of 0.2500. The right panel, labeled “Smallest Curved Cut,” shows a curved, ribbon-like cross-section with a smaller cut area of approximately 0.2173. Below the diagrams, text summarizes the KLS Conjecture: among cuts that divide a convex body into two equal volumes, the best flat cut has area at most a universal constant times the smallest possible cutting area in any dimension.

At a glance

  • Fundamental scientific breakthrough: Researchers resolved the Kannan-Lovász-Simonovits (KLS) conjecture, a 31-year-old problem widely regarded as one of the central open questions in high-dimensional geometry, with implications for statistics, optimization, algorithms, and computer science.
  • A universal geometric principle: The result establishes a universal geometric principle for log-concave distributions, showing that simple flat cuts can capture their narrowest bottlenecks within a fixed factor, regardless of dimension.
  • Human-AI collaboration: The breakthrough emerged from a human-directed agentic research process in which AI systems explored mathematical possibilities while researchers evaluated, pruned, and redirected the search.
  • Independent confirmation: Multiple independent researchers have validated this research, identifying its central criterion as the key breakthrough, followed by a machine-checked formal verification.

For decades, a fundamental question about the difficulty of computing in high-dimensional spaces has resisted proof. New research resolves this question, removing a major theoretical obstacle to understanding the efficiency of randomized algorithms used across science and computing.

The Kannan–Lovász–Simonovits (KLS) conjecture was proposed in 1995. It asks whether, for a broad class of high-dimensional probability distributions, the best flat or hyperplane cut is always nearly as effective as the best cut of any shape. More precisely, KLS predicts that the two differ by no more than a universal constant, regardless of the number of dimensions. This would establish a dimension-free geometric principle with important consequences for high-dimensional geometry, probability, and theoretical computer science. Because the geometry of these cuts governs how quickly random walks can explore a distribution, KLS also plays a central role in the theory of high-dimensional sampling.

Side-by-side diagrams compare a flat cut and a curved cut through the same convex geometric shape. The left panel, labeled “Flat cut,” shows a diamond-shaped cross-section with a cut area of 0.2500. The right panel, labeled “Smallest Curved Cut,” shows a curved, ribbon-like cross-section with a smaller cut area of approximately 0.2173. Below the diagrams, text summarizes the KLS Conjecture: among cuts that divide a convex body into two equal volumes, the best flat cut has area at most a universal constant times the smallest possible cutting area in any dimension.

Figure 1: An illustration of the KLS Conjecture (simplified) on regular tetrahedron.

Since 1995, mathematicians have accumulated evidence that the conjecture was true, but a complete proof remained elusive. Now, two researchers, including Xinzhi Zhang from the Machine Learning and Optimization group at Microsoft Research, have proved the KLS conjecture (opens in new tab). They have shown that the relationship holds with a fixed bound, regardless of how many dimensions a shape has. Before this work, the best known result (opens in new tab), established in July 2026, allowed that bound to grow slowly as the number of dimensions increased. This work establishes a fundamental geometric principle: high-dimensional spaces are better behaved than previously known, and the obstacles to navigating them do not grow without bound as dimensions increase.

ACADEMIC CONFERENCE

ICLR event page header - abstract shapes on a purple gradient background

Microsoft at SOSP 2026

Academic and industrial participants present research and experience papers that cover the full range of theory and practice of computer systems software.

The importance of the KLS conjecture was recognized across the field long before it was resolved. In its 2017-18 Annual Report, the Mathematical Sciences Research Institute (MSRI) (opens in new tab) called it “a central open problem in high-dimensional convex geometry.” The Simons Institute (opens in new tab) described it as “one of the most important open problems in convex geometry.” In the proceedings of the 2022 International Congress of Mathematicians (ICM) (opens in new tab), Ronen Eldan noted its broad implications for high-dimensional convex and computational geometry. Quanta Magazine (opens in new tab) wrote that KLS “lies at the heart of many questions in statistics and computer science.”

Technical details

The authors began by improving the July 2026 result in order to make the mathematical bound more precise. Working with AI agents in a structured, human-directed process, they explored more than 100 candidate approaches, many involving lengthy calculations with higher-order tensors. This produced a new mathematical criterion that became the foundation of the final proof.

The authors then discovered that the new criterion could be applied recursively. Each improved bound could be fed back into the same argument to produce a still tighter one. In the October 1, 2026 version of the paper, this reduced the dependence on dimension to the iterated logarithm. This function grows extraordinarily slowly, but it still grows with the dimension and therefore did not yet fully resolve the conjecture.

The final step was to repeat the entire recursive refinement, rather than applying it only once. This idea was inspired by the authors’ earlier work on fast algorithms for linear programming. The authors proved that the small errors introduced at each stage shrink fast enough that their total remains bounded by a universal constant, independent of the dimension. This eliminated the dependence on the number of dimensions and completed the proof in the October 4, 2026 version of the paper.

The recursive method, its repeated application, and the proof that the accumulated errors remain bounded are original contributions of the researchers. AI tools helped explore candidate approaches, carry out detailed derivations, prepare the manuscript, and perform internal proof checks. The researchers determined the mathematical direction, selected the promising ideas, assembled them into the final argument, and verified the proof.

Independent confirmation

On the same day that the authors posted their complete proof, a separate group of leading experts posted a full proof (opens in new tab) that they developed in parallel. Their work built upon the findings in the first version (opens in new tab) of the Microsoft paper, calling it “the crucial step in the proof.” A third proof (opens in new tab) which appeared separately on the same day relies on a closely related idea. In addition, a Lean 4 formalization (opens in new tab) was subsequently released, combining the key criterion from the first Microsoft paper with additional research.

Independent proofs are among mathematics’ strongest forms of validation because they demonstrate that a result does not rest on a single chain of reasoning. The subsequent appearance of alternative approaches and formal verification further strengthens confidence that the field has uncovered a genuine underlying principle rather than a fragile technical argument. The authors have also shortened their proof and verified the streamlined argument in Lean; they plan to release both after final review. Together, these developments provide complementary forms of confirmation.

Human-AI guidance

In the process of proving KLS, this research also demonstrates the power of having researchers direct AI rather than simply asking AI to solve a complex problem through a single end-to-end run of a frontier model or agent. The authors used an agentic search process with iterative, human-assisted “pruning”: As multiple agents explored variations of an idea in parallel, the researcher examined their intermediate result, eliminated unpromising directions, and passed the most promising result to the next round. Roughly one hundred research trajectories were explored before the key breakthrough emerged.

In a separate track of the project, the authors made repeated unguided attempts to solve the same problem with several leading AI models, using roughly the same total token budget as the main process. That effort fell short of the goal. The eventual success depended on both the capabilities of the AI systems and the mathematical judgment of the researchers.

Conclusion

Taken together, resolving KLS settles a central problem in high-dimensional geometry. A wide range of results that previously relied on the conjecture as an assumption can now be stated unconditionally. The proof therefore provides a stronger foundation for research in convex geometry, probability, and theoretical computer science.

The work also demonstrates how carefully guided human-AI collaboration can contribute to genuine scientific discovery while reinforcing, rather than replacing human insight. It highlights the continuing importance of scientific judgment in identifying promising directions, recognizing conceptual connections, and seeing when a partial insight points toward a deeper result. The authors are now simplifying the proof and extending its formal verification so that the mathematics and theoretical computer science communities can more easily examine the result and build on it.

Acknowledgements

Thank you to our co-author Zhao Song for his contributions to this work, and Victor Reis (opens in new tab) and Ishai Menache for helpful discussions throughout the project.

原文版权归 Microsoft Research 及原作者所有,本站转载仅供阅读。如需删除,请联系 support@aisa.one。