Exponentialzeithypothese von einem OpenAI-Modell widerlegt?

Am 26. Oktober hat OpenAI im Repository openai/math die Arbeit „The Exponential Time Hypothesis is False“ veröffentlicht. Demnach hat ein nicht näher benanntes internes OpenAI-Modell die Exponentialzeithypothese (ETH) widerlegt, eine der Grundannahmen der Komplexitätstheorie. Eine unabhängige Gruppe von Informatikern, darunter zwei Mitautoren der Hypothese selbst, untersucht die Arbeit samt ihrer Formalisierung in Lean.

Was ist die Exponentialzeithypothese?

ETH (Exponential Time Hypothesis) besagt, dass sich das Problem 3-SAT, also die Frage, ob eine logische Formel mit Klauseln aus je drei Variablen erfüllbar ist, nicht schneller als in der Zeit 2^Ω(n) für n Variablen entscheiden lässt. Einfacher gesagt: Mit jeder zusätzlichen Variable wächst die Zeit exponentiell, und kein noch so cleverer Algorithmus ändert daran etwas.

Formuliert haben die Hypothese Russell Impagliazzo und Ramamohan Paturi (mit Francis Zane). Auf der ETH beruhen Hunderte Arbeiten, die zeigen, dass ein Problem aus Graphen, Datenbanken oder Bioinformatik „nicht“ schneller lösbar ist (wie The Next Web erinnert).

Was genau hat das OpenAI-Modell bewiesen?

Die Arbeit liefert einen deterministischen Algorithmus, der alle erfüllenden Belegungen einer k-CNF-Formel exakt zählt, für jedes feste k ≥ 2. Er arbeitet mit polynomiellem Speicher und in der Zeit (n + m)^O(1) · 2^(n/(log n)^(1/2+o(1))), also subexponentiell. Der Fall 3-SAT genügt, um die ETH zu widerlegen.

Interessant ist, dass der Algorithmus nicht nur „ja“ oder „nein“ antwortet, sondern die Lösungen zählt. Daraus leitet die Arbeit weitere Folgerungen ab:

1. subexponentielle Algorithmen zum Zählen von Graphfärbungen, unabhängigen Mengen und perfekten Matchings,
2. beliebig genaue Approximationen für Max-k-SAT in subexponentieller Zeit,
3. eine neue untere Schranke für die Größe logischer Schaltkreise für die Klasse E^NP.

Laut The Next Web fand das Modell den Beweis am 16. Oktober, und einen Tag später war er bereits in Lean verifiziert (einer formalen Sprache, in der Computer Beweise prüfen). Im Änderungsverlauf des Repositorys gibt OpenAI an, dass die Arbeit zusammen mit der Lean-Formalisierung online ging.

Wer prüft den Beweis?

Die Gruppe, die den Beweis untersuchen und erklären soll, leiten Russell Impagliazzo, Ramamohan Paturi (UC San Diego) und Ryan Williams (MIT). Laut Änderungsverlauf des Repositorys wurden die Materialien gerade auf Wunsch dieser Gruppe sofort veröffentlicht, damit alle sie prüfen können. Williams schrieb auf X, ein internes OpenAI-Modell habe eine „claimed refutation of ETH“ erzeugt, also eine behauptete Widerlegung der ETH.

Die Forscher haben keine NDAs unterschrieben und werden dafür nicht bezahlt (laut The Next Web). Sie haben OpenAI gebeten, alle Rohdaten offenzulegen und eine Konferenz über die Folgen des Ergebnisses zu finanzieren, und das Unternehmen hat zugestimmt. In einem offenen Brief betonen sie jedoch, dass ihre Beteiligung keine Bestätigung des Ergebnisses ist („should not be taken as certification of the claim“), und fügen hinzu, dass der Beweis, falls er korrekt ist, „it will change an important part of theoretical computer science“.

Ist das etwas Neues in der KI-Welt?

