722 KI-Manuskripte: OpenAI legt seine Mathe-Ergebnisse offen

Zwei Wochen lang hatte OpenAI behauptet, ein internes Modell habe mehr als 100 offene Probleme der Mathematik gelöst, ohne die zugehörigen Beweise zu zeigen. Am 6. Oktober hat das Unternehmen nachgeliefert: 722 Manuskripte, gesammelt in einem öffentlichen GitHub-Archiv, ein Teil davon mit maschinell überprüften Beweisen. Damit kann die Fachwelt erstmals selbst nachsehen, was an den Ankündigungen dran ist. Zugleich zeigt die Veröffentlichung, wie schlecht die Mathematik auf Forschung in diesem Tempo vorbereitet ist.

Das Wichtigste in Kürze

• Das Archiv enthält 722 Manuskripte in 372 thematischen Familien aus reiner Mathematik, theoretischer Informatik und mathematischer Physik.
• OpenAI stellte dem unveröffentlichten Modell rund 4.000 Aufgaben. Jedes Ergebnis kostete im Schnitt etwa drei Stunden Rechenzeit im Denkmodus von ChatGPT Pro.
• Für 162 Manuskripte liegt laut Katalog eine Formalisierung des Hauptergebnisses in der Beweissprache Lean vor, die ein Computer prüfen kann. Für den Rest gilt das nicht; OpenAI räumt ein, dass einzelne Ergebnisse Fehler enthalten könnten.
• Ein unabhängiger Beirat von Mathematikern hatte Regeln für die Veröffentlichung empfohlen. OpenAI hat sie nur teilweise umgesetzt.

Was in dem Archiv steckt

Das Archiv ist nüchtern aufgebaut. Ein Übersichtsdokument beschreibt die 372 Familien, also Gruppen zusammengehöriger Arbeiten mit einem Hauptergebnis, Folgerungen oder alternativen Beweisen. Jede Arbeit liegt als PDF samt Quelltext und Zitierhinweis vor. Für zehn Ergebnisse veröffentlicht OpenAI zudem gekürzte Zusammenfassungen der Gedankengänge des Modells. Die Titel dieser Familien zeigen, wie hoch das Unternehmen greift: Sie reichen vom Irrationalitätsexponenten der Kreiszahl Pi über die Vermutungen des Mathematikers Kurt Mahler bis zum Isomorphieproblem freier Gruppenfaktoren, einer seit Jahrzehnten offenen Frage der Operatoralgebren. Darunter ist auch ein Gegenbeispiel zu einer Vermutung des Algebraikers Irving Kaplansky, dessen Kern in Lean formalisiert ist.

Wie die Ergebnisse entstanden, beschreibt OpenAI knapp. Die große Mehrheit stamme aus einem festen Verfahren mit demselben internen Modell. Nachdem das Modell die bisherigen Mathematiktests ausgereizt hatte, habe man die Bewertung auf offene Forschungsprobleme ausgeweitet. Aus den rund 4.000 gestellten Aufgaben blieb nach Zusammenfassung und einer Mindestschwelle für Bedeutsamkeit knapp ein Zehntel übrig. Zwei prominente Ausnahmen nennt das Unternehmen selbst: eine Arbeit über eine nullstellenfreie Region der Riemannschen Zetafunktion, deren Text für die Lesbarkeit von Menschen überarbeitet wurde, und eine Arbeit zur Hodge-Vermutung für eine spezielle Klasse geometrischer Objekte. Beide entstanden nicht nach dem Standardverfahren.

Lean macht den Unterschied, aber nur zum Teil

Der eigentliche Fortschritt gegenüber den bisherigen Ankündigungen sind die Lean-Beweise. Lean ist eine Programmiersprache, in der sich mathematische Beweise so aufschreiben lassen, dass ein Computer jeden einzelnen Schritt nachprüft. Ist ein Ergebnis dort sauber formalisiert, muss niemand dem Modell glauben. Fachleute müssen dann nur noch prüfen, ob die formale Aussage wirklich dem entspricht, was behauptet wird. Für 162 Manuskripte liefert das Archiv eine solche Formalisierung, weitere will OpenAI nachreichen.

