Einen Tag nach der Veröffentlichung von 722 Mathematik-Manuskripten hat OpenAI drei davon zurückgezogen. Der Eintrag im Verlauf des Repositorys ist auf den 7. Oktober datiert und nennt den Grund: ein Vorzeichenfehler.
Ein Fehler, drei Papiere
Der Fehler steckt in „Algebraicity of Weil classes on split abelian eightfolds“. Er macht ein Argument über die Aufhebung einer Stabilisierungsspur ungültig, und damit auch die Konstruktion, auf der zwei weitere Arbeiten aufbauen. Zurückgezogen sind deshalb:
- Algebraicity of Weil classes on split abelian eightfolds
- Algebraicity of Kuga-Satake Correspondences for K3 Surfaces
- The rational Hodge conjecture for products of K3 surfaces
Die drei Seiten tragen jetzt einen Hinweis auf die Lücke und einen Link auf das archivierte Manuskript. Dazu hat OpenAI 14 weitere Arbeiten repariert, von geflickten Beweisschritten über korrigierte Aussagen bis zu einem veralteten Literaturverweis, und 13 Manuskripte bekamen neue Querverweise auf die überarbeiteten Fassungen. Sechs weitere Formalisierungen kamen hinzu. Formalisiert sind damit 300 von 719 Hauptergebnissen, also rund 42 Prozent.
Der Beratungskreis hat anderes empfohlen
OpenAI hatte sich vor der Veröffentlichung von einem Gremium beraten lassen: der Advisory Group on Mathematics and Artificial Intelligence, neun Forscher, angesiedelt am Institute for Advanced Study in Princeton. Ihre Richtlinien von Ende September beginnen mit der Bitte, aufzuhören, fortgeschrittene Mathematikprobleme an proprietären Modellen zu testen. Genau das beschreibt OpenAIs Veröffentlichung von sich selbst.
Andere Punkte hat OpenAI erfüllt: schnell veröffentlichen, mitteilen, wie die Modelle zu ihren Ergebnissen kamen. Beim nächsten wird es dünn. Die Gedankenkette des Modells liegt bei zehn der 719 Manuskripte offen.
Zwei Abweichungen zwischen Prosa und Lean
Parallel haben Mathematiker aus Cambridge und vom King’s College London ein Papier vorgelegt, das am Verfahren ansetzt. Ein Modell schreibt zuerst einen Beweis in natürlicher Sprache und übersetzt ihn dann nach Lean, wo der Compiler die Korrektheit prüfen soll.
Das Papier dokumentiert mindestens zwei Stellen, an denen Prosabeweis und Lean-Code auseinandergehen, bei einer Lösung zu einem Problem aus den Navier-Stokes-Gleichungen. Keine der beiden Fassungen ist damit widerlegt. Aber die Frage, ob ein Modell seine eigene Lösung ohne Menschen formalisieren darf, ist damit gestellt.
Terence Tao, seit Längerem Kritiker des Vorgehens, hat nach der Veröffentlichung geschrieben, Probleme würden autonom von KI-Promptern gelöst, die sich für das Feld selbst nicht interessierten und die Ausgabe nicht gut genug verstünden, um Fragen zum Ergebnis zu beantworten oder Vorträge zu halten.
Die Association for Human Mathematics ruft zum Abbruch auf
Deutlicher wird eine zweite Gruppe. In einer Stellungnahme vom 7. Oktober schreibt die Association for Human Mathematics, über 700 Dateien auf einmal zu veröffentlichen sei keine Demonstration von Gelehrsamkeit, sondern eine Demonstration von Macht. Sie fordert Mathematiker auf, die Zusammenarbeit mit OpenAI zu beenden.
Dass der Rückzug kam, ist die gute Nachricht
Ein Vorzeichenfehler, der zwei abhängige Arbeiten mitreißt, ist genau das, was Begutachtung finden soll. Dass er innerhalb eines Tages gefunden und protokolliert wurde, spricht für das öffentliche Repository und gegen die Vorstellung, hier sei etwas unprüfbar.
Das eigentliche Problem steht in der Zahl zehn. Wenn 709 von 719 Manuskripten ohne offene Gedankenkette dastehen und 419 ohne Formalisierung, dann liegt die Last der Nachvollziehbarkeit bei Leuten, die nicht gefragt wurden. Beide Gremien sagen dasselbe, nur in unterschiedlicher Lautstärke: Nicht das Lösen ist der Engpass, sondern das Verstehen danach. Das ist dieselbe Verschiebung, die Anthropic diese Woche bei Sicherheitslücken beschreibt.