Das mathematische Beweissystem AlphaProof Nexus von Google DeepMind ist offiziell in Science erschienen. Als Erstautor ist Tsoukalas genannt, das gesamte Forschungsteam stammt von DeepMind. Die Arbeit war Ende Mai bereits als Preprint öffentlich; jetzt liegt die begutachtete Fassung in der Fachzeitschrift vor.
Die Bilanz bleibt dieselbe: Das System hat sich an 353 ungelösten Erdős-Problemen versucht und 9 gelöst, darunter 2, die seit 56 Jahren offen waren. Von 492 offenen Vermutungen aus der Online-Enzyklopädie der Ganzzahlfolgen OEIS bewies es 44. Außerdem beantwortete es eine seit rund 15 Jahren offene Frage zur Hilbert-Funktion in der algebraischen Geometrie und verbesserte eine bekannte Schranke in der Min-Max-Optimierung.
Ein Gemini, ein Lean-Compiler
Die Grundlage des Systems ist Gemini 3.1 Pro. Das Modell entwirft Beweise in der formalen Sprache Lean; der Lean-Compiler prüft nach jeder Änderung, und die Fehlermeldungen fließen direkt in den nächsten Versuch zurück. Der Mensch sieht sich erst am Ende das Ergebnis an.
Das Paper unterscheidet vier Varianten:
- Variante A: die schlichteste Generieren-und-Prüfen-Schleife – das große Modell schreibt, der Compiler urteilt;
- Variante B: baut auf A auf und bindet AlphaProof ein, den früheren Beweiser von DeepMind, der gezielt fehlende Beweisabschnitte ergänzt;
- Variante C: fügt einen evolutionären Mechanismus hinzu, bei dem mehrere Sub-Agenten einen gemeinsamen Pool von Beweisentwürfen nutzen, der nach Elo-Wert sortiert wird;
- Variante D: alles zusammen, eingesetzt für die Erdős-Probleme.
Am aufschlussreichsten ist ein Detail des Ergebnisses: Auch Variante A bewies unabhängig alle 9 Erdős-Aufgaben, nur kosteten die schwierigsten davon mehr. Die von The Decoder angeführten Inferenzkosten liegen bei einigen hundert US-Dollar pro Aufgabe. Die Autoren schreiben dazu in der Arbeit:
"power of compiler feedback in grounding LLM reasoning"
(Die Rückmeldungen des Compilers verankern das Schlussfolgern großer Sprachmodelle in der Realität.)
Einige Vorbehalte spanischer Wissenschaftler
Das spanische Science Media Centre holte am Tag der Veröffentlichung mehrere Forschende aus dem Land um eine Einschätzung; die Meinungen fielen auseinander.
Pablo Haya Coll von der UAM sieht in dem Ansatz ein Verfahren, das systematisch gewichtige mathematische Entdeckungen hervorbringen kann. Josep Curto von der UOC urteilte, es sei "a dazzling display of technical capability marred by significant methodological inconsistencies" – sinngemäß eine technisch blendende Vorstellung mit deutlichen methodischen Widersprüchen. Er nannte drei Punkte: Dass A und D dieselben Aufgaben lösen, zeige, dass die Komplexität des Frameworks nicht zwingend die Entdeckungsfähigkeit bestimme; die Kosten werden nur für die erfolgreichen Läufe gerechnet, und bei B und D fehlt zudem der Inferenzaufwand von AlphaProof selbst; und Lean garantiere nur, dass der Beweis für die „aufgeschriebene Aussage“ gilt – ob diese Aussage die ursprüngliche Aufgabe getreu abbildet, müssten weiterhin Mathematiker von Hand prüfen, und das Paper räumt ein, dass es Formalisierungsfehler gab.
Javier Aramayona, Leiter des ICMAT, sorgt sich um etwas anderes: Es entstehe eine Fülle an Ergebnissen, die „bekanntermaßen wahr, aber von niemandem vollständig verstanden“ seien; das Verstehen als Kern mathematischer Forschung und die Ausbildung junger Forschender könnten darunter leiden. Teodoro Calonge von der Universität Valladolid sagt es noch direkter: Das Feld habe noch beträchtlichen Verbesserungsspielraum.
Auch die Autoren selbst benennen die Grenzen: Die Gesamterfolgsquote von KI bei Erdős-Problemen liege bei etwa 1 bis 2 Prozent, gelöst würden überwiegend vergleichsweise leichte Aufgaben, und zwar in Kombinatorik, konvexer Optimierung und Zahlentheorie – Gebiete, in denen die Bibliothek Mathlib besonders dicht ausgebaut ist und sich Probleme gut in Teilziele zerlegen lassen. An Problemen, die viel neue Theorie erfordern, komme das System kaum heran.
Die Ereignisse dieses Jahres im Zusammenhang
Im Mai berichteten wir, dass ein OpenAI-Modell eine 80 Jahre alte Erdős-Vermutung geknackt habe; im September entbrannte zwischen Mathematikern und OpenAI ein Streit um die Autorenschaft; am 6. Oktober stellte OpenAI auf GitHub auf einen Schlag 722 KI-generierte mathematische Manuskripte bereit – als Open-Source-Repository unter Apache-2.0-Lizenz, ohne den Weg über eine Fachzeitschrift. The Decoder berichtet, eine von Terence Tao angeführte Gruppe von Mathematikern habe anschließend zum Boykott dieser Praxis aufgerufen.
Der Unterschied zwischen den Ansätzen der beiden Unternehmen wird hier deutlich. OpenAI setzt auf Masse und Offenheit und überlässt der Community die Sichtung; DeepMind setzt auf deutlich weniger Ergebnisse, die aber alle den Lean-Compiler und zusätzlich die Zeitschriftenbegutachtung durchlaufen haben. Auch die Rolle von Lean legt DeepMind in der Arbeit zurückhaltend an; wörtlich heißt es, formale Verifikation "can serve as a filter for determining which proofs merit human review" – sie dient also dazu zu entscheiden, welche Beweise es wert sind, dass Menschen sie lesen.
Eine grobe Überschlagsrechnung: Bei einigen hundert Dollar pro Aufgabe liegen die Inferenzkosten für die 9 Erdős-Probleme weit unter dem Monatsgehalt eines Postdocs. Wie viel höher die Rechnung nach Curtos Maßstab ausfällt, wenn gescheiterte Läufe und AlphaProof-Aufrufe hinzukommen, beziffert das Paper bislang nicht. DeepMind hat die Beweise und einen Teil der Erläuterungen im GitHub-Repository alphaproof-nexus-results abgelegt, sodass externe Mathematiker sie Stück für Stück nachprüfen können.
Quellen: Fachartikel in Science, The Decoder, CocoLoop, Expertenstimmen des spanischen Science Media Centre; anhand des Papers geprüft wurden die 9 gelösten von 353 Erdős-Problemen, die 44 bewiesenen von 492 OEIS-Vermutungen sowie die Aufgabenverteilung der vier Agentenvarianten.