Ein KI-Beweis wartet darauf, dass Menschen ihn verstehen

Ein Beweis in Verwahrung

Ein Beweis von 1.147 Seiten, geschrieben von einer künstlichen Intelligenz, wartet darauf, dass Menschen ihn verstehen. Am 16. Oktober bittet OpenAI David Gross, Physik-Nobelpreisträger von 2004, die Verwahrung zu übernehmen und zu entscheiden, wie der Beweis am besten an die Fachwelt übergeben wird. Gross wählt vier Kollegen aus, die ihm helfen.

Zehn Tage später, am 26. Oktober, verkündet OpenAI das Ergebnis. Tags darauf veröffentlichen die fünf Physiker ein zweiseitiges Papier, das auf den Servern des Instituts von Gross in Santa Barbara liegt. Ein Satz fasst ihre Haltung zusammen: Bevor sie den Beweis freigeben, wollen sie überzeugt sein, dass er stimmt.

Sonst läuft diese Geschichte andersherum: Das Unternehmen verkündet zu früh, die Forscher verlangen Belege. Diesmal liegt der Text in den Händen der Forscher. Sie sind es, die den Tresor zuhalten.

Was OpenAI bewiesen haben will

Die Ankündigung reicht weiter, als es in der Berichterstattung ankam. OpenAI will einen mathematisch rigorosen Existenzbeweis für bestimmte wechselwirkende Quantenfeldtheorien in vier Dimensionen erbracht haben. Darunter die Quantenchromodynamik (QCD), die Theorie der starken Kernkraft, die Quarks in Protonen zusammenhält, sowie die einfachste der Grand Unified Theories, die die Teilchen des Standardmodells enthalten.

Zur Einordnung: Die Physik arbeitet seit fünfzig Jahren mit diesen Theorien, mit spektakulärem Erfolg, ohne dass jemand je bewiesen hätte, dass sie im mathematischen Sinn existieren. Das ist, als würde man jahrzehntelang in einem Haus wohnen, dessen Fundament nie jemand gesehen hat.

Nebenbei will OpenAI auch die Existenz der „reinen“ Yang-Mills-Theorie ohne Quarks bewiesen haben. Dieses Stück machte die Schlagzeilen, weil es eines der sieben Millennium-Probleme des Clay-Instituts berührt, die mit je einer Million Dollar dotiert sind. OpenAI selbst nennt es „einen Teil“ des Problems.

Die offizielle Problemstellung von Arthur Jaffe und Edward Witten verlangt zweierlei zugleich, und zwar für jede Symmetriegruppe eines bestimmten Typs: Die Theorie muss existieren, und sie muss eine „Massenlücke“ aufweisen, ihre Teilchen dürfen also keine beliebig nahe bei null liegende Masse haben. Auf die Massenlücke erhebt OpenAI keinen Anspruch. Und für welche Gruppen der Beweis der reinen Yang-Mills-Theorie gelten soll, sagt die Ankündigung nicht. Die fünf Physiker zählen die Massenlücke zu den weiterhin offenen Herausforderungen. Das Preisgeld steht nicht zur Debatte.

Lean prüft den Beweis, nicht die Frage

Ein Argument scheint die Vorsicht überflüssig zu machen. OpenAI sagt, man habe mit der Veröffentlichung gewartet, bis der Beweis in Lean formalisiert war, einer Sprache, in der ein Computer jeden Schritt eines Beweises kontrolliert. Fertig gewesen sei das am 16. Oktober, am selben Tag, an dem man Gross ansprach; von außen konnte es noch niemand kontrollieren. Wenn eine Maschine schon alles geprüft hat, warum warten?

Die Antwort steht im Text der fünf. Ihre erste Aufgabe ist es nicht, den Beweis Zeile für Zeile nachzulesen. Sie wollen prüfen, ob die in Lean übersetzten Definitionen und die Problemstellung mit den in Physik und Mathematik üblichen übereinstimmen und ob die formale Fassung zur ausgeschriebenen passt.

Lean garantiert, dass bewiesen wurde, was man ihm aufgetragen hat. Über die Frage selbst sagt es nichts. Eine perfekte Rechtschreibprüfung merkt nicht, dass der Brief an die falsche Person adressiert ist. Wir haben es hier schon zu Navier-Stokes festgehalten: Lean prüft nur die Aussage, die man ihm vorlegt.

Wo schon die saubere Definition einer Quantenfeldtheorie in vier Dimensionen ein offenes Problem ist, ist die Übersetzung der Aussage keine Formsache. Nach diesem Abgleich wollen die fünf zuerst den Lean-Beweis veröffentlichen und, sobald sie zufrieden sind, die 1.147 Seiten samt ihrer Einschätzung.

