Die Mathematikgemeinschaft stellt grundlegende Fragen dazu, inwieweit den 719 von OpenAI veröffentlichten KI-generierten mathematischen Manuskripten zu trauen ist. Anlass dafür ist eine aktuelle Arbeit, die darauf hinweist, dass der zuvor von OpenAI vorgestellte Navier-Stokes-Beweis nicht exakt mit dem vom Computer verifizierten Lean-Code übereinstimmt.

Die wichtigsten Punkte

• Nachdem ein Vorzeichenfehler aufgedeckt wurde, sank die Zahl der mathematischen KI-Manuskripte von OpenAI von 722 auf 719.

• Drei britische Mathematiker fanden im Navier-Stokes-Beweis zwei Stellen, an denen der schriftliche Beweis und der Lean-Code voneinander abweichen.

• Die Autoren der Arbeiten behaupten zwar nicht, dass die Beweise selbst falsch seien, betonen aber, dass eine maschinelle Überprüfung das Peer-Review-Verfahren nicht ersetzen kann.

OpenAIs Veröffentlichung zu KI-Mathematik

OpenAI veröffentlichte am 6. Oktober eine umfangreiche Sammlung mathematischer Beweise. Ein am Donnerstag erschienener Analysebericht wies darauf hin, dass diese Arbeit von den Leitlinien abweiche, die ein unabhängiges Gremium von Mathematikern für KI-Labore formuliert hatte. Bei der Erstveröffentlichung umfasste der Katalog 722 Arbeiten. OpenAI zog jedoch drei davon zurück, nachdem Vorzeichenfehler entdeckt worden waren, durch die eine Argumentationskette zusammenbrach und zwei weitere Arbeiten, die darauf aufbauten, ebenfalls infrage gestellt wurden.

Die Leitlinien wurden am 29. September von der neunköpfigen Advisory Group on Mathematics and Artificial Intelligence veröffentlicht. Gleich im ersten Satz fordern sie die Labore auf, „fortgeschrittene mathematische Probleme nicht mit geschlossenen kommerziellen Modellen zu testen“. Im OpenAI-Repository heißt es dagegen, die Arbeiten seien durch den Einsatz geschlossener interner Modelle auf nicht veröffentlichte Forschungsprobleme entstanden.

Nur 10 der gesamten Ergebnisse enthalten eine Erläuterung, die den Denkprozess des Modells zusammenfasst. Nur etwa 42 % der wichtigsten Endergebnisse sind in Lean formalisiert – einer Programmiersprache, mit der mathematische Beweise maschinell überprüft werden können.

Auch lesenswert: Wie viel verdient der CEO von Anthropic pro Jahr? Die Vergütungsvereinbarung, die aus den IPO-Unterlagen hervorgeht

Navier-Stokes-Beweis: Wo ging etwas schief?

**Alexander Bastounis** vom King's College London sowie Fabian Circelli und **Anders Hansen** von der University of Cambridge untersuchten eingehend einen Beweis zu den Navier-Stokes-Gleichungen, den OpenAI im vergangenen September als „gelöst“ vorgestellt hatte. Sie fanden zwei Stellen, an denen die schriftliche Arbeit und der Lean-Code voneinander abwichen. An einer davon stellte sich heraus, dass der Lean-Code lediglich eine schwächere Form der Abschätzung beweist als die in der Arbeit behauptete.

Die Autoren ließen offen, ob die schriftlichen Beweise richtig oder falsch sind. Der Streitpunkt ist enger gefasst: Lean kann zwar bestätigen, dass der endgültige Satz gilt, aber nicht gewährleisten, dass alle Zwischenschritte der für Menschen lesbaren Argumentation stichhaltig sind. Sie betonen daher, dass auch diese Art KI-gestützter Beweise letztlich einem menschlichen Peer-Review-Verfahren unterzogen werden muss.

Der Fields-Medaillist **Terence Tao** kritisierte am 6. Oktober in einem Beitrag, dass die aktuellen Probleme zwar von „KI-Promptern“ gelöst würden, diese die Ergebnisse aber nicht ausreichend verstünden und deshalb kaum in der Lage seien, Fragen dazu zu beantworten oder sie in Seminaren vorzustellen. Melanie Matchett Wood, Mitglied des Beirats und Professorin an der Harvard University, sagte ebenfalls, dass zum Zeitpunkt der Veröffentlichung solcher Ergebnisse „noch niemand das Ganze versteht und die eigentliche Arbeit erst jetzt beginnt“.

OpenAI-Beweis wird zum Vertrauensstreit

Der Beirat hat klargestellt, dass letztlich die Mathematikgemeinschaft in ihrer Gesamtheit – weit gefasst – beurteilen muss, inwieweit OpenAI den Empfehlungen gefolgt ist. Die Kontroverse um die Überprüfung kommt nach einem bereits angespannten Monat.

OpenAI stellte am 8. September ein Ergebnis zu den Navier-Stokes-Gleichungen vor. Darauf folgte unmittelbar ein Streit über die Zuordnung der wissenschaftlichen Leistung mit dem NYU-Mathematiker **Tristan Buckmaster**. Drei Tage nach der Ankündigung veröffentlichten 25 Fields-Medaillisten eine gemeinsame Erklärung, in der sie davor warnten, dass die massenhafte Produktion von KI-generierten Mathematikergebnissen dem akademischen Ökosystem schaden könnte.

Weiterer Artikel: OpenAIs 722 veröffentlichte KI-Mathematikarbeiten – nun sind die Mathematiker mit der Bewertung an der Reihe