AlphaProof Nexus kombiniert LLM-gestützte Beweisführung mit maschineller Verifikation und knackt damit jahrzehntealte mathematische Forschungsprobleme.
Google Deepminds neues Framework AlphaProof Nexus hat autonom neun von 353 angegangenen offenen Erdős-Problemen gelöst, darunter zwei Fragen, die seit 56 Jahren unbeantwortet waren.
Zusätzlich bewies das System 44 von 492 offenen Vermutungen aus der Online Encyclopedia of Integer Sequences (OEIS), klärte eine 15 Jahre alte Frage zu Hilbert-Funktionen in der algebraischen Geometrie und verbesserte eine offene Schranke in der konvexen Optimierung. Die Inferenzkosten lagen laut dem Forschungspapier bei wenigen hundert Dollar pro Problem.
Anders als bei (womöglich) rein natürlichsprachlichen Ansätzen wie der kürzlich vorgestellten OpenAI-Lösung muss das zugrundeliegende Sprachmodell, in diesem Fall Gemini 3.1 Pro, die gesamte logische Kette nicht allein tragen.
Stattdessen generiert es Beweisschritte in der formalen Sprache Lean, deren Compiler jeden einzelnen Schritt maschinell verifiziert. Fehlermeldungen fließen direkt in den nächsten Versuch zurück. Das LLM wird so durch symbolisches Feedback geerdet, ein Sicherheitsnetz, das die bekannten Schwächen von Sprachmodellen beim logischen Schließen kompensiert. Erst ganz am Ende prüfen Menschen.
Vier Agenten, ein überraschendes Ergebnis
Das System besteht aus vier Agenten-Varianten mit steigender Komplexität. Der einfachste Agent (A) setzt unabhängige Subagenten ein, die auf Basis von Gemini 3.1 Pro in Schleifen arbeiten: Das Sprachmodell generiert Beweisschritte, der Lean-Compiler prüft sie, Fehlermeldungen fließen zurück in den nächsten Versuch.
Agent (B) erweitert diesen Ansatz um Abfragen an AlphaProof, Googles auf Reinforcement Learning basierendes System für Olympiade-Mathematik, das fehlende Beweisteile ausfüllen kann.
Agent (C) fügt eine evolutionäre Komponente hinzu: Inspiriert von AlphaEvolve teilen sich Subagenten eine gemeinsame Population von Beweisskizzen, die von Rating-Agenten auf Basis von Gemini 3.0 Flash nach Plausibilität und Neuheit bewertet und per Elo-System gerankt werden. Der vollausgestattete Agent (D) kombiniert alle Fähigkeiten.
Für die Erdős-Probleme kam Agent (D) zum Einsatz. Doch eine nachträgliche Analyse lieferte ein überraschendes Ergebnis: Der einfachste Agent (A), der nur aus LLM und Compiler-Feedback besteht, konnte alle neun gelösten Erdős-Probleme ebenfalls beweisen. Bei den schwierigsten Problemen war er allerdings teurer.
Die Forscher führen den Erfolg des simplen Agenten auf zwei Faktoren zurück: die rasante Verbesserung der zugrundeliegenden Sprachmodelle und die "Macht des Compiler-Feedbacks für die Erdung des LLM-Reasonings". Der vollausgestattete Agent behalte seinen Vorteil bei den härtesten Aufgaben vorerst, doch dieser Vorsprung könnte mit wachsenden LLM-Fähigkeiten schrumpfen.
Lösungsrate gegen Kosten für sechs der neun gelösten Erdős-Probleme: Bei einfacheren Aufgaben wie erdos_26 erreichen alle vier Agenten-Varianten hohe Erfolgsraten. Bei schwierigeren Problemen wie erdos_125 oder erdos_152 zeigen sich deutliche Unterschiede, wobei der vollausgestattete Agent (D) teils mit weniger Versuchen zum Ziel kommt, der einfache Agent (A) aber bei ausreichendem Budget ebenfalls erfolgreich ist. | Bild: Tsoukalas et al.Dieses Ergebnis deutet laut den Forschern auf einen breiteren Trend hin: einen "fortschreitenden Wandel von spezialisierten, trainierten Systemen hin zu einfachen agentischen Schleifen, während LLMs leistungsfähiger werden."
Nützlich auch ohne vollständigen Beweis
Die Erfolge des Systems konzentrieren sich laut den Forschern auf Gebiete wie Kombinatorik, konvexe Optimierung und Zahlentheorie, in denen Leans Mathematik-Bibliothek Mathlib ausgereift ist und Aufgaben sich in handhabbare Teilziele zerlegen lassen. Die meisten Erdős-Probleme blieben unerreichbar, "geschweige denn Probleme, die umfangreiche neue Theorie erfordern". Zudem erben die Agenten die Unzuverlässigkeit der zugrundeliegenden Sprachmodelle.
Dennoch sehen die Forscher einen Nutzen, der über gelöste Probleme hinausgeht. Mathematiker, die mit dem System zusammenarbeiteten, berichteten, dass selbst gescheiterte Beweisversuche ihr Verständnis eines Problems vertieften. Weil die Skizzen formal waren, konnten Experten sich auf die ungelösten Teilziele konzentrieren, statt das gesamte Argument neu zu überprüfen.
Außerdem erwiesen sich die Agenten als wirksame Werkzeuge, um Fehlformalisierungen in der Literatur aufzudecken. "Formale Verifikation kann als Filter dienen, um festzustellen, welche Beweise eine menschliche Überprüfung verdienen", schreiben die Autoren.
Das System wird laut dem Papier bereits in laufender Forschung zu Quantenoptik und Graphentheorie eingesetzt. Alle Lean-Beweise und ausgewählte natürlichsprachliche Beweise sind auf GitHub verfügbar.
So löst AlphaProof Nexus das Erdős-Problem #125: Der Agent erhält eine Lean-Datei, in der der eigentliche Beweis durch eine Lücke ersetzt ist (a), sieht im Prompt frühere Versuche mit Elo-Ratings und einen aktuellen Plan (b), zerlegt dann schrittweise den Beweis, ruft AlphaProof für Teilziele auf und verfeinert gescheiterte Schritte durch weitere Zerlegung in Lemmas, bis alle Ziele bewiesen sind (c). | Bild: Tsoukalas et al.Erdős-Probleme als Testfeld für KI-Mathematik
Vor kurzem hatte OpenAI mit einem hauseigenen Reasoning-Modell die Unit-Distance-Vermutung von Erdős widerlegt, was Fields-Medaillist Tim Gowers als "Meilenstein in der KI-Mathematik" bezeichnete. Schon zuvor half GPT-5.2 Pro bei der Lösung des Erdős-Problems #281, wobei Terence Tao den Fall als "vielleicht das eindeutigste Beispiel" für eine KI-Lösung eines offenen mathematischen Problems einordnete.
Diese Erfolge sind in gewisser Hinsicht beeindruckender als der Deepmind-Ansatz: Das Sprachmodell musste die gesamte logische Kette rein durch natürliche Sprache tragen, ohne symbolische Stützräder wie einen Lean-Compiler, der jeden Schritt verifiziert. AlphaProof Nexus ist dafür systematischer und skalierbarer, löst aber eine andere Aufgabe: den Aufbau eines robusten KI-Werkzeugs für die mathematische Forschungspraxis.
Tao warnte allerdings vor einer verzerrten Wahrnehmung: Die tatsächliche Erfolgsquote von KI bei Erdős-Problemen liege nur bei ein bis zwei Prozent, konzentriert auf leichtere Aufgaben. Auch das Google-System war in nur neun von 353 Aufgaben erfolgreich. Das entspricht ziemlich genau Taos Zwei-Prozent-Hürde.
KI-News ohne Hype – von Menschen kuratiert
Mit dem THE‑DECODER‑Abo liest du werbefrei und wirst Teil unserer Community: Diskutiere im Kommentarsystem, erhalte unseren wöchentlichen KI‑Newsletter, 6× im Jahr den "KI Radar"‑Frontier‑Newsletter mit den neuesten Entwicklungen aus der Spitze der KI‑Forschung, bis zu 25 % Rabatt auf KI Pro‑Events und Zugriff auf das komplette Archiv der letzten zehn Jahre.
