Google DeepMind hat Forschungsergebnisse vorgestellt, in denen ihr Forschungsagent AlphaProof Nexus die Fähigkeit unter Beweis stellte, nicht nur Olympiade-Aufgaben, sondern offene mathematische Probleme auf Forschungsniveau zu lösen. Das System löste 9 von 353 offenen Problemen, die mit dem Namen des ungarischen Mathematikers Paul Erdös verbunden sind, wobei zwei davon 56 Jahre lang ungelöst geblieben waren. Darüber hinaus bewies der Agent 44 von 492 offenen Vermutungen aus der Online-Enzyklopädie ganzzahliger Folgen (OEIS). Nach Einschätzung der Autoren kosteten die Berechnungen für jedes gelöste Erdös-Problem einige hundert Dollar.

Neun Erdös-Probleme und 44 OEIS-Vermutungen

Die Arbeit widmet sich der Anwendung großer Sprachmodelle zur Suche nach formalen Beweisen. Die Autoren gingen bewusst über Standard-Wettbewerbsaufgaben hinaus und testeten den Ansatz an echten offenen Problemen, mit denen sich die Mathematik seit Jahren plagt. Der Erfolg bei 9 Erdös-Problemen und 44 OEIS-Vermutungen zeigt, dass der Ansatz für die explorative Mathematik geeignet ist und nicht nur für Lehr- und Wettbewerbsbeispiele. Wichtig ist dabei, dass der Agent die Mehrheit der offenen Erdös-Probleme nicht lösen konnte: Die aktuellen Erfolge konzentrieren sich auf Bereiche, für die bereits eine entwickelte Bibliothek formalisierter Ergebnisse existiert und komplexe Überlegungen in einzelne Teilprobleme zerlegt werden können.

Formale Überprüfung statt überzeugender Erklärung

Der Hauptunterschied zwischen AlphaProof Nexus und einem gewöhnlichen Chatbot ist die Verwendung von Lean, einer Sprache und Umgebung zur Formalisierung mathematischer Beweise. Die KI schlägt einen Beweis in formaler Form vor, woraufhin Lean jeden logischen Schritt überprüft. Wenn die Überprüfung einen Fehler entdeckt, erhält der Agent Feedback und setzt die Suche fort. Eine überzeugend geschriebene Erklärung reicht nicht aus: Das Ergebnis muss eine maschinelle Überprüfung nach strengen logischen Regeln bestehen. Genau diese Schleife aus „Generierung — Überprüfung — Korrektur“ macht den Prozess für echte Mathematik geeignet und nicht für die Generierung plausiblen Textes.

Architektur: Mehrere Agenten und ein evolutionärer Algorithmus

In AlphaProof Nexus suchen mehrere KI-Agenten parallel nach Lösungen, überprüfen Ansätze und verfeinern Beweise. In der komplexesten Konfiguration wird ihre Arbeit von einem evolutionären Algorithmus koordiniert, während für bestimmte Suchphasen AlphaProof eingesetzt wird — ein von Google DeepMind entwickeltes und auf Reinforcement Learning basierendes System zum automatisierten Beweisen von Theoremen. Diese Multi-Agenten-Architektur ermöglicht es, die Suche auf verschiedene Strategien zu verteilen und die vielversprechendsten Beweiszweige auszuwählen.

Ein einfacher Agent hat es auch geschafft — aber teurer

Die Autoren verglichen separat die komplexe Architektur mit einem einfacheren Agenten, der lediglich die Beweisgenerierung durch das Sprachmodell mit der Überprüfung in Lean abwechselt. Bei der erneuten Analyse der neun gelösten Erdös-Probleme schaffte der einfache Agent ebenfalls alle neun. Bei den schwierigsten Aufgaben war seine Verwendung jedoch teurer. Dies deutet darauf hin, dass das Ergebnis nicht nur von den Fähigkeiten des Sprachmodells selbst abhängt, sondern auch von der Organisation der Beweissuche: Die komplexe Architektur spart Rechenleistung bei schwierigen Fällen.

Horizonte und Grenzen

Die Fähigkeiten des Systems beschränken sich nicht auf Erdös-Probleme und OEIS-Vermutungen. AlphaProof Nexus half dabei, ein offenes Problem in der algebraischen Geometrie zu lösen, Schätzungen in der konvexen Optimierung zu verbessern und Fehler bei der Formalisierung mathematischer Aussagen zu entdecken, die in der wissenschaftlichen Literatur vorkommen. Es wird auch in der Graphentheorie und Quantenoptik-Forschung eingesetzt. Gleichzeitig erbt das System die Einschränkungen von Sprachsmodellen: Die Suchergebnisse können von Versuch zu Versuch stark variieren, und Probleme, die die Entwicklung einer umfassenden neuen Theorie erfordern, bleiben außerhalb seiner Reichweite. Die Autoren glauben, dass formale Beweise eine Möglichkeit sein können, KI in echte mathematische Arbeit einzubinden, anstatt nur Antworten von ihr zu erhalten.