OpenAI veröffentlicht 722 mathematische Manuskripte, die ein bislang namenloses internes Modell erzeugt hat. Ein Teil der Beweise lässt sich von Maschinen prüfen, ein Teil nicht.
OpenAI öffnet das Repository openai/math mit 722 Manuskripten
Am 6. Oktober ist auf GitHub das Repository openai/math erschienen. OpenAI hat dazu einen Beitrag mit dem Titel „Sharing AI progress in mathematics" veröffentlicht. Das Repository enthält 722 mathematische Manuskripte, die in 372 Forschungsfamilien gruppiert sind.
Erzeugt wurden die Ergebnisse laut OpenAI von einem internen Frontier-Modell, das weder einen Namen noch einen Preis noch eine API hat. Das Unternehmen nennt es nur ein internes Modell. Nach eigenen Angaben lösen oder treiben die Manuskripte bedeutende offene Probleme aus der Mathematik und der theoretischen Informatik voran. Für die Öffentlichkeit ist ein solcher Vorstoß ungewöhnlich, weil die Ergebnisse nicht von bekannten Werkzeugen stammen, die jeder nutzen kann.
Warum 722 Manuskripte nicht automatisch 722 Beweise sind
Der wichtigste Unterschied liegt nicht in der Menge, sondern in der Prüfbarkeit. OpenAI schreibt selbst, die Sammlung enthalte Ergebnisse in unterschiedlichen Stadien der Überprüfung. Die stärkste Form des Belegs ist eine Formalisierung in Lean. Lean ist eine Programmiersprache, mit der sich mathematische Beweise von einem Computer prüfen lassen, ähnlich wie ein Compiler ein Programm auf Fehler prüft. Stimmt ein Lean-Beweis, ist er korrekt, weil der Rechner jeden einzelnen Schritt nachrechnet und kein Schritt übersehen werden kann.
Nicht alle Manuskripte haben aber eine solche Formalisierung. Bei diesen liegt die Prüfung bei Menschen, und dort können Fehler vorkommen. OpenAI räumt ein, dass einige der nicht formalisierten Ergebnisse Probleme haben könnten, und verspricht, solche Fälle rasch zu korrigieren. Der Unterschied zwischen einem Lean-geprüften und einem nicht geprüften Ergebnis ist für Leser entscheidend, denn nur bei der ersten Gruppe steht die Korrektheit rechnerisch fest und nicht bloß auf dem Papier.
Für die Veröffentlichung hat sich OpenAI von der unabhängigen „Advisory Group on Mathematics and Artificial Intelligence" am Institute for Advanced Study beraten lassen. Das Repository arbeitet mit Regeln für Überarbeitungen und Zitate, damit die Ergebnisse nachvollziehbar bleiben.
Wie das namenlose Modell die Aufgaben bearbeitet hat
OpenAI liefert zum Ablauf einige Details. Das Modell bearbeitete die Probleme und erzeugte Argumente, die anschließend von Menschen mit demselben Modell zu Manuskripten ausgearbeitet wurden. Danach hat das Modell jedes Argument in ein Lean-Zertifikat formalisiert, das sich maschinell nachrechnen lässt.
Zum Rechenaufwand nennt OpenAI eine greifbare Größe: Das Ergebnis einer durchschnittlichen Aufgabe entsprach ungefähr drei Stunden Denkleistung auf dem Niveau von ChatGPT Pro. Das klingt viel, bleibt aber im Verhältnis überschaubar. Die vollständigen Token-Kosten, um Lösungen für diese Probleme zu finden, würden nach OpenAI-Angaben bei Sol-API-Preisen etwa 2.000 Dollar betragen. Für ein Paket mit mehreren hundert Forschungsfamilien ist das ein bemerkenswerter Betrag.
Allerdings hält OpenAI das Modell selbst zurück. Das Unternehmen will die internen Frontier-Modelle weiter testen und erst dann mit aller gebotenen Vorsicht veröffentlichen. Nutzer bekommen also die Ergebnisse, aber nicht das Werkzeug, das sie erzeugt hat. Warum diese Trennung? Wer ein Modell mit dieser Leistungsfähigkeit in die Hände bekommt, könnte damit auch andere, weit schwerer zu prüfende Aufgaben lösen, und darauf hat OpenAI bislang keine Antwort, außer dem Versprechen weiterer Tests.
Was unabhängige Prüfer bisher sagen
Die unabhängige Überprüfung ist bislang uneinheitlich. Mehrere Beobachter weisen darauf hin, dass OpenAI keine unabhängigen Lean-Läufe aller Beweise vorlegt, sodass die zentrale Prüfung teilweise bei den Lesern selbst liegt. Berichte über eine angebliche Lösung des Navier-Stokes-Problems aus den Millennium-Preisen, ebenfalls mit Lean-Beweis, verstärken den Eindruck eines großen Schritts, lassen aber offen, ob die Formalisierung vollständig extern geprüft wurde.
Das ist kein Grund, die Ergebnisse pauschal abzutun. Ein Lean-Beweis enthält einen maschinell prüfbaren Kern, der unabhängig von der Reputation des Prüfers funktioniert. Solange dieser Kern korrekt ist, steht die Gültigkeit fest. Die offene Frage betrifft weniger die starken Ergebnisse als die schwächeren, die ohne Formalisierung auskommen.
Warum das Fach aufgeschreckt reagiert
OpenAI schreibt, das Modell löse reale Probleme aus der Mathematik und der theoretischen Informatik. Solche Fortschritte treffen auf ein Fach, das sich in den vergangenen zwei Jahren an einem raschen Tempo von KI-Ergebnissen bereits abarbeitet. Die Scientific American berichtet von einem Fach, das angesichts weiterer Hunderte Ergebnisse ohnehin unter Druck steht. Ein einzelnes Modell, das in der Größenordnung von 372 Forschungsfamilien liefert und dabei selbst anonym bleibt, sorgt für zusätzliche Fragen.
Für die mathematische Gemeinschaft steht vor allem die Frage im Raum, wie sich diese Flut von Ergebnissen in vertretbarer Zeit überhaupt prüfen und sauber einordnen lässt, wenn ein Teil der Beweise nur mit Lean und ein Teil nur von Menschen nachvollziehbar ist. OpenAI kündigt an, Workshops, Konferenzen und Programme zur Erschließung großer KI-Ergebnisse zu finanzieren. Das Repository lässt sich auf GitHub einsehen; weitere Lean-Formalisierungen sollen dort nachgereicht werden.
