Microsoft-Forscher lösen 31 Jahre alte KLS-Vermutung mit menschlich gesteuerter KI

Worum es bei der KLS-Vermutung geht

Die KLS-Vermutung wurde 1995 aufgestellt. Sie betrifft eine breite Klasse hochdimensionaler Wahrscheinlichkeitsverteilungen und fragt, ob der beste ebene Schnitt, ein sogenannter Hyperebenenschnitt, stets nahezu so wirksam ist wie der beste Schnitt beliebiger Form. KLS sagt voraus, dass sich beide unabhängig von der Zahl der Dimensionen höchstens um eine universelle Konstante unterscheiden.

Die Frage ist auch über die reine Geometrie hinaus von Bedeutung. Laut Microsoft bestimmt die Geometrie dieser Schnitte, wie schnell Zufallsbewegungen eine Verteilung erkunden können, weshalb KLS in der Theorie des hochdimensionalen Samplings eine zentrale Rolle spielt. Das Unternehmen sieht Folgen für Statistik, Optimierung, Algorithmen und Informatik.

Die Fachwelt stufte das Problem seit Langem als vorrangig ein. Microsoft verweist auf das Mathematical Sciences Research Institute, das es als „zentrales offenes Problem der hochdimensionalen konvexen Geometrie“ bezeichnete, sowie auf das Quanta Magazine, das schrieb, KLS liege „im Zentrum vieler Fragen der Statistik und Informatik“.

Wie der Beweis entstand

Zwei Forscher, darunter Xinzhi Zhang aus der Gruppe Machine Learning and Optimization bei Microsoft Research, bewiesen, dass der Zusammenhang in beliebig vielen Dimensionen mit einer festen Schranke gilt. Vor dieser Arbeit erlaubte das beste bekannte Ergebnis vom Juli 2026, dass die Schranke mit wachsender Dimension langsam anstieg.

Zunächst verbesserten die Autoren dieses Ergebnis, um die Schranke zu präzisieren. In einem strukturierten, von Menschen gesteuerten Prozess mit KI-Agenten untersuchten sie mehr als 100 mögliche Ansätze, von denen viele langwierige Rechnungen mit Tensoren höherer Ordnung umfassten. Daraus ging ein neues mathematisches Kriterium hervor, das zur Grundlage des endgültigen Beweises wurde.

Anschließend stellten sie fest, dass sich das Kriterium rekursiv anwenden lässt: Jede verbesserte Schranke wird erneut in dasselbe Argument eingespeist und liefert eine engere. Die Fassung der Arbeit vom 1. Oktober 2026 reduzierte die Abhängigkeit von der Dimension auf den iterierten Logarithmus, eine Funktion, die extrem langsam wächst, aber eben doch wächst. Der letzte Schritt bestand darin, die gesamte rekursive Verfeinerung zu wiederholen, statt sie nur einmal anzuwenden, eine Idee, die von früheren Arbeiten der Autoren zu schnellen Algorithmen für die lineare Programmierung inspiriert war. Sie wiesen nach, dass sich die kleinen Fehler der einzelnen Stufen zu einer Gesamtgröße summieren, die durch eine universelle Konstante beschränkt ist. Damit war der Beweis in der Fassung vom 4. Oktober 2026 vollständig.

Unabhängige Bestätigung und die Rolle der KI

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 baute auf der ersten Fassung der Microsoft-Arbeit auf, die er als „den entscheidenden Schritt im Beweis“ bezeichnete. Ein dritter Beweis, der auf einer eng verwandten Idee beruht, erschien am selben Tag. Danach wurde eine Formalisierung in Lean 4 veröffentlicht, die das zentrale Kriterium aus der ersten Microsoft-Arbeit mit weiteren Forschungsergebnissen verbindet. Die Autoren haben zudem ihren Beweis gekürzt und die kürzere Fassung in Lean überprüft; beide wollen sie nach der abschließenden Prüfung veröffentlichen.

Microsoft betont, dass Menschen die KI gelenkt haben. Mehrere Agenten untersuchten parallel Variationen einer Idee, während ein Forscher Zwischenergebnisse prüfte, aussichtslose Richtungen verwarf und das beste Ergebnis in die nächste Runde weitergab. Rund einhundert Forschungspfade wurden verfolgt, bevor der entscheidende Durchbruch gelang. KI-Werkzeuge halfen dabei, Ansätze zu erkunden, Herleitungen durchzuführen, das Manuskript vorzubereiten und interne Beweisprüfungen auszuführen, während die Forscher die Richtung festlegten und den Beweis verifizierten.

In einem separaten Versuch unternahmen die Autoren wiederholt ungeführte Anläufe, das Problem mit mehreren führenden KI-Modellen zu lösen, bei etwa gleichem Gesamtbudget an Tokens. Laut Microsoft verfehlte dieser Versuch das Ziel.

Was das bedeutet

Laut Microsoft lassen sich nun zahlreiche Ergebnisse, die bislang die Vermutung voraussetzten, ohne Annahmen formulieren. Das schaffe ein stärkeres Fundament für konvexe Geometrie, Wahrscheinlichkeitstheorie und theoretische Informatik. Das Unternehmen präsentiert die Arbeit als Beispiel für eine geleitete Zusammenarbeit von Mensch und KI, die menschliche Einsicht eher stärke als ersetze.

Die Autoren vereinfachen den Beweis derzeit und weiten seine formale Verifikation aus, damit andere Mathematiker und Informatiker ihn leichter prüfen und darauf aufbauen können.