OpenAI hat am 26. Oktober drei Ergebnisse veröffentlicht, die interne Modelle erzeugt haben: eines in der harmonischen Analysis, eines in der Komplexitätstheorie, eines in der Quantenfeldtheorie. Das zweite ist das, über das jetzt alle reden. Die Exponential Time Hypothesis, kurz ETH, ist nach OpenAIs Darstellung falsch – bewiesen vom eigenen System, anschließend in Lean formalisiert und verifiziert.
Warum diese Hypothese so viel trägt
Die ETH ist eine Vermutung über die Komplexität des Erfüllbarkeitsproblems boolescher Formeln und damit eng mit P gegen NP verwandt. Fast alle hielten sie für wahr. Hunderte Arbeiten haben auf ihr bedingte Härteergebnisse aufgebaut, in der Graphentheorie, der Computerbiologie, bei Datenbanken und in der algorithmischen Geometrie. Fällt die Annahme, stehen all diese Schranken wieder zur Debatte. Und mit ihnen die Frage, wie viel schneller die betroffenen Aufgaben lösbar sein könnten.
Den Beweis in natürlicher Sprache hat das System laut OpenAI am 16. Oktober gefunden, die Formalisierung kam danach. Beides, der natürlichsprachliche Beweis und die Lean-Fassung, liegt im GitHub-Repository von OpenAI.
Drei Ergebnisse, drei Veröffentlichungswege
Interessanter als die Mathematik ist fast, wie OpenAI damit umgeht. Das Unternehmen nennt die Manuskripte „eine Form von Rohdaten der Forschung“ und hat externe Fachleute gebeten, als Treuhänder Arbeitsgruppen zu bilden. Die haben drei verschiedene Wege empfohlen: Beim Mathematikergebnis wird die Modellausgabe einfach veröffentlicht. Beim Informatikergebnis bildet sich eine externe Gruppe, die es erklärt, während die Ausgabe öffentlich bleibt. Beim Physikergebnis entscheidet die Gruppe selbst, was wann herauskommt. Sie hält die Artefakte zunächst zurück und schreibt es selbst auf.
Vier Prinzipien gelten für die Zusammenarbeit: keine Geheimhaltungserklärungen, kein akademischer Verdienst für OpenAI, Anerkennung für die Gruppe, Unabhängigkeit. Die Teilnahme ist freiwillig und unbezahlt.
Die ETH-Gruppe führen 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 selbst formuliert; Williams hat starke Varianten davon widerlegt. Die Gruppe hat sich zwei Dinge zusichern lassen: alle Rohdaten öffentlich, damit die Fachwelt unabhängig nachprüfen kann, und eine von OpenAI finanzierte Konferenz über die Folgen.
Die Prüfung ist die eigentliche Neuigkeit
Ein Modell, das ein offenes Problem löst, ist inzwischen ein wiederkehrender Vorgang. Was hier anders ist: Die Leute, deren Vermutung gefallen sein soll, sitzen in der Gruppe, die den Beweis durcharbeitet, und sie haben sich die Rohdaten erzwungen, statt eine Pressemitteilung zu bekommen. Das ist die Form, in der sich solche Behauptungen überhaupt erst überprüfen lassen – und sie ist nicht von OpenAI erfunden, sondern von den Treuhändern verlangt worden. Bis die Gruppe fertig ist, bleibt die ETH ein Ergebnis mit Lean-Siegel und ohne fremde Lesart.