Eine dreißig Jahre alte Vermutung, ein chinesisches Modell und ein maschinell geprüfter Beweis

Eine dreißig Jahre alte Vermutung, ein chinesisches Modell und ein maschinell geprüfter Beweis

Am 15. Oktober gab Shanghai AI Laboratory (上海人工智能实验室) bekannt, dass ein Forschungsteam den dreidimensionalen Fall der Ghys-Vermutung bewiesen hat, eines offenen Problems der dynamischen Systeme, das seit 1995 besteht. Die Arbeit wurde mit dem hauseigenen Modell Intern-S2 entwickelt, und der fertige Beweis wurde von einem Team der Peking University (北京大学) in Lean formal verifiziert.

Bemerkenswert ist nicht nur, dass ein schwieriges Problem gefallen ist. Bemerkenswert ist, dass die Ankündigung um einen Prozess herum aufgebaut war und nicht um eine Zahl: ein Modell, das Herleitungen erzeugt, Forschende, die entscheiden, auf welche Angriffslinien sie ihre Aufmerksamkeit richten, und ein Beweisassistent, der jeden Schritt zertifiziert. Genau diese Kombination verspricht die Branche seit zwei Jahren, und hier ist sie, mit einem Paper dazu.

Was die Vermutung fragt

Étienne Ghys stellte das Problem 1995. Grob gefragt: Kann das Verhalten chaotischer dynamischer Systeme ihre geometrische Klassifikation bestimmen? Anders gesagt, verrät die Bewegung die Form des Raums, in dem sie stattfindet?

Gelöst wurde nicht die allgemeine Frage. Das Team bewies den Fall der Kodimension eins, also den dreidimensionalen Rahmen, der drei Jahrzehnte offen geblieben war. Diese Unterscheidung ist wichtig, um die Aussage ehrlich zu lesen: Die vollständige Vermutung bleibt breiter, aber der spezifische Fall, der sich bis jetzt allen widersetzt hatte, ist nun geklärt.

Der erste Durchgang lieferte vierhundert Seiten

Die Mechanik der Zusammenarbeit ist interessanter als das Ergebnis, weil sie zeigt, wie Mensch-KI-Forschung Minute für Minute tatsächlich aussieht.

Die erste Erkundung des Problems durch Intern-S2 ergab einen Herleitungsbericht von rund 400 Seiten. Das ist keine Antwort. Es ist ein Haufen möglicher Argumentationen, teils nützlich, teils nicht, und genau die Form von Ausgabe, die man erhält, wenn ein Modell über etwas wirklich Ungelöstes nachdenken soll, statt sich an Bekanntes zu erinnern.

Von dort lief die Arbeit durch sieben Runden fortgesetztem Schlussfolgern. Der Problemgraph, eine Karte von Teilaussagen und ihren gegenseitigen Abhängigkeiten, wuchs von 15 auf 389 Knoten. Die angesammelte Ausgabe erreichte etwa tausend Seiten und umfasste Dutzende verschiedener Ansätze. In jeder Phase taten die Mathematiker das, was das Modell nicht selbst tun kann: Sie sahen sich die Vorschläge an, entschieden, welche Öffnungen vielversprechend waren, und steuerten die nächste Runde.

Xu Disheng, Gastwissenschaftler am Labor und Professor an der Greater Bay University, und Zhang Jiesong, Postdoktorand, der die Vermutung seit seinem Doktorstudium verfolgt hat, lieferten dieses Urteilsvermögen. Zhangs Paper, am 29. September auf arXiv veröffentlicht und am 13. Oktober überarbeitet, ist eine Einzelautorenarbeit mit einer Erklärung zur KI-Nutzung: Das Modell half, die Ideen und Argumente in mehreren Dialogrunden zu entwickeln, und er prüfte die Mathematik unabhängig.

Der Teil, der daraus mehr als eine Geschichte macht

Behauptungen, KI löse Mathematik, sind billig. Gewicht bekommt diese dadurch, dass der Beweis formalisiert wurde.

Das Team der Peking University unter Leitung von Bin Dong und Ruochuan Liu nutzte sein eigenes SHEAF-Framework, um alle vier Haupttheoreme sowie die stützenden Ergebnisse von Ghys zu formalisieren, von denen die Argumente abhängen. Formalisieren heißt, Definitionen, Annahmen und Schlussfolgerungen in eine Sprache zu übersetzen, die ein Computer prüfen kann, in der jeder Schritt des Arguments ausgeschrieben werden muss, statt einem geschulten Leser überlassen zu bleiben.

Die Arbeit dauerte etwa fünf Tage, mit bis zu 100 parallel arbeitenden Agenten, und erzeugte rund 550.000 Zeilen Lean-Code. Lean ist ein interaktiver Theorembeweiser. Ihm ist gleichgültig, wie sicher sich jemand fühlt. Er prüft die Logik und akzeptiert den Beweis oder eben nicht.

