Google DeepMind hat einen KI-Agenten, der neun offene Probleme rund um Paul Erdős gelöst hat. Zwei davon waren seit 56 Jahren ungelöst. Interessanter als die Schlagzeile ist jedoch das Kleingedruckte: Die Autoren berichten auch, was das System nicht konnte, und ein günstigerer, einfacherer Agent erwies sich als fast genauso leistungsfähig.
Die Zahlen
Das System heißt AlphaProof Nexus. Es wurde an 353 offenen Problemen getestet, die mit dem ungarischen Mathematiker Erdős verbunden sind, und knackte 9 davon, also rund 2,5 Prozent. Außerdem wurde es auf 492 offene Vermutungen aus der Online Encyclopedia of Integer Sequences (OEIS) angesetzt und bewies 44 davon, knapp 9 Prozent.
Auch die Rechnung gehört zur Geschichte. Jedes gelöste Erdős-Problem verursachte Rechenkosten von mehreren Hundert Dollar. Das ist nicht nichts, aber weniger als das Kaffeebudget eines Forschungsseminars für eine Woche – und erheblich weniger als 56 Jahre, in denen Mathematiker einen Beweis übersehen haben.
| Benchmark | Offene Probleme | Gelöst |
|---|---|---|
| Erdős-Probleme | 353 | 9 (zwei seit 56 Jahren offen) |
| OEIS-Vermutungen | 492 | 44 |
Warum Lean die Debatte verändert
Wer schon einmal einen Chatbot um einen Beweis gebeten hat, kennt das typische Fehlermuster. Die Antwort klingt wunderbar, liest sich flüssig und ist in Schritt vier falsch. Überzeugende Prosa ist das eine, was Sprachmodelle ohne jeden Aufwand produzieren.
AlphaProof Nexus umgeht dieses Problem, indem es in Lean arbeitet, einer Sprache und Umgebung zur Formalisierung mathematischer Beweise. Das Modell schreibt einen Beweis in formaler Form, und Lean überprüft jeden logischen Schritt. Schlägt etwas fehl, erhält der Agent die Fehlermeldung als Rückmeldung und sucht weiter. Eine schön formulierte Erklärung bringt keine Punkte. Nur ein Beweis, der der maschinellen Überprüfung standhält, zählt.
Darin liegt der eigentliche Beitrag dieser Arbeit. Die Autoren der Studie wollten testen, ob eine LLM-gesteuerte formale Beweissuche offene Forschungsprobleme bewältigen kann und nicht nur Aufgaben aus Mathematikolympiaden. Für neun Erdős-Probleme und 44 OEIS-Vermutungen lautete die Antwort: ja.
Wie die Maschine aufgebaut ist
Nexus ist kein einzelnes Modell, das auf einen einzelnen Prompt antwortet. Mehrere KI-Agenten arbeiten parallel, probieren Ansätze aus, überprüfen sie und verfeinern Beweise. In der aufwendigsten Variante koordiniert ein evolutionärer Algorithmus das gesamte Vorgehen. In bestimmten Phasen der Suche kommt AlphaProof zum Einsatz, der auf Reinforcement Learning basierende automatische Theorembeweiser von DeepMind.
Das klingt nach einem beträchtlichen technischen Aufwand. Also taten die Autoren das Vernünftige und fragten, ob er überhaupt nötig war.
Das unbequeme Kontrollexperiment
Sie verglichen die vollständige Architektur mit einem deutlich schlichteren Agenten, bei dem einfach abwechselnd ein Sprachmodell Beweise erzeugt und Lean sie überprüft. Als sie die neun gelösten Erdős-Probleme erneut durchgingen, löste der einfache Agent ebenfalls alle neun.
Bei den Fähigkeiten hatte das aufwendige System hier also nicht die Nase vorn. Sein Vorteil zeigte sich bei den schwierigsten Problemen, bei denen der Betrieb des einfachen Agenten teurer war. Die ausgefeilte Orchestrierung brachte also Effizienz, aber keine zusätzlichen Fähigkeiten – zumindest bei dieser Auswahl.
Die Autoren ziehen daraus eine bescheidene, aber nützliche Schlussfolgerung. Die Ergebnisse hängen nicht nur davon ab, wie leistungsfähig das zugrunde liegende Sprachmodell ist, sondern auch davon, wie die Beweissuche organisiert ist. Anders gesagt: Ein klug gestalteter Prozess rund um das Modell macht einen Unterschied. Und das durch ein Experiment herauszufinden ist günstiger als durch eine Pressemitteilung.
Über Erdős und OEIS hinaus
Das System wurde auch außerhalb dieser beiden Benchmarks eingesetzt. Der Bericht nennt folgende weitere Einsätze:
- Unterstützung bei der Lösung eines offenen Problems in der algebraischen Geometrie.
- Verbesserung einer Schranke in der konvexen Optimierung.
- Aufdeckung von Fehlern bei der Formalisierung mathematischer Aussagen aus der veröffentlichten Fachliteratur.
- Laufender Einsatz in der Forschung zur Graphentheorie und Quantenoptik.
Der dritte Punkt verdient einen genaueren Blick. Formalisierung bedeutet, eine von Menschen formulierte Aussage nach Lean zu übersetzen. Dabei passieren leicht Fehler, die ebenso leicht übersehen werden. Ein Werkzeug, das sie aufspürt, ist auch an Tagen nützlich, an denen es nichts Neues beweist.
Was es nicht kann
Die Autoren benennen die Grenzen direkt. Das ist erfrischend in einem Feld, in dem Grenzen meist in die Fußnoten verbannt werden.
- Die meisten Probleme bleiben offen. Von den 353 Erdős-Problemen wurden 344 nicht gelöst.
- Die Erfolge konzentrieren sich auf bestimmte Bereiche. Sie liegen in Gebieten, für die bereits eine gut ausgebaute Bibliothek formalisierter Ergebnisse existiert und in denen sich schwierige Beweisführungen in einzelne Teilprobleme zerlegen lassen.
- Die Ergebnisse schwanken. Wie bei den zugrunde liegenden Sprachmodellen können die Ergebnisse des Systems von Versuch zu Versuch stark variieren.
- Umfangreiche neue Theorie liegt außer Reichweite. Probleme, die den Aufbau eines umfangreichen neuen Theoriegebäudes erfordern, übersteigen vorerst seine Möglichkeiten.
Den zweiten Punkt sollte man sich merken. Lean kann nur prüfen, was sich darin ausdrücken lässt, und nur dort bei der Beweissuche helfen, wo bereits genügend formale Grundlagen vorhanden sind. Das System ist dort am stärksten, wo Mathematiker bereits die mühsame Arbeit erledigt haben, Dinge in maschinenlesbarer Form aufzuschreiben. Ehre also, wem Ehre gebührt: den Menschen, die die Bibliotheken formalisiert haben.
Welche Schlüsse die Autoren daraus ziehen
Nach Ansicht der Autoren könnten formale Beweise ein Weg sein, KI in die tatsächliche mathematische Arbeit einzubinden, statt sie als eine Maschine zu behandeln, die Antworten liefert, denen man entweder vertraut oder misstraut. Die Überprüfung macht das möglich. Ein Mathematiker muss nicht dem Modell vertrauen, sondern nur Lean.
Das ist ein reiferer Umgang mit KI-Ausgaben als der übliche, bei dem die Leser die Antwort bewundern und auf das Beste hoffen sollen.
Das Fazit
Neun gelöste Probleme von 353 werden niemanden zufriedenstellen, der bis Dienstag auf eine mathematische Revolution hofft. Aber zwei dieser neun hatten sich 56 Jahre lang menschlichen Lösungsversuchen widersetzt, jeder Beweis wurde maschinell überprüft, und die Kosten lagen bei einigen Hundert Dollar. Die Erkenntnis, dass eine einfache Schleife aus Erzeugen und Überprüfen bei den gelösten Problemen mit dem aufwendigen System mithalten konnte, könnte sich am Ende als das nützlichste Ergebnis von allen erweisen. In der Mathematik ist es wie so oft: Eine teuer aussehende Architektur ist manchmal nur der teurere Weg zur gleichen Antwort.