OpenAI beansprucht einen außergewöhnlichen Durchbruch in der theoretischen Informatik: Ein KI-System soll die seit Jahrzehnten diskutierte Exponential Time Hypothesis widerlegt haben. Der veröffentlichte Ansatz verspricht für eine grundlegende Klasse logischer Probleme eine bislang für unmöglich gehaltene asymptotische Beschleunigung. Eine formale Umsetzung in Lean liegt vor, während eine unabhängige Expertengruppe die Argumentation noch prüft. Entscheidend ist nun, ob der Beweis einer sorgfältigen fachlichen Prüfung standhält.
Eine KI von OpenAI hat nach Angaben des Unternehmens eine Widerlegung der Exponential Time Hypothesis (ETH) entwickelt, einer zentralen Annahme über die Grenzen schneller Algorithmen. In einer Originalmitteilung über die Zusammenarbeit mit Wissenschaftlern stellt OpenAI das Ergebnis vor und beschreibt zugleich eine ungewöhnliche Veröffentlichungspraxis: Externe Spezialisten sollen den maschinell erstellten Beweis nachvollziehen, erklären und kritisch prüfen.
Im Mittelpunkt steht eine Frage, die zunächst nach einem Rätsel aus dem Mathematikunterricht klingt: Wie schnell lässt sich feststellen, ob eine umfangreiche Sammlung logischer Bedingungen gleichzeitig erfüllt werden kann? Hinter dieser Frage stecken Grenzen der Berechenbarkeit, die in Hunderten wissenschaftlichen Arbeiten als Grundlage für weitere Aussagen dienten.
Russell Impagliazzo, Ramamohan Paturi und Francis Zane formulierten die ETH als Vermutung über das Problem 3-SAT. Dabei besteht eine Formel aus Bedingungen mit jeweils höchstens drei logischen Aussagen, deren Variablen entweder wahr oder falsch sein können. Gesucht ist eine Belegung, die sämtliche Bedingungen zugleich erfüllt. Bei n Variablen gibt es insgesamt 2 hoch n mögliche Belegungen, doch ein Algorithmus muss sie nicht zwangsläufig einzeln durchprobieren.
Die ETH behauptet vereinfacht, dass sich 3-SAT im schlechtesten Fall nicht in einer Zeit lösen lässt, deren Exponent gegenüber n gegen null geht. Schon ein Verfahren mit Laufzeit 2 hoch n geteilt durch die Quadratwurzel des Logarithmus von n würde die Vermutung daher widerlegen. Diese Unterscheidung betrifft die mathematische Wachstumsrate bei immer größeren Eingaben und ist wesentlich präziser als die Behauptung, jeder Computer müsse grundsätzlich alle Kombinationen testen.
Der öffentlich zugängliche Preprint behauptet sogar mehr als die Entscheidung, ob eine Lösung existiert. Für jede feste Klauselbreite k ab zwei soll ein deterministischer Algorithmus die Anzahl sämtlicher erfüllender Belegungen einer k-CNF exakt bestimmen. Wer die Anzahl kennt, kann auch feststellen, ob sie null ist und damit die ursprüngliche Entscheidungsfrage beantworten.
Für Formeln mit n Variablen und m Klauseln nennt das Manuskript eine Laufzeit von einem polynomialen Faktor multipliziert mit 2 hoch O(n log log n geteilt durch die Quadratwurzel von log n). Bei einer festen oberen Schranke für das Verhältnis m zu n fällt der zusätzliche log-log-Faktor im Exponenten weg. Laut Preprint genügt dafür polynomial begrenzter Speicher. Diese Aussagen betreffen eine theoretische Obergrenze, nicht gemessene Geschwindigkeiten eines bereits eingesetzten Programms.
Die veröffentlichte Konstruktion übersetzt logische Formeln unter anderem in Netzwerke aus miteinander verbundenen Booleschen Bausteinen. An Knoten werden lokale Bedingungen beschrieben, während Verbindungen die Übereinstimmung gemeinsam genutzter Variablen erzwingen. Eine mathematische Zusammenfassung der Beiträge soll die Anzahl der Lösungen liefern, ohne jede mögliche Belegung ausdrücklich als vollständigen Datensatz durchzugehen.
Der technische Kern nutzt spezielle algebraische Umformungen, rekursive Zerlegungen und die kontrollierte Berechnung von Netzwerkbeiträgen. Das Manuskript beschreibt dafür eine sogenannte Tensor-Kontraktion und begrenzt die Zahl der Zwischenterme mithilfe arithmetischer Eigenschaften. Die Komplexität dieser Schritte erklärt, warum eine verständliche Kurzfassung allein kaum ausreicht, um die behauptete Laufzeitgarantie zu beurteilen.
OpenAI berichtet, sein Modell habe zunächst einen natürlichsprachlichen Beweis erzeugt und anschließend eine Formalisierung in Lean erstellt. Dieser Beweisassistent prüft, ob die einzelnen formal formulierten Ableitungen aus ihren Voraussetzungen folgen. Die veröffentlichte Lean-Dokumentation beschreibt ausdrücklich den Umfang der Formalisierung, darunter exaktes Zählen für kanonisch kodierte Formeln und eine subexponentielle Laufzeit mit polynomialem Speicher.
Eine maschinelle Prüfung ist ein starkes zusätzliches Indiz für die interne Konsistenz der formalisierten Argumentation. Fachleute müssen dennoch prüfen, ob die Formalisierung exakt die beanspruchte mathematische Aussage abdeckt, ob alle Voraussetzungen korrekt modelliert sind und ob sich die Konstruktion unabhängig nachvollziehen lässt. OpenAI selbst spricht bereits von einer Widerlegung, während die externe fachliche Prüfung ausdrücklich weiterläuft.
Die unabhängige Arbeitsgruppe wird von Russell Impagliazzo und Ramamohan Paturi von der University of California San Diego sowie Ryan Williams vom Massachusetts Institute of Technology geleitet. Damit sind zwei der ursprünglichen ETH-Forscher und ein ausgewiesener Experte für Algorithmen und Komplexitätsgrenzen beteiligt. Ihre Aufgabe ist es, die Ergebnisse gemeinsam mit weiteren Fachleuten zu untersuchen und verständlich einzuordnen.
Ihre Beteiligung dieser Wissenschaftler bedeutet noch keine abgeschlossene Bestätigung des Beweises. Nach Angaben von OpenAI soll die Gruppe unabhängig arbeiten, öffentlich diskutieren können und Zugang zu den Rohmaterialien erhalten. Für die Fachgemeinschaft liegt die eigentliche Bewährungsprobe deshalb in der nachvollziehbaren Kontrolle der mathematischen Details und der Reichweite des Ergebnisses.
Wenn die Widerlegung Bestand hat, verlieren zahlreiche Aussagen ihre bisherige bedingte Grundlage, sofern sie ausdrücklich auf ETH beruhen. Das betrifft unter anderem Fragestellungen aus Graphentheorie, Datenbanken und algorithmischer Biologie. Solche Resultate werden dadurch nicht automatisch falsch; häufig muss neu geklärt werden, welche unteren Laufzeitschranken weiterhin gelten und ob andere Begründungen möglich sind.
Eine Widerlegung der ETH wäre auch keine Lösung des berühmten Problems P gegen NP. Subexponentielle Algorithmen können weiterhin erheblich langsamer wachsen als polynomielle Verfahren und für realistische Eingabegrößen unpraktisch bleiben. Ob aus der behaupteten theoretischen Beschleunigung eines Tages schneller nutzbare Programme entstehen, hängt von weiteren algorithmischen Entwicklungen und konkreten Implementierungen ab.
Auf der mit Kreide geschriebenen Booleschen Formel stehen nur wenige Variablen und Klammern. Bei großen Formeln wächst die Zahl der denkbaren Wahr-falsch-Kombinationen explosionsartig. OpenAI beansprucht nun eine mathematisch nachgewiesene Abkürzung durch diesen Suchraum; ob sie tatsächlich trägt, müssen die laufenden unabhängigen Prüfungen zeigen.
OpenAI, Working with academic communities to build scientific understanding
OpenAI, The Exponential Time Hypothesis is False
OpenAI, Lean formalization scope for The Exponential Time Hypothesis is False
Mit KI-Unterstützung erstellt
Wählen Sie Forschung und Wissen bei Google als bevorzugte Quelle oder folgen Sie uns per RSS-Feed.
