Der Kampf um P vs. NP und 3-SAT
Stellt euch vor, ein fundamentales Axiom, auf dem seit Ende der 90er-Jahre hunderte wissenschaftliche Arbeiten aufbauen, löst sich an einem einzigen Nachmittag in Luft auf. Genau das soll Ende Oktober passiert sein: OpenAI und Anthropic veröffentlichten fast zeitgleich Publikationen, in denen ihre KI-Systeme eine zentrale Annahme der Informatik-Theorie, die sogenannte Exponentialzeithypothese (ETH) beim 3-SAT-Problem widerlegt haben wollen.
Fangen wir mal von vorne an. In unserem Fall mit diesem Video das schon paar Jahre auf dem Buckel hat, denn was in der Einleitung klingt wie ein trockenes Mathe-Rätsel, greift tief in eines der größten ungelösten Rätsel der Menschheit ein: das berühmte P-gegen-NP-Problem:
Ich greife gleich mal weit vor, denn in seinem aktuellen Video geht YouTuber Cedric, euch evtl. besser bekannt unter seinem Nick „The Morpheus“ der Sache auf den Grund, was die Jungs und Mädels von OpenAI und Anthropic nun gefunden haben wollen, baut den Lean-Beweis-Code lokal nach und hinterfragt, was es eigentlich bedeutet, wenn Maschinen wissenschaftliche Grundannahmen abräumen.
Schauen wir uns gemeinsam an, was da genau passiert ist und warum wir trotzdem nicht sofort den Champagner kaltstellen müssen.
Das Schalter-Rätsel: Was ist 3-SAT überhaupt?
Um zu verstehen, was KI da angeblich geknackt hat, stellen wir uns einfach einen riesigen Haufen Lichtschalter vor:
Jeder Schalter kennt nur zwei Zustände: AN oder AUS.
Dazu gibt es Regeln (Bedingungen), die jeweils höchstens drei Schalter betreffen (z. B. „Schalter 1 ist AN ODER Schalter 2 ist AUS ODER Schalter 3 ist AN“).
Die Frage: Gibt es eine Kombination aller Schalter, bei der alle Bedingungen gleichzeitig erfüllt sind?
Das ist das 3-SAT-Problem (Satisfiability Problem / Erfüllbarkeitsproblem). Bei 3 Schaltern gibt es nur 8 Möglichkeiten, das probiert man kurz im Kopf durch. Doch mit jedem weiteren Schalter verdoppelt sich die Anzahl der Möglichkeiten. Bei 100 Schaltern stößt selbst der stärkste Supercomputer beim stumpfen Ausprobieren an seine Grenzen.
Dabei begegnen uns SAT-Solver im Alltag ständig:
Linux-Paketmanager (wie apt, dnf oder zypper) lösen SAT-Probleme, um Abhängigkeiten von Softwarepaketen konfliktfrei aufzulösen.
Sudokus lassen sich 1:1 in SAT-Formeln übersetzen.
Tech-Riesen wie Amazon (Cloud-Rechte) oder Intel (Routing auf Mikrochips) nutzen Solver zur Verifizierung.
Das P vs. NP-Dilemma & die ETH
In der Theorie unterscheidet man zwischen zwei Klassen:
- P: Probleme, die sich schnell lösen lassen (in polynomieller Laufzeit).
- NP: Probleme, deren Lösung man zumindest schnell prüfen kann (wie ein fertig ausgefülltes Sudoku).
Seit 1971 ist bekannt, dass 3-SAT „NP-vollständig“ ist: Wer einen effizienten Algorithmus findet, der 3-SAT schnell löst, löst damit auf einen Schlag alle Probleme in NP (und entscheidet P = NP).
Hier ist ein schönes Video das nochmal ordentlich in die Tiefe geht:
Da bisher niemand P ≠NP beweisen konnte, behelfen sich Informatiker seit 1999 mit der Exponentialzeithypothese (ETH) von Impagliazzo und Paturi. Diese besagt vereinfacht: Egal wie schlau der Algorithmus ist, der Rechenaufwand pro Schalter bei 3-SAT bleibt exponentiell. Darauf baut eine ganze Pyramide an Schranken auf: Fällt die ETH, fallen auch die Schranken für hunderte andere Algorithmen.
Der Doppel-Schlag: Was OpenAI & Anthropic behaupten
Am 26. Oktober behauptete OpenAI, mit ihren Forschungs-KIs die ETH widerlegt zu haben. Knappe 6 Stunden später zog Anthropic nach, aber mit einem komplett anderen mathematischen Ansatz (auf Basis des Gitterschnitts und der 8-Quadrate-Identität).
Beide Beweise zeigten (formal verifiziert im Beweis-Assistenten Lean), dass der Faktor pro Schalter bei sehr großen Formeln unter jeden festen Wert gedrückt werden kann. Tatsächlich wächst somit der Aufwand langsamer als jede klassische Exponentialfunktion.
Das Morpheus-Video: Wenn der Rechner den Beweis prüft
Wie fundiert ist das Ganze? In seinem sehr ausführlichen Video zeigt Cedric/Morph, was genau passiert, wenn man den Lean-Code lokal kompiliert und laufen lässt:
Die wichtigsten Erkenntnisse aus dem Video:
Machine-Checked: Der Beweis von Anthropic lief sauber durch Lean durch und wurde sogar von einem unabhängigen Prüftool (Typechecker) als valide akzeptiert.
Keine versteckten Tricks: Morph hat nachgeprüft, ob schmutzige Extra-Axiome eingebaut wurden, um den Beweis vorzugaukeln. Fehlanzeige, es kamen nur Leans Standard-Axiome zum Einsatz. Soweit, sogut.
Der Haken mit der Semantik: Lean prüft nur, ob die Logik innerhalb der mathematischen Typen korrekt abgeleitet wurde. Ob die formalen Definitionen im Code aber wirklich exakt das bedeuten, was das Paper in Worten beschreibt, kann die Maschine (noch) nicht prüfen.
„Ein durchgelaufener Build allein sagt uns natürlich überhaupt nichts […] Ob die Datei überhaupt das sagt, was das Paper meint, das muss tatsächlich immer noch ein Mensch lesen.“
Fazit: Zerstörte Forschung oder KI-Halluzination auf hohem Niveau?
Dass zwei völlig unterschiedliche KI-Modelle wie eingangs erwähnt am selben Tag über zwei verschiedene mathematische Wege zum selben Ergebnis kommen, verleiht der Sache eine gewisse Wertigkeit.
Sollten sich die Beweise nach der Peer-Review durch richtig echte menschliche Spitzenmathematiker als lückenlos erweisen, wären wohl irgendwas über 800 Forschungsarbeiten der letzten 27 Jahre quasi obsolet.
Es zeigt vor allem eines: KI wird vom reinen Werkzeug zum aktiven Partner in der Grundlagenforschung. Es stellt uns Menschen aber gleichzeitig vor das grundsätzliche Problem, diese gewaltigen Gedankengänge überhaupt noch nachvollziehen zu können.
Schaut euch unbedingt auch dieses Video von Morph an, wenn ihr in die Richtung mehr sehen wollt, denn es ist noch gar nicht so lange her als es zum letzten Mal in der theoretischen Mathematik zu einem der Millennium-Probleme Beef gab: