Mathematiker stellen die Verlässlichkeit von OpenAIs 719 KI-generierten Mathematikmanuskripten infrage, nachdem ein neues Paper darauf hinweist, dass der von OpenAI präsentierte Navier-Stokes-Beweis nicht vollständig mit seiner formal in Lean geprüften Fassung ü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 voneinander abweichen.
- Die Autoren erklären den Beweis nicht für falsch, betonen aber, dass maschinelle Prüfungen das Peer Review nicht ersetzen können.
OpenAIs Mathematik-Offensive
OpenAI stellte die Sammlung am 6. Oktober online. Ein am Donnerstag veröffentlichter Bericht kommt zu dem Schluss, dass das Projekt von Leitlinien abweicht, die ein unabhängiges Gremium von Mathematikern für KI-Labore formuliert hat. Der Katalog startete mit 722 Manuskripten. Bereits einen Tag später zog OpenAI drei davon zurück, nachdem ein Vorzeichenfehler ein Argument zerstört hatte und zwei weitere Arbeiten davon abhingen.
Diese Leitlinien wurden am 29. September vom neunköpfigen Advisory Group on Mathematics and Artificial Intelligence veröffentlicht. Gleich zu Beginn wird darin gefordert, dass Labore aufhören, schwierige Mathematikaufgaben auf proprietären Modellen zu testen. Laut OpenAIs Repository stammen die Manuskripte aus Tests eines unveröffentlichten internen Modells an offenen Forschungsproblemen.
Erläuternde Zusammenfassungen zum „Reasoning“ des Modells gibt es nur zu 10 Resultaten; rund 42 % der präsentierten Hauptaussagen wurden in Lean formalisiert – einer Programmiersprache, mit der sich Beweise maschinell verifizieren lassen.
Lesen Sie außerdem: Wie viel verdient der CEO von Anthropic? Der IPO-Prospekt liefert die Antwort
Lücken im Navier-Stokes-Beweis
Alexander Bastounis vom King's College London sowie Fabian Circelli und Anders Hansen von der University of Cambridge haben den von OpenAI im September angekündigten Navier-Stokes-Beweis unter die Lupe genommen. Sie dokumentieren zwei Stellen, an denen das schriftliche Argument und der Lean-Code auseinanderlaufen – darunter eine, bei der der Code nur eine schwächere Abschätzung beweist, als sie im Manuskript beansprucht wird.
Die Autoren betonen, dass sie keine Aussage darüber treffen, ob der schriftliche Beweis inhaltlich korrekt ist. Ihr Punkt ist präziser: Lean bestätigt zwar, dass der abschließende Satz gilt, aber das System garantiert nicht, dass die im Paper präsentierten Zwischenschritte, die Menschen lesen, tatsächlich sauber hergeleitet sind. Solche Beweise benötigen daher weiterhin klassisches Peer Review.
Fields-Medaillenträger Terence Tao schrieb am 6. Oktober, dass derzeit Probleme von „KI-Propmptern“ gelöst würden, die die Ergebnisse nicht tief genug verstünden, um Rückfragen zu beantworten oder Vorträge dazu zu halten. Die Harvard-Professorin Melanie Matchett Wood, Mitglied der Advisory Group, sagte, beim Erscheinen solcher Resultate verstehe zunächst kein Mensch den vollen Gehalt: „Jetzt beginnt erst die eigentliche Arbeit.“
Streit um OpenAIs Beweise
Die Advisory Group verweist darauf, dass letztlich nur die breitere mathematische Fachgemeinschaft beurteilen könne, wie eng OpenAI ihre Empfehlungen befolgt hat. Die Debatte folgt auf einen angespannten Monat: OpenAI hatte das Navier-Stokes-Resultat am 8. September vorgestellt – und damit einen Urheberstreit mit dem NYU-Mathematiker Tristan Buckmaster ausgelöst. Nur drei Tage später veröffentlichten 25 Fields-Medaillenträger eine Erklärung, in der sie warnten, massenhaft erzeugte KI-Beweise könnten dem Fachgebiet schaden.
Weiterlesen: OpenAIs 722 KI-Mathematik-Papers sind öffentlich – jetzt ist die Fachwelt am Zug
