OpenAI meldet drei Beweise seiner internen Modelle, darunter eine Wider­le­gung der Expo­nen­ti­al­zeit-Hypothese, und lässt externe Gruppen sie erklären

OpenAI hat am 26. Oktober drei Ergebnisse seiner internen Modelle bekanntgegeben, aus der harmonischen Analysis, der Kom­ple­xi­täts­theorie und der Quan­ten­feld­theorie. Das folgenreichste betrifft die Informatik: Nach Angaben des Unternehmens hat sein System die Exponentialzeit-Hypothese widerlegt, eine seit Langem bestehende Vermutung über die Rechenzeit beim Erfüll­bar­keits­pro­blem für boolesche Formeln, das eng mit der Frage P gegen NP zusammenhängt. Die Widerlegung in natürlicher Sprache fand die KI am 16. Oktober, die Formalisierung in Lean folgte am 17. Oktober. Beides liegt im öffentlichen GitHub-Repository von OpenAI. Alles Weitere in dieser Meldung ist OpenAIs Darstellung, die Prüfung durch Fachleute außerhalb des Unternehmens beginnt gerade erst.

Hunderte Härteergebnisse ruhen auf der Exponentialzeit-Hypothese

Bisher galt die Hypothese weithin als zutreffend, und entsprechend viel ist auf ihr aufgebaut. Hunderte Arbeiten haben aus ihr bedingte Härteergebnisse abgeleitet, in der Graphentheorie, der Bioinformatik, bei Datenbanken und in der algorithmischen Geometrie. Ein solches Ergebnis sagt, dass sich eine Aufgabe nicht wesentlich schneller lösen lässt, sofern die Hypothese stimmt. Fällt die Hypothese, verliert jede dieser Schranken ihre Voraussetzung, und für jede dieser Aufgaben ist wieder offen, wie viel schneller sie sich lösen lässt. Ein schnelleres Verfahren liegt damit noch nicht vor: Solche Algorithmen zu finden und aus dem theoretischen Fortschritt praktische Verbesserungen zu machen, braucht nach OpenAIs eigener Einschätzung erhebliche weitere Forschung. Ganz ohne Vorlauf kommt der Angriff auf die Hypothese allerdings nicht, denn Ryan Williams hat bereits starke Fassungen von ihr widerlegt.

Die Urheber der Hypothese prüfen ihre Widerlegung

Eine Formalisierung in Lean klingt, als wäre die Frage damit entschieden. OpenAI selbst bewertet seine Manuskripte zurückhaltender, als Rohdaten der Forschung, aus denen erst noch Verständnis werden muss. Deshalb hat das Unternehmen externe Fachleute gebeten, als Betreuer Gruppen zusammenzustellen, die die Ergebnisse verstehen und erklären. Für die Informatik leiten diese Gruppe Russell Impagliazzo und Ramamohan Paturi von der UC San Diego sowie Ryan Williams vom MIT. Impagliazzo und Paturi haben die Hypothese gemeinsam mit Francis Zane aufgestellt und in den vergangenen 30 Jahren mehrere einflussreiche Arbeiten dazu veröffentlicht. Die Gruppe hat um zwei Dinge gebeten, und OpenAI hat beidem zugestimmt: Alle Rohdaten werden öffentlich, damit die Fachwelt das Ergebnis unabhängig prüfen kann, und OpenAI finanziert eine Konferenz über die Folgen für das ganze Fach. Beweis und Lean-Fassung sind deshalb schon jetzt einsehbar.

Wellen in jeder Dimension, Quantenchromodynamik in vier

