Google DeepMind knackt 56 Jahre alte Rätsel
AlphaProof Nexus beweist ungelöste Probleme der Mathematik. Es arbeitet fehlerfrei dank ständiger Code Überprüfung.
Google DeepMind hat mit AlphaProof Nexus ein KI-Modell präsentiert, das neun ungelöste Erdős-Probleme der Mathematik selbstständig bewiesen hat. Die Architektur kombiniert das Sprachmodell Gemini 3.1 Pro mit der Verifizierungssprache Lean und filtert so Logikfehler automatisch heraus. Einige der gelösten Aufgaben galten seit 56 Jahren als offene Fragen der Forschung.
Compiler verhindert mathematische Halluzinationen
Große KI-Modelle erzeugen bei komplexen Beweisen häufig subtile Denkfehler, die von Experten aufwendig korrigiert werden müssen. AlphaProof Nexus löst dieses Problem durch einen formalen Filter. Das KI-Modell formuliert seine Lösungsansätze in Lean, woraufhin ein Compiler jeden einzelnen logischen Schritt direkt auf Korrektheit prüft.
Wenn das KI-Modell einen Beweis erfindet, der in der Fachliteratur nicht existiert, schlägt der Code-Check sofort fehl. Erst wenn der Lean-Compiler den gesamten Beweis ohne Fehlermeldung akzeptiert, ist die Aufgabe gelöst. Dadurch fungiert das KI-Modell gleichzeitig als Lösungsfinder und diagnostisches Instrument, das Ungenauigkeiten in bestehenden Problemstellungen erkennt.
Quelle: Google - Funktionsweise
Geringe Kosten und einfache Architektur
Die Forscher testeten die KI an 353 Erdős-Problemen sowie an 492 ungelösten Vermutungen der Online Encyclopedia of Integer Sequences (OEIS). AlphaProof Nexus lieferte neben den neun Erdős-Lösungen auch 44 gültige OEIS-Beweise. Die Rechenkosten für einen erfolgreichen Beweis beliefen sich auf lediglich wenige hundert US-Dollar.
Die Studie zeigt eine interessante Entwicklung im Aufbau aktueller KI-Modelle auf. Eine simple Basisversion, die nur zwischen Prompting und Compiler-Feedback wechselte, konnte alle neun Erdős-Beweise reproduzieren. Die aufwendige Vollversion mit evolutionärer Suche und zusätzlichen AlphaProof-Komponenten brachte nur bei den extrem schwierigen Aufgaben einen statistischen Vorteil.
Neben den klassischen Beweisen entdeckte das KI-Modell auch einen neuen algorithmischen Parameter in der Optimierungstheorie. Dieser war menschlichen Forschern bisher verborgen geblieben. Die Ergebnisse deuten darauf hin, dass einfache Feedback-Schleifen zunehmend mit spezialisierten Architekturen konkurrieren können.
Quelle: Google - Beispielausgabe
Starke Abhängigkeit von Lean-Bibliotheken
Die Fähigkeiten des KI-Modells unterliegen jedoch klaren technischen Begrenzungen. Erfolge verzeichnet das Projekt primär in der Kombinatorik, der Optimierung und der Zahlentheorie. In diesen Fachbereichen ist die mathematische Bibliothek von Lean bereits sehr ausgereift und bietet dem KI-Modell eine solide Basis.
Fehlt diese Vorarbeit, stößt die KI an ihre Grenzen. Aufgaben, die den Aufbau umfangreicher neuer Theorien erfordern, bleiben vorerst außerhalb der Reichweite. Die Mehrheit der 353 getesteten Erdős-Probleme konnte AlphaProof Nexus daher noch nicht knacken. Das Projekt zeigt dennoch präzise, wie formale Verifizierung die Zuverlässigkeit von KI-Modellen in der Forschung messbar erhöht.
