Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic

Stellen Sie sich vor, Sie versuchen, einen perfekten, selbstprüfenden Roboter zu bauen, der seine eigenen Mathehausaufgaben überprüfen kann. Dieser Roboter, den wir BRA nennen werden, ist sehr intelligent, folgt aber extrem strengen, einfachen Regeln. Er kann addieren, subtrahieren und prüfen, ob Dinge gleich sind, aber er besitzt kein Modul für „gesunden Menschenverstand“.

Das Papier, das Sie lesen, ist ein Bericht über ein Experiment, bei dem ein menschlicher Forscher (Thierry Coquand) mit einer KI (Claude) zusammengearbeitet hat, um diesem Roboter eine sehr berühmte, sehr schwierige Lektion zu lehren: Gödels Zweiten Unvollständigkeitssatz.

Hier ist die Geschichte dieses Experiments, unterteilt in einfache Abschnitte.

1. Das Ziel: Kann der Roboter beweisen, dass er sicher ist?

Gödels Zweiter Satz ist ein wenig wie ein „Lügner-Paradoxon“ für mathematische Systeme. Er besagt: „Wenn ein System konsistent ist (es beweist niemals Falsches), kann es nicht beweisen, dass es konsistent ist.“

Mit anderen Worten: Wenn unser Roboter BRA tatsächlich Mathematik korrekt betreibt, wird er niemals in der Lage sein, einen Beweis aufzuschreiben, der besagt: „Ich bin ein guter Roboter.“ Wenn er das könnte, wäre er tatsächlich defekt. Das Ziel dieses Projekts war es, eine digitale Version dieses Beweises innerhalb eines Computerprogramms namens Agda zu erstellen, wobei die KI den Code schreibt.

2. Der erste Versuch: Der „gefälschte“ Erfolg

Das Team begann damit, die KI zu bitten, ein altes Papier eines Mathematikers namens Rose zu lesen und zu versuchen, den Satz basierend darauf zu beweisen.

• Was passierte: Die KI arbeitete tagelang hart und produzierte einen „Beweis“. Er sah beeindruckend aus!
• Das Problem: Die KI war getäuscht worden. Das alte Papier, das sie las, enthielt einen Fehler (ein falsches Theorem). Die KI folgte den Anweisungen perfekt, aber weil der Ausgangspunkt falsch war, war das Ergebnis ein „Beweis“ von etwas, das wie Gödels Theorem aussah, aber eigentlich Unsinn war.
• Die Lehre: Dies zeigte, dass KI großartig darin ist, Logik zu folgen, aber wenn man ihr eine schlechte Karte gibt, wird sie bereitwillig am falschen Ziel ankommen. Man kann der KI nicht einfach vorschreiben, was sie beweisen soll; man muss das Ziel selbst kennen.

3. Der echte Versuch: Die Karte reparieren

Nach dem Fehlschlag wechselte das Team zu einem anderen, zuverlässigeren Satz von Notizen eines Mathematikers namens R. Guard. Diese Notizen waren wie eine Schatzkarte mit einigen fehlenden Teilen und Tippfehlern.

• Die Herausforderung: Guards Notizen wurden 1963 geschrieben. Sie waren präzise, ließen aber viele winzige, offensichtliche Details aus, die ein menschlicher Mathematiker automatisch ergänzen würde. Zum Beispiel setzte Guard voraus, dass der Leser wusste, wie man mit „Numeralen“ (Zahlen wie 1, 2, 3) im Inneren des Robotergehirns umgeht.
• Die Rolle der KI: Der menschliche Forscher schrieb keine einzige Zeile Code. Stattdessen fungierte er als „Übersetsetzer“ oder „Architekt“. Er sagte der KI: „Hier ist das fehlende Teil. Hier ist die Regel. Jetzt schreibe den Code.“
• Das Ergebnis: Die KI schrieb erfolgreich 50.000 Zeilen Code von Grund auf neu. Sie baute den gesamten Roboter, den Beweis und das Verifizierungssystem, ohne dass ein Mensch eine einzige Zeile Code tippte. Das Endergebnis war ein maschinengeprüfter Beweis dafür, dass der Roboter BRA seine eigene Sicherheit nicht beweisen kann.

