OpenAI hat am 6. Oktober die mathematischen Ergebnisse eines unveröffentlichten internen Modells in ein öffentliches GitHub-Repository gelegt. Der Umfang steht in der README: 722 Manuskripte, sortiert in 372 Familien, wobei eine Familie ein Hauptresultat mit Begleitargumenten, Folgerungen und alternativen Beweisen zusammenfasst.
Der Anlass für die Veröffentlichung ist nicht nur der Inhalt. OpenAI schreibt, man habe die existierenden Mathematik-Benchmarks ausgereizt und sei deshalb auf offene Forschungsprobleme umgestiegen.
Wie die Ergebnisse entstanden sind
Dem Modell wurden rund 4.000 Probleme vorgelegt. Im Schnitt kostete ein Ergebnis Rechenzeit im Umfang von drei Stunden ChatGPT-Pro-Denken. Aus der Ausgabe wurden dann Familien und Manuskripte gebildet, bei denen die Bedeutung als ausreichend galt.
Zwei Fälle liefen anders: ein nullstellenfreier Bereich für die Riemannsche Zetafunktion und ein Beweis der Hodge-Vermutung für CM-abelsche Varietäten. Die Darstellung des Bereichs Re(s) > 11/12 hat zudem ein Mensch für die Lesbarkeit überarbeitet.
Zu zehn Resultaten gibt OpenAI gekürzte Zusammenfassungen der Modell-Gedankengänge heraus, darunter zum Irrationalitätsexponenten von π, zu den Mahler-Vermutungen, zu Kaplanskys Vermutung zur direkten Endlichkeit in Charakteristik zwei und zur Mézard-Parisi-Formel für verdünnte Spingläser.
Der Vorbehalt steht in der README, nicht in der Ankündigung
Viele Beweise liegen als Lean-Formalisierung bei, nachprüfbar per Computer, und OpenAI will weitere nachliefern. Aber nicht alle. In der README steht der Satz, auf den es ankommt: Die Sammlung enthält Ergebnisse in unterschiedlichen Prüfstadien, und einige der nicht formalisierten könnten Fehler haben.
Das ist die ehrliche Variante. Sie bedeutet aber auch, dass die Zahl 722 nicht 722 geprüfte Sätze beschreibt.
Beraten hat eine Gruppe von außen
Für die Form der Veröffentlichung hat OpenAI die unabhängige Advisory Group on Mathematics and Artificial Intelligence am Institute for Advanced Study hinzugezogen und sich an deren öffentliche Empfehlungen gehalten. Daraus kommen die Protokolle für Überarbeitungen und Zitate im Repository, und die Absicht, weiter nach einer von der Fachgemeinschaft getragenen Ablage zu suchen.
Dazu kündigt OpenAI Workshops, Konferenzen und Programme an, in denen es darum gehen soll, von KI erzeugte Ergebnisse überhaupt zu verstehen. Und einen Satz, der mehr Gewicht hat als der Rest: Man arbeite daran, das Modell, das diese Ergebnisse produziert hat, verantwortungsvoll zu veröffentlichen.
Der Prüfaufwand wandert zu den Lesern
Anthropic hat im September mit Claude den Satz von Fermat in Lean formalisiert — ein Beweis, einmal, vollständig maschinell nachprüfbar. OpenAI geht die andere Richtung: viel Material, teilweise formalisiert, mit dem ausdrücklichen Hinweis, dass Fehler drin sein können.
Beides ist legitim, und beides verschiebt dieselbe Arbeit. Wer 722 Manuskripte liest, von denen ein Teil nicht maschinengeprüft ist, muss selbst entscheiden, was er glaubt. Die Advisory Group und die Lean-Dateien sind genau dafür da, und ohne sie wäre die Veröffentlichung eine Behauptung in großer Zahl. Dass OpenAI den Vorbehalt in die README schreibt statt in die Ankündigung, ist der einzige Punkt, an dem ich mir mehr Mut gewünscht hätte.