OpenAI-Mathebeweise: 372 KI-Ergebnisse landen auf GitHub

OpenAI hat 372 neue mathematische Ergebnisse veröffentlicht, die eines seiner internen Frontier-Modelle hervorgebracht hat. An Fachzeitschriften hat das Unternehmen sie nicht geschickt. Stattdessen hat es sie alle in einem öffentlichen GitHub-Repository bereitgestellt, samt Änderungsprotokollen und Quellenangaben. Nach Angaben des Unternehmens löst jedes Ergebnis entweder ein offenes Problem oder bringt dessen Lösung ein gutes Stück voran.

Die Sammlung ist breit gefächert. Einige Ergebnisse verbessern wichtige Computeralgorithmen. Andere betreffen die Riemannsche Vermutung, eines der bekanntesten ungelösten Probleme der Mathematik. Laut OpenAI hat dasselbe Modell bereits eine Lösung für ein Navier-Stokes-Problem geliefert, die seit Wochen formal geprüft wird.

Ein Prompt, ein Agent, drei Stunden

Am auffälligsten ist die Art, wie die Ergebnisse entstanden sind. OpenAI zufolge stammt fast jedes Ergebnis aus einem einzigen Prompt an einen einzigen KI-Agenten, auch wenn manche mehr als einen Anlauf brauchten. Im Schnitt kostete jedes Ergebnis rund drei Stunden Rechenzeit mit ChatGPT Pro Thinking.

Bei der Navier-Stokes-Arbeit sah das ganz anders aus. Dafür war ein Schwarm aus 10.000 Agenten nötig, dazu Rechenleistung im Wert von Millionen Dollar. Die neue Serie legt nahe, dass die Kosten pro Ergebnis stark gesunken sind, zumindest bei den Problemen, an die sich OpenAI gewagt hat.

OpenAI hat außerdem Notizen zu seiner Vorgehensweise veröffentlicht:

• Zusammenfassungen des Denkprozesses des Modells
• Statistiken dazu, an wie vielen Problemen sich das Modell versucht hat
• Schätzungen der Rechenkosten

Lean als Abkürzung bei der Prüfung

Viele der Beweise liegen auch als Formalisierung in Lean vor, einer Programmiersprache für mathematische Beweise, die sich maschinell überprüfen lassen. Weitere Formalisierungen sollen laut OpenAI folgen.

Der Grund ist ganz praktisch. Hunderte KI-generierte Beweise könnten Mathematikerinnen und Mathematiker, die sie von Hand prüfen müssten, schnell überfordern. Andere Bereiche kennen ähnliche Probleme. Google zum Beispiel hat ein Open-Source-Bug-Bounty-Programm ausgesetzt, nachdem es mit KI-generierten Meldungen überschwemmt worden war. Mit maschinell prüfbaren Beweisen will OpenAI einen solchen Engpass in der Mathematik vermeiden.

Vorbei an den Fachzeitschriften

Dass OpenAI GitHub statt begutachteter Fachzeitschriften gewählt hat, ist ein Signal. Es deutet an, dass das klassische wissenschaftliche Publizieren für so viele möglicherweise neue Ergebnisse zu langsam ist.

OpenAI hat sich mit der Advisory Group on Mathematics and Artificial Intelligence am Institute for Advanced Study (IAS) beraten, dem Forschungszentrum in Princeton. Zu den Mitgliedern gehört Fields-Medaillenträger Timothy Gowers. An die öffentlichen Empfehlungen der Gruppe hat sich OpenAI nur lose gehalten. Keiner seiner Prompts wurde veröffentlicht, und bei den Rechenkosten nannte das Unternehmen nur Durchschnittswerte statt Zahlen für jedes einzelne Problem.

Außerdem hatte das Unternehmen schon vor Beginn der Beratung eine Grenze gezogen. Die Mathematiker durften mitreden, wie die Ergebnisse kommuniziert werden, aber nicht, ob sie überhaupt erzeugt werden oder wie schnell.

