KLS-Vermutung nach 31 Jahren bewiesen – mit KI-Agenten unter menschlicher Führung

Worum es geht

Microsoft Research meldet, dass die Kannan-Lovász-Simonovits-Vermutung (KLS-Vermutung) bewiesen ist. Sie wurde 1995 aufgestellt und gilt als eine der zentralen offenen Fragen der hochdimensionalen Geometrie. Der Beweis stammt von zwei Forschenden, darunter Xinzhi Zhang aus der Gruppe Machine Learning and Optimization bei Microsoft Research. Im Blogbeitrag wird auch Zhao Song als Co-Autor genannt. Bemerkenswert ist der Weg dorthin: KI-Agenten erkundeten mathematische Möglichkeiten, während die Forschenden die Ergebnisse bewerteten, aussortierten und die Suche umlenkten.

Worum es in der Vermutung geht

Die KLS-Vermutung betrifft sogenannte log-konkave Verteilungen. Das ist eine breite Klasse von Wahrscheinlichkeitsverteilungen in vielen Dimensionen, zu der zum Beispiel die gleichmäßige Verteilung in einem konvexen Körper gehört. Man kann sich eine solche Verteilung als Masse vorstellen, die man mit einem Schnitt in zwei Teile trennt. Gefragt wird, wo die engste „Engstelle“ liegt, also wo sich die Masse am schlechtesten teilen lässt.

Die Vermutung sagt: Es reicht, nur flache Schnitte (Hyperebenen) zu betrachten. Der beste flache Schnitt ist höchstens um eine feste, universelle Konstante schlechter als der beste Schnitt beliebiger Form – unabhängig davon, wie viele Dimensionen der Raum hat.

Das hat praktische Bedeutung, weil die Geometrie dieser Schnitte bestimmt, wie schnell Zufallsbewegungen (Random Walks) eine Verteilung erkunden. Solche Verfahren werden zum Sampling, also zum Ziehen von Stichproben aus hochdimensionalen Verteilungen, genutzt. KLS spielt daher in Statistik, Optimierung, Algorithmen und theoretischer Informatik eine Rolle. Das Institut MSRI nannte sie ein „zentrales offenes Problem der hochdimensionalen konvexen Geometrie“, das Simons Institute eines der wichtigsten offenen Probleme der konvexen Geometrie.

Der Weg zum Beweis

Ausgangspunkt war ein Ergebnis vom Juli 2026, bei dem die Schranke noch langsam mit der Dimension wuchs. Die Autoren wollten es zunächst verbessern und die Schranke präziser machen. Dazu arbeiteten sie mit KI-Agenten in einem strukturierten, menschlich geleiteten Verfahren und untersuchten mehr als 100 Lösungsansätze, viele davon mit langen Rechnungen über Tensoren höherer Ordnung (mehrdimensionale Verallgemeinerungen von Matrizen). Daraus entstand ein neues mathematisches Kriterium, das die Grundlage des Beweises bildet.

Dann zeigte sich, dass sich dieses Kriterium rekursiv anwenden lässt: Jede verbesserte Schranke kann wieder in dasselbe Argument eingespeist werden und liefert eine noch bessere. In der Fassung vom 1. Oktober 2026 reduzierte das die Abhängigkeit von der Dimension auf den iterierten Logarithmus. Diese Funktion wächst extrem langsam, wächst aber doch, sodass die Vermutung noch nicht vollständig bewiesen war.

Der letzte Schritt war, die gesamte rekursive Verfeinerung zu wiederholen, statt sie nur einmal anzuwenden. Die Idee stammt aus früherer Arbeit der Autoren zu schnellen Algorithmen für lineare Programmierung. Sie bewiesen, dass die kleinen Fehler jeder Stufe schnell genug schrumpfen, sodass ihre Summe durch eine universelle Konstante beschränkt bleibt. Damit entfiel die Dimensionsabhängigkeit; der Beweis war in der Fassung vom 4. Oktober 2026 vollständig.

Rolle der KI

Laut Microsoft sind die rekursive Methode, ihre wiederholte Anwendung und der Nachweis beschränkter Fehler eigene Beiträge der Forschenden. KI-Werkzeuge halfen, Ansätze zu erkunden, detaillierte Herleitungen auszuführen, das Manuskript vorzubereiten und interne Beweisprüfungen durchzuführen. Die Forschenden bestimmten die Richtung, wählten vielversprechende Ideen aus, fügten sie zum Beweis zusammen und prüften ihn.

Das Verfahren beschreiben sie als agentische Suche mit schrittweisem „Pruning“: Mehrere Agenten untersuchten parallel Varianten einer Idee, die Forschenden sichteten Zwischenergebnisse, verwarfen aussichtslose Richtungen und gaben die besten Ergebnisse an die nächste Runde weiter. Rund hundert Forschungspfade wurden verfolgt, bevor der Durchbruch kam.

In einem getrennten Versuch ließen die Autoren mehrere führende KI-Modelle wiederholt ohne Anleitung am selben Problem arbeiten, mit ungefähr demselben Token-Budget. Das scheiterte. Microsoft folgert, der Erfolg habe von den KI-Fähigkeiten und vom mathematischen Urteilsvermögen der Forschenden abgehangen.

Unabhängige Bestätigung

Am Tag, an dem die Autoren ihren vollständigen Beweis veröffentlichten, stellte eine separate Gruppe führender Fachleute einen parallel entwickelten, vollständigen Beweis online. Er baut auf der ersten Version des Microsoft-Papers auf, deren Kriterium die Gruppe „den entscheidenden Schritt im Beweis“ nennt. Ein dritter Beweis, am selben Tag erschienen, beruht auf einer eng verwandten Idee. Später folgte eine Lean-4-Formalisierung (maschinell prüfbarer Beweis), die das Schlüsselkriterium aus dem ersten Microsoft-Paper mit weiteren Arbeiten kombiniert. Die Autoren haben ihren Beweis außerdem gekürzt und die kürzere Version in Lean verifiziert; beides soll nach abschließender Prüfung erscheinen.

Einordnung

Wenn der Beweis hält, gilt eine Reihe von Ergebnissen, die KLS bisher als Annahme voraussetzten, nun unbedingt. Das stärkt die Grundlage für konvexe Geometrie, Wahrscheinlichkeitstheorie und theoretische Informatik. Die parallelen Beweise und die Formalisierung sprechen dafür, dass es sich um ein echtes Prinzip handelt und nicht um ein fragiles Argument.

Beim KI-Anteil ist Vorsicht angebracht: Die Angaben zum Scheitern ungeleiteter Modelle stammen von Microsoft selbst und sind nicht unabhängig überprüft, auch welche Modelle genutzt wurden, nennt der Beitrag nicht. Die Botschaft des Herstellers lautet, dass geleitete Mensch-KI-Zusammenarbeit menschliche Einsicht verstärkt statt ersetzt. Das Ergebnis selbst dürfte unabhängig von dieser Deutung Bestand haben, weil es mathematisch prüfbar ist.