OpenAI steht im scharfen Streit mit akademischen Mathematikern. Im Zentrum steht ein formal verifizierter Beweis. Der NYU-Mathematiker Tristan Buckmaster wirft OpenAI vor, sich die Anerkennung zu sichern.
Buckmaster und sein Mitautor Alpoege veroeffentlichten Lean-verifizierte Preprints zu den Euler-Gleichungen. Lean ist eine Sprache zur formalen Beweispruefung.
Ihre Arbeit beruehrt Probleme, die mit den Navier-Stokes-Gleichungen verwandt sind, berichtet Technology.org.
Hintergrund des Streits
Buckmaster behauptet, private Details seiner Forschung seien vor der Veroeffentlichung durchgesickert. Er wirft OpenAI vor, daraufhin einen massiven Rechenaufwand gestartet zu haben. Ziel sei es gewesen, seinem Team zuvorzukommen.
Die zugrunde liegenden Gleichungen betreffen Stroemungsdynamik und Turbulenzmodellierung.
Sie haengen mit einem der Millennium-Probleme zusammen. Formale Verifikation durch KI-gestuetzte Denkwerkzeuge hat solche mathematischen Arbeiten zuletzt stark beschleunigt.
Die Reaktion von OpenAI
OpenAI bestaetigte, am 1. September ein automatisiertes Reasoning-Projekt gestartet zu haben. Das Unternehmen begruendet dies mit Geruechten aus der Mathematik-Community. Man betont, die eigenen Modelle haetten ein unabhaengiges, neuartiges Manuskript erstellt.
OpenAI beteuert, sein System habe die Gleichungen angegangen, ohne private Arbeiten zu kopieren. Das Unternehmen sieht im Ergebnis einen Beleg fuer echte Denkfaehigkeit. Das aehnelt anderen Behauptungen der Branche ueber KI-Systeme auf Expertenniveau.
Scientific American beschrieb das Manuskript, ueber AI Weekly berichtet, als ungewoehnlich ausgefeilt. Das Modell naeherte sich demnach Gebieten nahe der Millennium-Probleme an. Diese Einordnung hat die Kritik am Zeitplan von OpenAI verschaerft.
Reaktionen der Mathematiker
Fields-Medaillist Terence Tao lobte oeffentlich die Fortschritte bei der Lean-Verifikation. Er betonte die wachsende Reibung zwischen menschlichen Forschern und fuehrenden KI-Labors. Formale Verifikation erhoehe die Einsaetze bei Streitfragen zur Urheberschaft, so Tao.
Forscher befuerchten, dass Anerkennungsregeln fuer menschliche Zusammenarbeit nicht mehr skalieren.
Preprints bewegen sich langsamer als automatisierte Systeme, die mit oeffentlichen Geruechten trainiert wurden. Dieses Missverhaeltnis befeuert derzeit die Spannungen in der Mathematik-Community.
Warum das wichtig ist
Der Streit stellt auf die Probe, wie Forschungsanerkennung im KI-Zeitalter funktioniert. Fuehrende Labors konkurrieren zunehmend direkt mit akademischen Forschern. Dieser Wandel koennte die Normen fuer Offenheit und Offenlegung neu formen.
Er zeigt zudem, wie weit KI bereits in die reine Mathematik vordringt. Aehnliche Spannungen koennten in anderen forschungsintensiven, von KI betroffenen Feldern entstehen. Vorerst warten beide Seiten auf das formale Peer-Review.
OpenAI hat bisher nicht erlaeutert, wie es Fragen der Urheberschaft angehen will. Buckmaster und Alpoege planen weitere Publikationen zur Verteidigung ihres Zeitplans. Laut Technology.org beobachtet die Mathematik-Community die Lage aufmerksam.
Was bedeutet das für die DACH-Region?
Deutsche und Schweizer Medien greifen den Streit intensiv auf. Die Sueddeutsche Zeitung analysierte, ob OpenAI unerlaubt Vorarbeiten anderer Mathematiker nutzte.
Die NZZ ordnete den Fall als moegliche „Jahrhundertkrise“ der Mathematik ein.
Terence Tao sagte der NZZ zufolge, es gebe kein Zurueck in die Zeit vor der KI. Auch die Deutsche Mathematiker-Vereinigung beobachtet solche Faelle aufmerksam. Fuer die DACH-Forschungslandschaft wirft der Streit Fragen zu Anerkennung und Kontrolle auf.
