Mathematiker stellen die Vertrauenswürdigkeit der 719 KI-generierten Mathematik-Manuskripte von OpenAI infrage. Auslöser ist ein neues Paper, wonach der von OpenAI präsentierte Navier-Stokes-Beweis in der schriftlichen Fassung nicht mit der formal verifizierten Version in Lean übereinstimmt.
Zentrale Punkte:
- OpenAIs Katalog ist von 722 auf 719 Manuskripte geschrumpft, nachdem das Unternehmen drei Arbeiten wegen eines Vorzeichenfehlers zurückgezogen hat.
- Drei Mathematiker aus Großbritannien dokumentieren zwei Stellen, an denen der schriftliche Navier-Stokes-Beweis und der Lean-Code auseinanderlaufen.
- Die Autoren erklären den Beweis nicht für falsch, betonen aber, dass maschinelle Checks keine fachliche Begutachtung ersetzen.
OpenAI-Math-Offensive
OpenAI veröffentlichte die Sammlung am 6. Oktober. Ein am Donnerstag erschienener Bericht stellt fest, dass das Projekt von Leitlinien abweicht, die ein unabhängiges Gremium von Mathematikern für KI-Labore formuliert hat. Der Katalog umfasste zunächst 722 Manuskripte. Bereits einen Tag später zog OpenAI drei davon zurück, nachdem ein Vorzeichenfehler ein Argument zerstörte und zwei weitere Arbeiten betraf, die darauf aufbauten.
Diese Leitlinien, am 29. September vom neunköpfigen Advisory Group on Mathematics and Artificial Intelligence veröffentlicht, beginnen mit der Forderung, dass Labore keine hochkomplexen Mathematikprobleme mehr an proprietären Modellen testen sollten. Laut OpenAIs Repository stammen die Arbeiten jedoch aus Tests eines bislang unveröffentlichten internen Modells an offenen Forschungsproblemen.
Begleitende, für Menschen lesbare Zusammenfassungen der Modellüberlegungen gibt es nur zu 10 Resultaten. Rund 42 % der Resultate „auf oberster Ebene“ sind in Lean formalisiert – einer Sprache, mit der Computer Beweise Schritt für Schritt prüfen können.
Mehr dazu: Wie viel verdient der CEO von Anthropic? Börsenprospekt liefert Details
Lücken im Navier-Stokes-Beweis
Alexander Bastounis vom King’s College London sowie Fabian Circelli und Anders Hansen von der University of Cambridge unterzogen den von OpenAI im September verkündeten Navier-Stokes-Beweis einer Detailanalyse. Sie dokumentierten zwei Punkte, an denen die schriftliche Argumentation und der Lean-Code auseinandergehen – darunter eine Stelle, an der der Code nur eine schwächere Abschätzung beweist, als im Paper behauptet wird.
Die Autoren äußern sich ausdrücklich nicht dazu, ob der schriftliche Beweis korrekt ist oder nicht. Ihr Anliegen ist präziser: Lean bestätigt zwar, dass der abschließende Satz gilt, kann aber nicht garantieren, dass die zwischengeschalteten Argumentationsschritte, die Menschen lesen, inhaltlich sauber sind. Auch formal verifizierte Beweise bräuchten daher weiterhin eine klassische Peer-Review.
Fields-Medaillenträger Terence Tao schrieb am 6. Oktober, Probleme würden derzeit von „KI-Promptern“ gelöst, die die ausgegebenen Ergebnisse nicht gut genug verstehen, um dazu Fragen zu beantworten oder Vorträge zu halten. Die Harvard-Professorin Melanie Matchett Wood, Mitglied der Expertengruppe, betonte, beim Erscheinen solcher Resultate verstehe zunächst kein Mensch den vollständigen Inhalt – „und damit beginnt erst die eigentliche Arbeit“.
Streit um OpenAIs Beweise
Die Expertengruppe betont, nur die breitere mathematische Community könne beurteilen, wie eng OpenAI den Empfehlungen tatsächlich gefolgt ist. Diese Prüfung folgt auf einen angespannten Monat. OpenAI hatte das Navier-Stokes-Resultat am 8. September verkündet – und damit einen Prioritätsstreit mit dem New-York-University-Mathematiker Tristan Buckmaster ausgelöst. Drei Tage später veröffentlichten 25 Fields-Medaillenträger eine Erklärung, in der sie warnen, massenhaft produzierte KI-Ergebnisse könnten der Entwicklung des Fachs schaden.
Weiterlesen: OpenAIs 722 KI-Math-Papers sind öffentlich – nun müssen Mathematiker urteilen