Es ist nicht die erste solche Veröffentlichung von OpenAI. Wie wir wissen, hat das Unternehmen am 6. Oktober über 700 vom Modell erzeugte mathematische Arbeiten in dasselbe Repository gestellt. In der README des Repositorys heißt es, das Modell habe rund 4.000 offene Probleme bekommen, und auf jedes Ergebnis entfielen im Schnitt drei Stunden „Nachdenken“ auf ChatGPT-Pro-Niveau.

Neu ist, dass OpenAI am 26. Oktober gleich drei Ergebnisse bekannt gab und für jedes einen anderen Weg wählte (das beschreibt Unite.AI):

1. ETH: Arbeit und Lean-Beweis sind öffentlich, eine offene Gruppe um Impagliazzo, Paturi und Williams prüft sie.
2. Sogges „Local Smoothing“-Vermutung in allen Dimensionen, aus der laut OpenAI die Kakeya-Vermutung und Steins Restriktionsvermutung folgen: ebenfalls mit Lean-Beweis veröffentlicht.
3. Die Existenz der Yang-Mills-Theorie und der QCD in vier Dimensionen (eines der Millennium-Probleme des Clay Institute): Hier gibt es noch keine Materialien. Eine Gruppe unter Leitung des Nobelpreisträgers David Gross will das Ergebnis selbst ausarbeiten.

OpenAI erklärt dabei, keinen wissenschaftlichen Verdienst für die Entdeckungen seiner Modelle zu beanspruchen. Die Anerkennung sollen die Menschen bekommen, die sie verstehen und beschreiben. Außerdem hat das Unternehmen der Simons Foundation 5 Mio. USD für Workshops und Konferenzen zu KI-generierten Ergebnissen gespendet.

Worauf sollte man achten?

Erstens auf den Stand der Prüfung. Eine Formalisierung in Lean ist ein starkes Signal, aber man muss immer prüfen, ob der in Lean formulierte Satz wirklich dasselbe aussagt wie der Text der Arbeit. OpenAI schreibt selbst in der README, dass einige Ergebnisse ohne Formalisierung Fehler enthalten können, und hat am 7. Oktober drei Arbeiten zurückgezogen, wegen eines Vorzeichenfehlers in einem der Beweise. Behandeln wir das Ergebnis also mit Vorsicht, bis die Gruppe ihre Arbeit abgeschlossen hat.

Zweitens darauf, was das Ergebnis nicht bedeutet. Die Autoren schreiben ausdrücklich, dass daraus nicht folgt, dass alle NP-Probleme subexponentielle Algorithmen haben. Das ist also keine Lösung des Problems P vs NP, und die Laufzeit wächst weiterhin schneller als jedes Polynom.

Drittens auf das Tempo. Ein Ergebnis, an dem Theoretiker über 20 Jahre gearbeitet haben, soll das Modell im Rahmen einer internen Evaluation gefunden haben. Falls es sich bestätigt, wäre das wohl das bisher stärkste Beispiel dafür, dass KI eigenständige Entdeckungen in der theoretischen Informatik macht. Nebenbei kehrt das Thema formaler Beweise zurück, über das ich bei der formalen Verifikation mit Claude geschrieben habe.

FAQ

Was ist die Exponentialzeithypothese?

Die Annahme der Komplexitätstheorie, dass sich 3-SAT nicht in kürzerer Zeit als 2^Ω(n) für n Variablen lösen lässt. Formuliert haben sie Impagliazzo und Paturi mit Francis Zane.

Hat OpenAI das Problem P vs NP gelöst?

Nein. Der Algorithmus ist subexponentiell, aber nicht polynomiell, und die Autoren betonen, dass sich das Ergebnis nicht auf alle NP-Probleme überträgt.

Ist die Widerlegung der ETH schon bestätigt?

Noch nicht. Es gibt eine Formalisierung in Lean, aber die unabhängige Gruppe um Impagliazzo, Paturi und Williams untersucht sie erst und betont, dass ihre Beteiligung keine Bestätigung bedeutet.

Welches OpenAI-Modell war das?

Ein nicht näher benanntes internes Modell. In der README des Repositorys nennt OpenAI seinen Namen nicht.