KI widerlegt 90 Jahre altes Mathe-Rätsel: Der Beweisassistent war zuerst defekt

Ende Juli verkündete eine KI: Das Collatz-Problem, das Mathematikern seit knapp 90 Jahren Kopfzerbrechen bereitet, sei widerlegt – das Gegenbeispiel liege vor. Der Beweis war eine maschinell Zeile für Zeile überprüfbare „formale Verifikation“, die lückenlos schien. Doch noch bevor die Welt jubeln konnte, kam die Wahrheit ans Licht: Das vermeintliche Gegenbeispiel war eine Halluzination, hervorgebracht durch einen Soundness-Bug im mathematischen Prüfwerkzeug selbst. Ironischerweise besteht die Daseinsberechtigung dieses Werkzeugs genau darin, KI-Halluzinationen keine Chance zu geben.

Diese Geschichte verdient es, von Grund auf erzählt zu werden. Sie betrifft eine Frage, auf die wir derzeit kollektiv wetten: Wie viel Vertrauen verdienen die Aussagen einer KI wirklich?

Das 90 Jahre alte Problem verstehen

Die Regeln der Collatz-Vermutung sind so einfach, dass sie jedes Grundschulkind versteht: Man wähle eine beliebige positive ganze Zahl. Ist sie gerade, teilt man sie durch 2; ist sie ungerade, multipliziert man sie mit 3 und addiert 1. Dieses Verfahren wendet man fortlaufend auf das Ergebnis an.

Ein Beispiel: Beginnen wir mit 6. Da 6 gerade ist, teilen wir durch 2 und erhalten 3. 3 ist ungerade, also 3 * 3 + 1 = 10. 10 ist gerade, geteilt durch 2 ergibt 5. 5 ist ungerade, ergibt 16. Von dort geht es über 16 -> 8 -> 4 -> 2 -> 1. Und was passiert bei 1? 1 ist ungerade, 1 * 3 + 1 führt zurück zu 4 – eine unendliche Schleife 4-2-1 entsteht. Die Frage lautet schlicht: Landet man unabhängig von der Startzahl am Ende immer im 4-2-1-Zirkel?

Der deutsche Mathematiker Lothar Collatz stellte diese Frage im Jahr 1937. Bis heute konnte sie niemand beweisen, und niemand hat ein Gegenbeispiel gefunden. Computer haben bereits jede Zahl bis (2^{68}) (über 295 Trillionen) überprüft – alle kehrten zu 1 zurück. Doch Mathematiker lassen sich davon nicht beeindrucken: Das Überprüfen noch so vieler Zahlen gilt nicht als Beweis, genauso wenig wie das Beobachten von Milliarden weißer Schwäne beweist, dass alle Schwäne weiß sind. Der ungarische Mathematik-Großmeister Paul Erdős prägte das berühmte Zitat: „Die Mathematik ist möglicherweise noch nicht bereit für solche Probleme.“ Die Tücke der Aufgabe liegt in ihrer täuschenden Einfachheit – einfache Regeln, aber glitschig wie ein Aal.

Abb.: Der Zahlenbaum der Collatz-Vermutung – alle Zahlen, die in weniger als 20 Schritten 1 erreichen, hängen an diesem Baum. Quelle: Wikipedia (All Collatz sequences of a length inferior to 20)

Wie der vermeintliche KI-Durchbruch entstand

Am 25. Juli veröffentlichte der Informatiker Raman Kumar ein Code-Repository mit einer angeblichen „Widerlegung“: Eine konkrete Riesenzahl, von der aus man angeblich nie zur 1 zurückkehrt. Das Hauptverkaufsargument lautete, dass diese Widerlegung ein mit KI-Unterstützung erstellter, maschinell verifizierbarer Beweis sei.