SHEAF organisierte die Aufgabe als gerichteten Graphen aus Definitionen, Aussagen und Abhängigkeiten, sodass getrennte Agenten an zusammenhängenden Teilen arbeiten konnten, während das Team verfolgte, welche Aussagen Beweise hatten und welche noch brauchten. Das ist eine wirklich neue Art der Arbeitsteilung, und das Framework musste zudem Lücken in der bestehenden formalen Bibliothek für dynamische Systeme schließen, weil das für diesen Beweis nötige Werkzeug schlicht noch nicht vorhanden war.

Mensch und Modell, verschiedene Aufgaben

Die vom Labor beschriebene Arbeitsteilung ist wörtlich zu nehmen, denn sie ist für keine der beiden Seiten die schmeichelhafte Version.

Das Modell durchforstete Literatur, zerlegte die Aussage in Teile, erkundete Beweiszweige parallel, prüfte logische Schritte und testete eine große Zahl von Ideen schnell. Die Menschen setzten die Richtung, beurteilten, welche Ansätze es wert waren, weiterverfolgt zu werden, und trafen die Entscheidungen darüber, wohin der Aufwand der nächsten Runde gehen sollte.

Keine der beiden Hälften ähnelt der anderen. Der Beitrag des Modells ist Umfang und Ausdauer: Es kann Dutzende Sackgassen im Blick behalten, ohne den Mut zu verlieren. Der Beitrag der Menschen ist Geschmack, also die Fähigkeit, hundert Seiten plausibler Argumentation anzusehen und zu wissen, welche drei Absätze zählen.

Eine Anekdote hängt daran, aus der die chinesische Presse viel gemacht hat. Ein Experte für dynamische Systeme soll dasselbe Problem aus Neugier an GPT-6 gereicht haben, nachdem er gehört hatte, ein inländisches Modell habe es gelöst, und es kam nicht dorthin. Eng gelesen ist das ein Vergleich zweier Systeme an einem Problem, was sehr wenig beweist. Als Signal für die Wettbewerbsdynamik gelesen, ist es die Art von Detail, die Investitionen treibt.

Warum formale Verifikation die Einsätze verändert

Über weite Strecken der letzten zwei Jahre war der Engpass in der KI-gestützten Mathematik nicht das Erzeugen möglicher Argumente. Modelle sind gut darin, plausibles Schlussfolgern zu produzieren. Der Engpass war zu wissen, welcher Teil davon korrekt ist, weil das Prüfen eines Beweises langsam ist, Sachverstand erfordert und sich schlecht parallelisieren lässt.

Lean kehrt das um. Ist eine Aussage einmal formalisiert, ist die Verifikation billig und schnell, und sie ist vertrauenswürdig, weil sie mechanisch ist und nicht sozial. Die 550.000 Zeilen sind der teure Teil, und dass ein Team plus hundert Agenten sie in fünf Tagen hervorbringen konnten, ist der eigentliche Fortschritt hier. Er legt nahe, dass sich der Verifikationsengpass gerade lockert, so wie der Generierungsengpass bereits locker war.

Das Labor kündigt an, den Arbeitsablauf als wiederverwendbares Modul zur mathematischen Verifikation auf seiner Plattform für wissenschaftliche Entdeckung zu bündeln und dabei Modell, Agenten, Daten und Versuchsgeräte zu verbinden. Es verweist außerdem auf ein früheres Ergebnis, bei dem ein Team der Wuhan University (武汉大学) mit der Plattform den Entwicklungszyklus für eine elektrochemische Synthese von fünf bis zehn Jahren auf ein bis zwei verkürzte.

Was daraus zu ziehen ist

Die ehrliche Zusammenfassung lautet: Dies ist ein echtes Ergebnis mit einem echten Beweis, hervorgebracht von einem Arbeitsablauf, der noch sehr personalintensiv ist. Sieben Runden Expertensteuerung sind kein Modell, das allein läuft. Eine Einzelautorenarbeit mit KI-Nutzungserklärung ist kein Modell, das Anerkennung beansprucht.

Was sich geändert hat, ist, dass sich die Schleife nun schließt. Ein Modell kann genug Argumentation erzeugen, um bei einem von niemandem gelösten Problem von Bedeutung zu sein, Menschen können es lenken, und ein Beweisassistent kann das Ergebnis zertifizieren, ohne dass jemand einer Zusammenfassung vertrauen muss. Das ist eine Pipeline, keine Demo, und Pipelines sind es, die eine Fähigkeit in eine Praxis verwandeln.

Die nächste Frage ist, ob sich das über die Fälle hinaus verallgemeinert, in denen Formalisierung überhaupt möglich ist. Geometrie und Dynamik haben eine Struktur, die sich für maschinelles Prüfen eignet. Ein Großteil der übrigen Wissenschaft nicht, und gerade in diesem unordentlicheren Gebiet, in Biologie, Materialwissenschaft und Medizin, wird sich das Versprechen der KI als Forschungsassistentin tatsächlich bewähren müssen. Das Ghys-Ergebnis sagt, dass das Werkzeug funktionieren kann. Wie oft, sagt es noch nicht.