OpenAI zufolge hat ein KI-Modell einen Weg gefunden, die Exponential Time Hypothesis (ETH) zu widerlegen – eine Informatik-Vermutung aus dem Jahr 1999. Der Anspruch hat keine Verbindung zu Ethereum, der Kryptowährung mit dem Ticker ETH, oder zum Ethereum-Mitgründer Vitalik Buterin.

Die Ankündigung löste dennoch Scherze auf Crypto Twitter aus. „Damn algo traders just slaughtered $ETH“, schrieb ein Nutzer namens Takumi auf X, während Andrew Jiang bemerkte: „Vitalik has been real quiet since this came out.“

Die fragliche ETH wurde von den Informatikern Russell Impagliazzo, Ramamohan Paturi und Francis Zane vorgeschlagen. Sie besagt, dass das Logikproblem 3-SAT nicht wesentlich schneller gelöst werden kann als durch die Prüfung jeder möglichen Variablenkombination. Bei 3-SAT geht es darum zu bestimmen, ob Wahrheitszuweisungen eine Sammlung von Regeln erfüllen können, wobei jede Regel drei Variablen enthält.

Hunderte wissenschaftliche Arbeiten haben sich auf die Hypothese gestützt, um nachzuweisen, dass bestimmte Probleme in der Graphentheorie, Computerbiologie, Datenbanktechnik und Geometrie nicht schnell lösbar sind, so OpenAI. Das Unternehmen erklärte, eine Widerlegung der ETH könnte die Frage erneut aufwerfen, wie viel schneller diese Aufgaben gelöst werden könnten, und Forschern bei der Suche nach besseren Algorithmen helfen.

„The refutation of the ETH reopens questions about how much faster these tasks could become“, schrieb OpenAI in seinem Blogbeitrag, „and may help guide the search for better algorithms.“

OpenAIs 67-seitiges Papier, datiert auf den 17. Oktober und überarbeitet am 25. Oktober, beschreibt einen deterministischen Algorithmus – einen ohne Zufallselement –, der alle erfüllenden Zuweisungen für diese Probleme in subexponentieller Zeit zählt. Das bedeutet, dass der Arbeitsaufwand langsamer wächst als jede Exponentialfunktion der Anzahl der Variablen. Da das Zählen der Lösungen schwieriger ist als die Frage, ob mindestens eine Lösung existiert, löst das Ergebnis auch das Entscheidungsproblem.

OpenAI teilte mit, seine KI habe die Widerlegung am 16. Oktober entdeckt, und das Ergebnis sei am 17. Oktober in Lean formalisiert worden – Software, die jeden logischen Schritt mechanisch verifiziert. Das Papier und die Formalisierung sind auf GitHub verfügbar. OpenAI erklärte, dies folge auf die Veröffentlichung von 722 mathematischen Manuskripten earlier im Monat, von denen nur 162 ein computerüberprüftes Hauptergebnis enthielten. Dieses maschinenprüfbare Format ermöglicht es unabhängigen Forschern, jeden Schritt des Arguments selbst zu verifizieren.

Impagliazzo, Paturi und der MIT-Professor Ryan Williams leiten eine unabhängige Prüfung des Anspruchs. In einem offenen Brief warnten sie davor, ihre Beteiligung als Zustimmung zu interpretieren.

„Our involvement should not be taken as certification of the claim“, schrieben die drei, und ergänzten: „a result of this significance requires careful, independent scrutiny and an understanding that others can reconstruct, question, and build upon.“

OpenAI erklärte, die Teilnehmer hätten keine Geheimhaltungsvereinbarungen unterschrieben und arbeiteten unbezahlt. Das Unternehmen verpflichtete sich zudem, alle Rohdaten zu veröffentlichen und eine Konferenz zu dem Ergebnis zu finanzieren.

Die praktischen Auswirkungen sind weiterhin ungewiss. „Finding such algorithms, and turning theoretical advances into practical improvements, will require significant further research“, schrieb OpenAI. Das Papier sagt auch, dass das Ergebnis nicht zeigt, dass jedes Problem in der Komplexitätsklasse NP in subexponentieller Zeit lösbar ist.

Das bedeutet, das Problem P versus NP bleibt offen. P umfasst Probleme, die Computer effizient lösen können, während NP Probleme umfasst, deren vorgeschlagene Lösungen sich effizient überprüfen lassen. Die offene Frage ist, ob jedes Problem, dessen Antwort sich effizient überprüfen lässt, sich auch effizient lösen lässt.

Anthropic stieg am 26. Oktober in die Diskussion ein – mit einem Papier, das Claude zugeschrieben wird und den Titel „A 2^o(n) Time Algorithm for 3-SAT“ trägt. Das Repository, das sich ebenfalls mit dem ETH-Problem befasst, erklärt, ein internes Forschungsmodell von Claude habe den Algorithmus entdeckt. Ergänzt wird, dass „the result is purely asymptotic and says nothing about solving formulas in practice.“

Claude hatte den Großen Satz von Fermat im September in Lean formalisiert. Der Mathematiker Terence Tao hatte vor der Möglichkeit sich überschneidender KI-Bemühungen gewarnt und im September geschrieben: „We have now seen that even the rumor of someone working on a problem can trigger a massive amount of AI-powered effort to flatten it before the original research project has time to reach its full potential.“

OpenAIs kürzlicher Beitrag von 5 Millionen US-Dollar an die Simons Foundation wird Workshops, Konferenzen und Sonderprogramme finanzieren, die Forschern dabei helfen sollen, KI-generierte Ergebnisse zu prüfen und darauf aufzubauen.

Quelle: Decrypt