Hierzu muss ein zentrales Konzept erläutert werden. In der modernen Mathematik hat sich die Praxis etabliert, Beweise als Code in einer speziellen Programmiersprache zu verfassen und sie einem „Beweis-Compiler“ namens Lean zu übergeben. Lean agiert wie der strengste Prüfer: Er zerlegt jeden Beweisschritt und prüft ihn Zeile für Zeile. Wird ein logischer Schritt übersprungen, schlägt Lean sofort Alarm. Ein von Lean akzeptierter Beweis kann theoretisch nicht falsch sein – genau das ist das explizite Designziel: Die Unnachgiebigkeit einer Maschine tritt an die Stelle menschlicher Versehen und Voreingenommenheiten bei der Begutachtung.

Die Tragweite dieses Werkzeugs ist enorm: Sicherheitskritische Betriebssystem-Kernel, Kryptowährungsprotokolle und zehntausende mathematische Theoremprüfungen stützen sich auf diese maschinelle Verifikation. In der Branche wurde Lean gar als ultimatives Mittel gegen KI-Halluzinationen gefeiert: Es spiele keine Rolle, ob die KI Unsinn erzählt, solange die Maschine das letzte Wort behält.

Als Kumar also ein „von Lean verifiziertes Gegenbeispiel“ vorlegte, war die Fachwelt zunächst erschüttert. Sollte der Beweis tatsächlich die maschinelle Prüfung bestanden haben, wäre das 90 Jahre alte Rätsel gelöst. Die Nachricht verbreitete sich rasend schnell in den sozialen Medien unter reißerischen Schlagzeilen: „KI widerlegt 90 Jahre altes Mathe-Rätsel“.

Die Wahrheit: Der Prüfer hat sich selbst verrechnet

Die Wendung folgte auf dem Fuße. Am 28. Juli reduzierte ein anderer Forscher den Beweis auf einen minimalen logischen Widerspruch und eröffnete ein Ticket im offiziellen Lean-Bugtracker unter der Nummer #14576. Der Titel des Bugs war unterkühlt: „kernel accepts ill-typed projection, allowing proof of false without premises.“ (Der Kernel akzeptiert fehlerhaft typisierte Projektionen, was den Beweis von Falschem ohne Prämissen erlaubt).

In einfachen Worten: Der angeblich unfehlbare Prüfer hatte in seiner zentralen Prüfroutine einen Schritt ausgelassen. Bei der Überprüfung verschachtelter Datentypen wurde an einer Stelle nicht kontrolliert, ob die Typnamen übereinstimmen. Dadurch schmuggelte sich ein fehlerhaftes Bauteil im KI-generierten Beweis durch die Lücke. Als die Maschine „Verifikation erfolgreich“ meldete, stempelte sie in Wahrheit eine Illusion ab.

Abb.: Trajektorien kleiner Zahlen unter den Collatz-Regeln, die alle in der 1 münden. Quelle: Wikipedia (Collatz graph, skipping 27)

Daraufhin folgte die dramatischste Szene des ganzen Falls. Die Lean-Community setzt seit jeher auf ein Konzept der doppelten Absicherung: Neben dem offiziellen Kernel-Prüfer existiert ein unabhängiger Verifizierer von Drittanbietern (geschrieben in einer anderen Sprache von einem anderen Team), der die Ergebnisse des offiziellen Kernels kreuzprüft. Diese Unabhängigkeitsannahme dient als Schmelzsicherung der gesamten Vertrauenskette.

Doch diesmal brannte die Sicherung durch. Die anschließende Postmortem-Analyse bestätigte, dass zwei voneinander unabhängige Bugs gleichzeitig getroffen werden mussten: Der offizielle Kernel versäumte die Prüfung verschachtelter Typen, während der unabhängige Prüfer bei der Projektionsprüfung an einer Stelle unaufmerksam war. Zwei Bugs, die in verschiedenen Ecken zweier unterschiedlicher Codebasen vergraben lagen, wurden von genau derselben „Widerlegung“ getriggert. Der Bug im unabhängigen Prüfer war zufällig erst eine Woche zuvor behoben worden, doch die KI nutzte eine Version vor diesem Fix. Lean-Schöpfer Leo de Moura schrieb in seiner Analyse gewohnt ehrlich, dass der Autor den Zeitpunkt zwar für einen Zufall halte, man aber nicht ausschließen könne, dass die KI den Bug-Report in ihren Trainingsdaten gesehen habe.