Verwahrer, die OpenAI nichts schulden

Wer sind die fünf? David Gross, Nobelpreisträger für die asymptotische Freiheit, eine Schlüsseleigenschaft dieser Theorien. Arthur Jaffe, Mitautor der Problemstellung. Michael Douglas, der in diesem Jahr eine Bestandsaufnahme des Problems vorgelegt hat; Igor Klebanov, Spezialist für das Confinement der Quarks; Nikita Nekrasov, Dannie-Heineman-Preisträger für mathematische Physik 2023.

Man könnte meinen, OpenAI habe sich seine Gutachter selbst ausgesucht. Das stimmt nur für einen der fünf. Wie es in ihrem Text heißt (aus dem englischen Original übersetzt), bat OpenAI Gross, die Verwahrung zu übernehmen, und Gross wählte den Rest des Komitees. Die fünf schreiben, sie handelten im Namen der akademischen Gemeinschaft und hätten „keinerlei Verantwortung gegenüber OpenAI“. Bestätigen tun sie nichts: Der Beweis „scheint“ ihnen ein wichtiger Schritt zu sein.

OpenAI hat dabei mitgespielt. Die drei Ergebnisse des Tages folgen drei Strategien, jeweils beraten von den jeweiligen Verwahrern: Das mathematische Resultat erscheint unverändert, das informatische wird einer Gruppe anvertraut, aber sofort online gestellt, das physikalische bleibt der Entscheidung der Gruppe überlassen. Stand 29. Oktober enthält das öffentliche Repository von OpenAI keine einzige Datei zu Yang-Mills.

Die Mathematiker wollen alles, und zwar sofort

Der öffentliche Streit geht nicht von OpenAI aus, sondern von den Mathematikern. Am 26. Oktober, dem Tag, an dem OpenAI bekannt gab, dass die Physikergruppe die Unterlagen zurückhält, verlangt die Advisory Group on Mathematics and Artificial Intelligence, ein unabhängiges Beratungsgremium am Institute for Advanced Study in Princeton, von OpenAI die unverzügliche Veröffentlichung des ausformulierten Beweises und seiner Lean-Fassung. Zu den neun Mitgliedern zählen Edward Witten, Timothy Gowers und Martin Hairer. Der Text ist ein gemeinsamer.

Das Argument lässt sich in zwei Sätzen sagen: Verständnis müsse sich offen entwickeln, mit gleichem Zugang für alle, und da die Formalisierung nach OpenAIs eigener Darstellung abgeschlossen sei, gebe es keinen wissenschaftlichen Grund mehr zu warten. Dem Gremium zufolge hat es „großen Respekt“ vor den angefragten Wissenschaftlern.

Am Vortag hatte es grundsätzlicher kritisiert, dass ein Labor Gelehrte bestimmt, die ein Ergebnis vor allen anderen zu sehen bekommen: ein Vorsprung für wenige, eine Auswahl, die die Netzwerke des Unternehmens widerspiegelt, und Namen, die am Ende als Gütesiegel dienen. Schon bei der Veröffentlichung der 722 Manuskripte von OpenAI hatte sich dieselbe Gruppe geweigert, als Gütesiegel zu dienen. Sie betont allerdings, ihre Empfehlungen zielten auf die Mathematik, nicht zwingend auf andere Wissenschaften.

So stehen die beiden Autoren der Problemstellung auf verschiedenen Seiten: Jaffe im Komitee, das den Beweis verwahrt, Witten in der Gruppe, die seine Veröffentlichung verlangt.

Die Prüfung als neuer Flaschenhals

Dass der Beweis falsch sei, behauptet in diesem Streit niemand. Es geht darum, wer ihn als Erster sieht und wie lange Menschen brauchen, um zu wissen, was er tatsächlich zeigt. Die Maschine hat ihren Yang-Mills-Beweis laut OpenAI am 9. September vorgelegt. Um Methode und Bedeutung zu verdauen, warnen die fünf, werde es Zeit brauchen.

OpenAI räumt selbst ein, was die Methode kostet: Die Wahl der ersten Verwahrer bestimme mit, wer sich zuerst beteilige, und schaffe ein Informationsgefälle. Die fünf Physiker nennen ihr Vorgehen ein Experiment darüber, wie die akademische Gemeinschaft mit dem rasch wachsenden, von KI erzeugten Wissen umgehen kann. Und sie kündigen an, sehr behutsam vorzugehen.