OpenAI kündigt an, Workshops und Konferenzen zu finanzieren, die sich mit dem Verständnis KI-erzeugter Ergebnisse befassen. Das Unternehmen räumt ein, dass Quellenangaben und Aufbereitung noch verbessert werden müssen. Zudem bereite es eine verantwortungsvolle Veröffentlichung des Modells vor, um "Wissenschaftlerinnen und Wissenschaftler direkt mit modernsten Fähigkeiten auszustatten".

Korrekt heißt nicht bedeutsam

Lean kann bestätigen, dass ein Beweis logisch korrekt ist. Ob ein Ergebnis originell ist oder mathematisch etwas bedeutet, kann es nicht beurteilen. OpenAI setzt darauf, dass seine Ergebnisse die Grenzen des menschlichen Wissens verschieben. Ob die Mathematik das genauso sieht, ist noch offen, und die ersten Reaktionen reichen von Begeisterung bis Frust.

Einige der prominentesten Köpfe des Fachs haben bereits Bedenken geäußert. In einem offenen Brief mit dem Titel "A Severe Misalignment of AI in Mathematics" beschrieben 25 Fields-Medaillenträger eine tiefe Kluft zwischen den Zielen der KI-Branche und denen der Mathematik. Aus ihrer Sicht ist das Lösen von Problemen nur ein Werkzeug und ein Stellvertreter. Das eigentliche Ziel seien begriffliches Verständnis und Einsicht. Massenhaft wahre Aussagen zu produzieren, könne fruchtbaren Boden zerstören, statt neue Ideen hervorzubringen, argumentierten sie, und der Schaden würde auf andere Fächer übergreifen.

Gowers hat gewarnt, dass die mathematische Literatur innerhalb von ein bis zwei Jahrzehnten enorm anwachsen könnte, ohne dass es noch eine menschliche Gemeinschaft gibt, die sie wirklich versteht. Terence Tao, ebenfalls Fields-Medaillenträger, hat gesagt, die Ausbildung junger Mathematikerinnen und Mathematiker solle die menschliche Seite der Disziplin betonen und den Einsatz von KI-Werkzeugen streng begrenzen, damit echtes Lernen und Verstehen erhalten bleiben.

Unsere Einschätzung

Bei dieser Veröffentlichung scheint es ebenso sehr um das Verfahren zu gehen wie um die Mathematik. Ein einzelner Agent, der drei Stunden pro Problem rechnet, verändert die Wirtschaftlichkeit der Beweisproduktion. Bleiben die Kosten so niedrig, wird der Ausstoß weiter schneller wachsen, als menschliche Gutachter hinterherkommen. Lean hilft bei einem Teil des Problems, nämlich der Korrektheit. Die schwierigeren Fragen sind, ob ein Ergebnis relevant ist und ob es originell ist, und die hängen weiterhin an Menschen, die schon jetzt am Limit arbeiten.

Auch die Spielregeln verdienen Aufmerksamkeit. OpenAI hat führende Mathematiker um Rat gebeten, sie aber nicht mitentscheiden lassen, ob und wie schnell die Arbeit entsteht. Prompts und Kosten pro Problem hat das Unternehmen zudem zurückgehalten. Damit bleibt der Forschungsgemeinschaft nur, auf die Veröffentlichung zu reagieren, statt sie mitzugestalten. Ähnliche Spannungen zeigen sich auch an anderen Stellen der Wissenschaft, wie unser Bericht über einen MIT-Bericht zum schwindenden Vertrauen der Lehrenden gezeigt hat.

Worauf es als Nächstes ankommt:

1. Ob unabhängige Mathematikerinnen und Mathematiker bestätigen, dass einige der 372 Ergebnisse tatsächlich neu und bedeutsam sind.
2. Wie die Prüfung der Navier-Stokes-Lösung ausgeht.
3. Ob die angekündigte Modellveröffentlichung von OpenAI Forschenden ein Werkzeug in die Hand gibt, das sie selbst steuern können, so wie es Harnesses wie BootLoops bei anderen Modellen anstreben.

Wenn die Veröffentlichung nur einen ungelesenen Stapel Beweise weiter wachsen lässt, könnte sich die Warnung der Fields-Medaillenträger als die treffendere Prognose erweisen.