Wie ist das ingenieurtechnisch zu bewerten? Dass zwei unabhängige Implementierungen von derselben Kugel gleichzeitig durchschlagen werden, hat eine astronomisch geringe Wahrscheinlichkeit. Das bedeutet entweder extremes Pech – oder dass die Widerlegung exakt auf diese Lücke maßgeschneidert war. De Moura gab seine eigene Einschätzung ab: „Solche Vorfälle werden sich wiederholen. KIs sind extrem gut darin, Soundness-Bugs in Kerneln auszunutzen.“ Der Bug wurde innerhalb einer Stunde nach Einreichung behoben und ausgerollt. Das zeigt, dass die Kernel-Architektur selbst gesund ist – entdeckt wurde die Lücke jedoch erst durch den angeblichen KI-Durchbruch.

Wer überprüft die Prüfer?

Die Nachwirkungen dieses Vorfalls geben noch mehr zu denken als das Ereignis selbst. Nach Entdeckung der Lücke entsandte OpenAI einen auf Cybersicherheit spezialisierten KI-Forscher, um den Lean-Kernel zu auditieren. Dabei wurden weitere Programmierfehler im Kernel entdeckt und behoben. Mit anderen Worten: Das Werkzeug, das uns vor KI schützen soll, benötigt nun KI, um die eigenen Bugs zu finden.

Gleichzeitig deckt das Projekt „Lean in Lean“ (welches den Prüfer selbst in Lean verifizieren soll) den betroffenen Codeabschnitt noch nicht ab, und im portierten Code schlummerte exakt derselbe Bug. Verifikation verläuft in Schichten: Die Ergebnisse der KI werden vom Verifizierer kontrolliert, der Verifizierer von einer zweiten unabhängigen Implementierung. Doch wer kontrolliert die zweite Implementierung? Jede Ebene bringt zusätzlichen Aufwand und Kosten mit sich, aber eine „letzte Ebene“ gibt es nicht. Das entspricht der ingenieurmäßigen Realität: „Maschinell verifiziert“ ist stets eine probabilistische Eigenschaft – je tiefer und unabhängiger die Prüfung, desto geringer die Fehlerwahrscheinlichkeit, aber sie wird nie absolut null.

Für die Allgemeinheit liegt der größte Wert dieses Vorfalls in der Kalibrierung von Erwartungen. Wenn Sie das nächste Mal Schlagzeilen lesen wie „KI löst einhundert Jahre altes Mathe-Rätsel“ oder „KI beweist Theorem“, stellen Sie eine Frage mehr: Wurde es von Menschen oder Maschinen verifiziert? Und falls von Maschinen: Wurde die Maschine selbst verifiziert? Umgekehrt gibt es keinen Grund, in nihilistische Skepsis zu verfallen. Die Mathematik selbst blieb völlig unbeschädigt; das Collatz-Problem steht unverändert. Der Bug wurde offengelegt, behoben und in einer vorbildlichen Analyse dokumentiert. Das System hatte einen Bug, aber die Art und Weise, wie es ihn verdaut und korrigiert hat, ist genau der Grund, warum es unser Vertrauen verdient.

Vertrauen ist eine Kette, bei der jederzeit ein Glied brechen kann. Kluge Beobachter tun nicht so, als sei die Kette unzerstörbar – sie denken lediglich daran, jedes Glied regelmäßig zu überprüfen. Diesmal hat uns die KI einen Riss in einem der Glieder aufgezeigt – in Form eines falschen Durchbruchs.

Referenzlinks:

• Leo de Mouras Postmortem: Vollständige Analyse des Kernel-Soundness-Bugs #14576
• Lobsters-Diskussion (ojcl8j): Community-Diskussion zum Kernel-Bug (48 Punkte)
• Wikipedia: Collatz-Problem (Regelwerk, Geschichte und Verifikationsfortschritt)