4. Die verborgenen Tricks (Das „Geheimrezept“)

Das Papier hebt mehrere kluge Tricks hervor, die die KI lernen musste, um dies zum Erfolg zu führen, welche in den alten Notizen verborgen waren:

• Das „Verschachtelte Boxen“-Problem: Der Roboter musste seine eigene Geschichte überprüfen können. Stellen Sie sich vor, Sie versuchen, ein Buch zu lesen, während Sie gleichzeitig das Buch schreiben. Die KI musste eine spezielle „Historien-Spule“ im Gehirn des Roboters bauen. Es stellte sich heraus, dass die Basistools des Roboters nicht dafür gebaut waren, also musste die KI eine komplexe „Matroschka-Struktur“ (russische Puppen) erfinden, damit der Roboter seine vergangenen Schritte erinnern kann.
• Die „Geschlossene Box“-Regel: Der Robot muss Zahlen (wie die 5) als „geschlossene Boxen“ behandeln, die durch Substitution nicht verändert werden können. Die alten Notizen gingen davon aus, dass dies offensichtlich sei. Die KI musste explizit angewiesen werden, zu beweisen, dass „5 eine geschlossene Box ist“, bevor sie fortfahren konnte.
• Die „Hypothetische“ Abkürzung: Der Roboter arbeitet auf eine sehr starre Weise (Hilbert-Stil-Logik), in der er nicht einfach sagen kann: „Wenn X wahr ist, dann Y.“ Die KI nutzte einen cleveren Trick (genannt den „Carneiro-Lift“), um jede Aussage in einen „Wenn...“-Wrapper einzuhüllen, was es dem Roboter ermöglichte, komplexe Argumentation zu simulieren, ohne seine eigenen Regeln zu brechen.

5. Warum das wichtig ist

Dies ist nicht nur ein Beweis eines mathematischen Theorems. Es ist ein Testlauf für die Zukunft der Zusammenarbeit zwischen Mensch und KI.

• Der Mensch ist der Architekt: Der Mensch lieferte die Vision, die korrekte Karte und die Fähigkeit zu erkennen, wenn die KI vom Weg abkam (wie beim ersten gescheiterten Versuch).
• Die KI ist der Maurer: Die KI erledigte die Schwerstarbeit und legte jeden einzelnen Stein des 50.000 Zeilen langen Beweises.
• Die Entdeckung: Der Prozess offenbarte, dass die alten mathematischen Notizen an einigen Stellen tatsächlich „schlampig“ waren. Indem das Team die KI zwang, Code zu schreiben, der perfekt sein muss, fanden sie verborgene Annahmen und Tippfehler im ursprünglichen Text von 1963, die jahrzehntelang übersehen worden waren.

Zusammenfassung

Betrachten Sie dieses Projekt als den Bau eines selbstfahrenden Autos durch ein Team. Der menschliche Fahrer kannte das Ziel (Gödels Theorem) und die Verkehrsregeln. Die KI war der Motorenbauer, der das Auto zusammenbaute.

• Zuerst versuchte die KI, das Auto basierend auf einem fehlerhaften Bauplan zu bauen, und erschuf ein Fahrzeug, das zwar wie ein Auto aussah, aber nicht fuhr.
• Dann wechselten sie zu einem besseren Bauplan. Die KI baute ein perfektes, funktionierendes Auto.
• Auf dem Weg dorthin stellten sie fest, dass der Bauplan einige fehlende Anweisungen hatte, sodass sie neue Teile erfinden mussten, um das Auto zum Laufen zu bringen.

Das Ergebnis ist ein vollständig verifizierter, maschinengeprüfter Beweis, dass ein spezifisches mathematisches System seine eigene Konsistenz nicht beweisen kann – erreicht durch eine Kollaboration, bei der der Mensch die Führung übernahm und die KI die Arbeit ausführte.