Terence Tao: Vor einigen Wochen hat die KI den kritischen Punkt der mathematischen Formalisierung durchbrochen

Die „stärksten Gehirne“ der Mathematikwelt werden fast von den von KI generierten Beweisen überschwemmt.

Der Fields-Medaille-Träger Tao Zhexuan hat seine neuesten Erfahrungen im IEANTN-Projekt (Integrated Explicit Analytic Number Theory Network) geteilt:

Die KI generiert korrekte Beweise so schnell, aber die Beweise sind so sperrig, dass die Menschen gar nicht schnell genug prüfen können.

Formalisierungsaufgaben, die vor einigen Wochen noch von Freiwilligen mehrere Wochen in Anspruch nahmen, können jetzt von der KI in wenigen Stunden erledigt werden.

Ein Phänomen, das bereits ein Mathematiker des 17. Jahrhunderts, Pascal, bemerkte, plagt die moderne Mathematik auf eine ganz neue Weise:

Es ist einfacher, einen langen, korrekten Beweis zu generieren als einen kurzen, korrekten Beweis.

Tao Zhexuan nennt dieses Phänomen „Impedanzfehlanpassung“, und die KI hat diesen Widerspruch auf die Spitze getrieben.

Von Wochen auf Stunden

Das von Tao Zhexuan geleitete IEANTN-Projekt hat das Ziel, eine große Anzahl technischer Artikel in der expliziten analytischen Zahlentheorie zu formalisieren und in der Lean-Beweishelferin ein lebendes, dynamisch aktualisierbares Netzwerk von Zahlentheorie-Schätzungen aufzubauen.

Diese Arbeit beinhaltet eine große Anzahl lästiger numerischer Verifikationen und Parameteranpassungen.

Nach Tao Zhexuans eigenen Worten nimmt diese Art von Arbeit mindestens 70 % seiner Zeit in Anspruch, wenn er über Probleme der analytischen Zahlentheorie nachdenkt.

Nach der herkömmlichen Methode würde er einzelne Lemmata in unabhängige Aufgaben aufteilen und dann auf Freiwillige warten, die diese Aufgaben übernehmen – normalerweise musste er mehrere Wochen warten.

Da die manuelle Formalisierung an sich schwierig ist, streben die Freiwilligen natürlich eine kurze, effiziente und natürliche Beweisform an, und die Überprüfung des eingereichten Codes ist auch sehr einfach.

Aber in den letzten Wochen hat die automatische Formalisierungstechnik plötzlich einen gewissen Wendepunkt überschritten.

Fast jede Formalisierungsaufgabe, die Tao Zhexuan veröffentlicht hat, kann von KI-Tools innerhalb weniger Stunden erledigt werden.

Die Warteschlange der noch ungelösten Aufgaben im Projekt ist fast leer.

KI kann lokale Optimierungen vornehmen, aber keine globale Neukonstruktion

Der Sprung in der Geschwindigkeit hat unerwartete Nebenwirkungen gebracht.

Die von KI generierten formellen Beweise sind oft um Hunderte von Zeilen länger als die von Menschen geschriebenen, enthalten eine große Anzahl redundanter Schritte, und viele Lemmata werden nicht auf der richtigen Abstraktionsebene formuliert.

Betrachtet man jeden einzelnen Beweis, scheint es kein großes Problem zu sein, denn diese Beweise sind ja nicht für Menschen gedacht.

Aber jeder sperrige Beweis verlängert die Gesamtbauzeit des Projekts um einige Sekunden, und die kumulative Wirkung wird nicht mehr vernachlässigbar.

Tao Zhexuan nennt dies „Impedanzfehlanpassung“: Die Geschwindigkeitsunterschiede zwischen den drei Schritten der Beweisgenerierung, -verifikation und -verarbeitung werden immer größer.

Die Generierungsseite wird von der KI um mehrere Größenordnungen beschleunigt, aber die Verifikations- und Verarbeitungsseite hängt immer noch von der kognitiven Bandbreite der Menschen ab.

In der Praxis ist es eine herausfordernde Aufgabe, ein mittelgroßes Lean-Dokument mit Tausenden von Codezeilen (teilweise von KI generiert) in eine version zu überführen, die elegant strukturiert und für die Einreichung in die Mathlib-Mathematikbibliothek geeignet ist.

Tao Zhexuan hat eine klare Grenze der aktuellen KI-Tools entdeckt.

Wenn man die KI zu lokalen „Code Golf“ (Code-Vereinfachungen) auffordert, kann sie das gut machen und das Volumen des Beweises etwas reduzieren.

Aber globale Neukonstruktionsentscheidungen liegen weit außerhalb der Fähigkeiten der vorhandenen KI-Tools.

Beispielsweise kann man feststellen, dass ein Argument an mehreren Stellen im Dokument wiederholt auftritt und es in ein unabhängiges Lemma abstrahieren kann. Dieses Lemma kann möglicherweise auch außerhalb der aktuellen Datei noch weitere Anwendungen haben.

Tao Zhexuan hat darauf hingewiesen, dass er einer KI ein solches Neukonstruktionsschema erklären kann und die KI es dann ausführen kann, aber die KI kann solche Neukonstruktionsmöglichkeiten nicht von selbst entdecken.

KI ist gut darin, lokale, atomisierte Aufgaben zu bewältigen, aber sie versteht die globale Struktur eines Projekts nicht. Im Kontext des IEANTN-Projekts bedeutet dies, dass die KI schnell den Beweis für ein einzelnes Lemma generieren kann, aber nicht beurteilen kann, wie dieses Lemma in die Architektur des gesamten Zahlentheorie-Schätzungsnetzwerks eingebettet werden sollte.

Die Fortschrittsgeschwindigkeit des Projekts ist tatsächlich viel schneller als erwartet.

Aber Tao Zhexuan hat angegeben, dass er jetzt mehr Zeit darauf verwenden muss, den Umfang der Formalisierungsaufgaben im Voraus zu planen. Da er weiß, dass die KI schnell einen Beweis zurückliefern wird, muss er bei der Veröffentlichung der Aufgabe berücksichtigen, wie das Ergebnis leichter überprüft werden kann und besser mit der globalen Struktur des Projekts kompatibel ist.

Mit anderen Worten, der Engpass hat sich von „Auf Menschen warten, die den Beweis führen“ zu „Aufgaben so gestalten, dass die Ergebnisse der KI effektiv integriert werden können“ verschoben. Die Rolle der Mathematiker wandelt sich von der direkten Ausführung von Beweisen zu der eines Architekten der Beweis-Engineering.

Um diese Vision zu verwirklichen, muss jedes Puzzlestück auf der richtigen Abstraktionsebene und mit den richtigen Schnittstellenstandards im System existieren. Die KI kann Puzzlestücke mit erstaunlicher Geschwindigkeit produzieren, aber ob die Form der Puzzlestücke mit dem Gesamtplan übereinstimmt, kann derzeit nur der Mensch beurteilen.

Referenzlinks:

[1]https://mathstodon.xyz/@tao/116789374373843141

[2]https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/

Dieser Artikel stammt aus dem WeChat-Account „Liangziwei“. Autor: Meng Chen. Veröffentlicht von 36Kr mit Genehmigung.