Das Ergebnis aus der Mathematik geht auf eine Vermutung zurück, die Sogge 1991 aufgestellt hat. Sie betrifft Wellen, die sich bündeln: Die stärkste Bündelung soll nur kurz anhalten, zu einem typischen Zeitpunkt fällt sie viel schwächer aus als im ungünstigsten Fall. Aus ihr folgen die Kakeya-Vermutung und Steins Restrik­ti­ons­ver­mu­tung. Guth, Wang und Zhang hatten die Vermutung 2019 für zwei Raumdimensionen bewiesen, Wang und Zahl 2025 die Kakeya-Vermutung in drei Dimensionen. OpenAIs Modelle haben nach Angaben des Unternehmens einen Beweis für jede Dimension geliefert, gestützt auf eine neue partielle Dif­fe­ren­ti­al­glei­chung als Hilfsmittel, und damit auch die beiden anderen Vermutungen in allen Dimensionen gelöst. Die KI-Ausgabe entstand am 18. Oktober, die Lean-Fassung am Tag darauf. Auf Rat einer externen Fachperson hat OpenAI beides veröffentlicht, wie schon bei einer Veröffentlichung am 6. Oktober, und überlässt die Erklärung der Fachwelt.

Das physikalische Ergebnis ist ein mathematisch strenger Existenzbeweis für bestimmte wechselwirkende Quan­ten­feld­theo­rien mit Eichfeldern und Fermionen in vier Dimensionen. Dazu gehören die Quan­ten­chro­mo­dy­namik, die beschreibt, wie Quarks und Gluonen über die starke Kraft wechselwirken, und eine vereinheitlichte Vervollständigung des Standardmodells. Als Teilproblem enthält er die Existenz der reinen Yang-Mills-Theorie, die Teil des Millennium-Problems des Clay Mathematics Institute ist. Den Beweis für Yang-Mills legten die Modelle am 9. September vor, den für die Quan­ten­chro­mo­dy­namik am 18. September; die Lean-Formalisierung für die Existenz der Yang-Mills-Theorie war am 16. Oktober fertig. Betreut wird das Ergebnis von einer Gruppe um David Gross, zu der Michael Douglas, Arthur Jaffe, Igor Klebanov und Nikita Nekrasov gehören. Sie hält die KI-Artefakte vorerst zurück und schreibt die Arbeit selbst auf.

Betreuer bestimmen, wer zuerst prüft

Für die Zusammenarbeit hat OpenAI Grundsätze festgelegt. Die Beteiligten unterschreiben keine Geheim­hal­tungs­ver­ein­ba­rung und dürfen Zwischenstände und Schlüsse veröffentlichen. Die Teilnahme ist freiwillig und unbezahlt, und OpenAI beansprucht für die Entdeckungen keine wissenschaftliche Anerkennung. Einen Nachteil des Verfahrens nennt das Unternehmen selbst: Wer die ersten Betreuer auswählt, bestimmt, wer zuerst beteiligt ist, und schafft ein Gefälle an Information. Beim Physikergebnis ist dieses Gefälle am größten, denn außerhalb der Gruppe liegt dort bisher nichts vor, und eine abgeschlossene Lean-Fassung nennt die Ankündigung nur für den Yang-Mills-Teil. Welcher der drei Freigabewege am meisten nützt, weiß OpenAI nach eigener Aussage noch nicht, und ein Urteil der Gruppen enthält die Ankündigung noch nicht. Ob die Exponentialzeit-Hypothese tatsächlich falsch ist, entscheidet die offene Prüfung, zu der die Gruppe um Impagliazzo, Paturi und Williams die Fachwelt einlädt.

Einordnung

Für alle, die KI-Ergebnisse im eigenen Fach bewerten, ist das Verfahren lehrreicher als das Ergebnis. Eine maschinelle Prüfung in Lean belegt, dass der Beweis zum formalen Satz passt, und lässt offen, ob dieser Satz die gemeinte Aussage genau wiedergibt. Darüber urteilen erst Fachleute, und dieselbe Arbeitsteilung gilt im Kleinen für jede Modellantwort, die nach Gewissheit klingt. Wie man eine solche Antwort prüft, statt ihr zu glauben, beschreibt Vibe-Coding / Agentic Engineering, Kapitel 07.