Für die übrigen rund 560 Manuskripte gilt das nicht. Dort bleibt nur klassische Begutachtung durch Menschen, und die ist langsam. Ein einzelner anspruchsvoller Beweis kann Fachleute Wochen beschäftigen. OpenAI schreibt selbst, einige der nicht formalisierten Ergebnisse könnten Probleme haben, und kündigt an, Korrekturen als neue Versionen festzuhalten, ohne alte zu löschen. Auch Zitate und Darstellung seien noch verbesserungsbedürftig. Hinzu kommt: Das Modell, das die Arbeiten erzeugt hat, ist nicht öffentlich. Unabhängige Forscher können die Ergebnisse prüfen, aber nicht reproduzieren, wie sie entstanden sind.

Ein Beirat mit Empfehlungen, aber ohne Macht

Wie wir nach der Ankündigung der über 100 gelösten Probleme berichtet haben, hatte OpenAI einen Beirat am Institute for Advanced Study in Princeton gebildet, die Advisory Group on Mathematics and Artificial Intelligence. Die neun Mitglieder arbeiten unbezahlt und haben keine Entscheidungsbefugnis. Am 29. September veröffentlichte die Gruppe Leitlinien, gestützt auf mehr als 600 Rückmeldungen aus der Fachwelt. Laut Berichten über die Leitlinien gehören dazu die Hinterlegung in einem akademischen Archiv, das kein KI-Labor kontrolliert, und für jedes Ergebnis die Offenlegung von Modellname, Prompts, Gedankengang, Zeitaufwand und Rechenkosten.

OpenAI hat davon einiges umgesetzt und anderes nicht. Das Archiv liegt auf dem eigenen GitHub-Konto des Unternehmens; man prüfe aber gemeinschaftlich betriebene Alternativen. Prompts zu einzelnen Aufgaben fehlen, Gedankengänge gibt es nur für zehn Ergebnisse. Der Beirat formulierte in seiner Stellungnahme vom 6. Oktober diplomatisch: Die Veröffentlichung sei der Anfang, nicht der Abschluss des menschlichen Verstehens. Ob die Empfehlungen ausreichend befolgt wurden, müsse am Ende die mathematische Gemeinschaft beurteilen.

Der Ärger in Teilen der Fachwelt reicht weiter zurück. Schon beim angeblichen Navier-Stokes-Beweis im September ging es um Zuschreibung und Umgang mit menschlichen Beiträgen. Jetzt kommen Sorgen um Kapazitäten hinzu: Wer soll mehr als 700 Arbeiten begutachten, wenn die nächste Lieferung womöglich schon in Arbeit ist? Und wem gehört die Verantwortung für einen Fehler, wenn als Autor nur ein Unternehmen auftaucht?

Was das für die Mathematik bedeutet

Für Forschende ist das Archiv zunächst ein Werkzeugkasten. Wer an einem der Themen arbeitet, kann die Manuskripte als Vorlage, als Gegenentwurf oder als Ausgangspunkt nutzen, und die formalisierten Ergebnisse lassen sich in eigene Lean-Projekte übernehmen. Die Lizenz der Formalisierungen ist Apache 2.0, also offen. Gerade in Teilgebieten mit wenigen Spezialisten kann das die Arbeit beschleunigen.

Die größere Verschiebung betrifft aber die Rolle des Menschen. Bislang galt ein Satz als bewiesen, wenn Fachleute den Beweis verstanden und akzeptiert hatten. Mit Hunderten maschinell erzeugter Arbeiten auf einmal kippt das Verhältnis: Das Verstehen hinkt der Produktion hinterher. Formale Prüfung durch Lean löst einen Teil dieses Problems, denn ein geprüfter Beweis ist korrekt, auch wenn ihn noch niemand nachvollzogen hat. Mathematik lebt aber nicht nur von korrekten Sätzen, sondern von Ideen, die man weiterverwenden kann. Ob die 722 Manuskripte solche Ideen enthalten, lässt sich nur auf dem langsamen Weg herausfinden. OpenAI hat angekündigt, Workshops und Konferenzen zu den wichtigsten Ergebnissen zu fördern. Wie ernst das gemeint ist, wird sich daran messen lassen, wie viel Zeit und Geld das Unternehmen in genau diesen langsamen Teil steckt.