KI-Modelle und Plattformen
Microsoft-Forscher und Mitarbeiter beweisen 31 Jahre alte KLS-Vermutung
Unite.AI zu deinen bevorzugten Quellen auf Google hinzufügen
Microsoft Research gab am 21. Oktober 2026 bekannt, dass Xinzhi Zhang, ein leitender Forscher in der Gruppe für maschinelles Lernen und Optimierung des Unternehmens, und sein Mitarbeiter Zhao Song die Kannan-Lovász-Simonovits-Vermutung bewiesen haben – ein 31 Jahre altes Problem der hochdimensionalen Geometrie und Wahrscheinlichkeitstheorie. Dabei nutzten sie einen von Menschen gesteuerten, agentenbasierten KI-Forschungsprozess.
Die Vermutung und die neue Schranke
Der Beweis findet sich in der 140 Seiten umfassenden Arbeit Eine O(1)-Schranke für die KLS-Konstante, die Zhao Song und Xinzhi Zhang zugeschrieben wird. Sie wurde erstmals am 1. Oktober 2026 bei arXiv eingereicht und am 4. Oktober 2026 überarbeitet; Zhang war der einreichende Autor. Im Abstract heißt es, die Autoren bewiesen, dass die KLS-Konstante ψ_n nach oben durch eine universelle Konstante C beschränkt ist, womit die Vermutung gelöst sei. Außerdem bewiesen sie eine universelle Schranke für die Poincaré-Konstante jedes isotropen log-konkaven Wahrscheinlichkeitsmaßes.
Formal fragt die 1995 aufgestellte Vermutung, ob die Cheeger-Konstante jedes isotropen log-konkaven Wahrscheinlichkeitsmaßes im n-dimensionalen Raum nach unten durch eine universelle positive Konstante beschränkt ist. Vereinfacht ausgedrückt, fragt der Beitrag von Microsoft Research, ob für eine breite Klasse hochdimensionaler Wahrscheinlichkeitsverteilungen der beste flache Schnitt oder Hyperflächenschnitt stets nahezu so wirksam ist wie der beste Schnitt beliebiger Form – wobei sich die beiden höchstens um eine universelle Konstante unterscheiden, unabhängig von der Anzahl der Dimensionen. Da die Geometrie dieser Schnitte bestimmt, wie schnell Zufallsbewegungen eine Verteilung erkunden können, spielt die Vermutung eine zentrale Rolle in der Theorie des hochdimensionalen Samplings.
Vor dieser Arbeit war das beste bekannte Ergebnis die 21-seitige Arbeit Die KLS-Konstante ist O(log^{1/4} n) von Brayden Letwin, die am 27. Juli 2026 eingereicht wurde. Sie zeigte, dass ψ_n höchstens das Produkt einer Konstanten und log^{1/4} n beträgt. Wie der Beitrag von Microsoft Research anmerkt, wuchs diese Schranke mit zunehmender Dimensionszahl jedoch weiterhin langsam an. Das neue Ergebnis gilt mit einer festen Schranke, die nicht von der Dimension abhängt.
Die Bedeutung der Vermutung war schon lange vor ihrer Lösung anerkannt. Dem Beitrag zufolge bezeichnete der Jahresbericht 2017–18 des Mathematical Sciences Research Institute die KLS-Vermutung als zentrales offenes Problem der hochdimensionalen konvexen Geometrie. Das Simons Institute beschrieb sie als eines der wichtigsten offenen Probleme der konvexen Geometrie, und Ronen Eldan verwies in den Tagungsberichten des Internationalen Mathematikerkongresses 2022 auf ihre weitreichenden Auswirkungen.
Ein menschlich gesteuerter, agentenbasierter Forschungsprozess
Dem Beitrag zufolge begannen die Autoren damit, das Ergebnis vom Juli 2026 zu verbessern. In einem strukturierten, von Menschen gesteuerten Prozess mit KI-Agenten prüften sie mehr als 100 mögliche Ansätze, von denen viele umfangreiche Berechnungen mit Tensoren höherer Ordnung erforderten. Dabei entwickelten sie ein neues mathematisches Kriterium, das zur Grundlage des endgültigen Beweises wurde.
Anschließend entdeckten die Autoren, dass sich das Kriterium rekursiv anwenden ließ: Jede verbesserte Schranke konnte in dasselbe Argument zurückgeführt werden, um eine noch engere Schranke zu erhalten. In der am 1. Oktober 2026 veröffentlichten Fassung der Arbeit verringerte dies die Abhängigkeit von der Dimension auf den iterierten Logarithmus. Dieser wächst zwar äußerst langsam, nimmt mit der Dimension aber weiterhin zu, sodass die Vermutung damit noch nicht gelöst war. Als letzten Schritt wiederholten die Autoren die gesamte rekursive Verfeinerung, statt sie nur einmal anzuwenden. Diese Idee war laut Beitrag von ihrer früheren Arbeit an schnellen Algorithmen für die lineare Programmierung inspiriert. Die Autoren bewiesen, dass die in jeder Stufe entstehenden kleinen Fehler schnell genug abnehmen, sodass ihre Summe durch eine universelle, von der Dimension unabhängige Konstante beschränkt bleibt. Damit war der Beweis in der am 4. Oktober 2026 veröffentlichten Fassung vollständig.
Dem Beitrag zufolge sind die rekursive Methode, ihre wiederholte Anwendung und das Argument mit den beschränkten Fehlern originäre Beiträge der Forscher. KI-Tools halfen dabei, mögliche Ansätze zu erkunden, detaillierte Herleitungen auszuarbeiten, das Manuskript vorzubereiten und interne Beweisprüfungen durchzuführen. Die Forscher bestimmten jedoch die mathematische Richtung, wählten die vielversprechenden Ideen aus, führten sie zum endgültigen Argument zusammen und überprüften den Beweis. Der Beitrag beschreibt die Methode als agentengestützte Suche mit iterativem, menschlich unterstütztem Aussortieren: Während mehrere Agenten parallel Varianten einer Idee untersuchten, prüfte der Forscher Zwischenergebnisse, verwarf aussichtslose Ansätze und gab das vielversprechendste Ergebnis an die nächste Runde weiter. Vor dem entscheidenden Durchbruch wurden rund hundert Forschungsansätze verfolgt.
In einem separaten Projektstrang unternahmen die Autoren mehrere ungeleitete Versuche, dasselbe Problem mit verschiedenen führenden KI-Modellen zu lösen. Dafür verwendeten sie insgesamt ungefähr dasselbe Token-Budget wie im Hauptprozess. Dem Beitrag zufolge blieb dieser Versuch jedoch hinter dem Ziel zurück. Der letztliche Erfolg beruhte laut Beitrag sowohl auf den Fähigkeiten der KI-Systeme als auch auf dem mathematischen Urteilsvermögen der Forscher. Der Beitrag dankt Song für seine Beiträge zur Arbeit sowie Victor Reis und Ishai Menache für die Gespräche während des gesamten Projekts.
Unabhängige Beweise und maschinelle Verifikation
Am 4. Oktober 2026, am selben Tag, an dem der vollständige Beweis veröffentlicht wurde, veröffentlichten Pierre Bizeul, Boaz Klartag und Joseph Lehec einen parallel entwickelten, 32-seitigen Beweis mit dem Titel „Ein Beweis der Kannan-Lovász-Simonovits-Vermutung“. Im Abstract der Arbeit heißt es, „der entscheidende Schritt im Beweis ist das erst kürzlich von Song und Zhang entwickelte Kriterium, das höhere Ableitungen von Kippmittelwerten einbezieht“. In den arXiv-Kommentaren wird außerdem vermerkt, dass die Arbeit einen Absatz zur Nutzung von KI enthält. Das Abstract nennt die KLS-Vermutung neben Bourgains Schnittproblem und der Varianzvermutung als treibende Kräfte für mathematische Entwicklungen in der hochdimensionalen Geometrie der vergangenen Jahrzehnte.
Krishnakumar Balasubramanian und Shiva Kasiviswanathan veröffentlichten einen separaten Beweis mit dem Titel Eine dimensionsunabhängige Schranke für die Poincaré-Konstante isotroper log-konkaver Maße. Er wurde erstmals am 6. Oktober 2026 eingereicht und am 8. Oktober 2026 überarbeitet. Das Abstract beschreibt einen deterministischen Variationsbeweis mit einer expliziten Schranke von 25 für die Poincaré-Konstante jedes isotropen log-konkaven Wahrscheinlichkeitsmaßes.
Darauf folgte eine Lean-4-Formalisierung namens KLS500, die für jede isotrope log-konkave Wahrscheinlichkeitsverteilung eine dimensionsunabhängige Poincaré-Konstante von höchstens 500 formalisiert. Laut Repository stützt sich die Entwicklung hauptsächlich auf den Kumulanten- und Suspensionsansatz von Bizeul, Klartag und Lehec, ergänzt um das Kipp-Spektralkriterium von Song und Zhang. Bei der Verifikation wurden 1.710 mathematische Module auf Kernel-Vertrauensebene null neu erstellt. Auch die von OpenAI definierte exakte Aussage der KLS-Vermutung wurde in Lean verifiziert, wobei die universelle Poincaré-Konstante 500 verwendet wurde. Das Projekt steht unter der Apache-2.0-Lizenz.
Der Beitrag von Microsoft Research beschreibt unabhängige Beweise als eine der stärksten Formen mathematischer Validierung, da sie zeigen, dass ein Ergebnis nicht auf einer einzigen Argumentationskette beruht. Nachdem die Vermutung bewiesen ist, können Ergebnisse, die zuvor auf ihr als Annahme beruhten, nun laut dem Beitrag ohne Vorbehalte formuliert werden. Die Autoren haben ihren Beweis verkürzt und das gestraffte Argument in Lean verifiziert. Dem Beitrag zufolge planen sie, beides nach einer abschließenden Prüfung zu veröffentlichen.
