Sind DeepMinds neun Beweise neu?

Bei mathematischen Beweisen sind formale Richtigkeit und wissenschaftlicher Neuigkeitswert zwei verschiedene Fragen. Google DeepMinds KI-Agent AlphaProof Nexus hat Beweise für neun von Paul Erdős gestellte Probleme erzeugt; eine Software prüfte jeden einzelnen Schritt. Die Arbeit erschien im Mai zunächst als Preprint (arXiv und nach Begutachtung am 8. Oktober in Science (Science). Ob die korrekte Argumentation auch etwas Neues ergab, mussten Mathematiker beurteilen.

Ein Prüfer, der sich nicht blenden lässt

Chatbots können mathematische Texte erzeugen, die plausibel klingen. Ein selbstsicher formulierter Absatz kann einen fehlenden Schritt verdecken, den nur sorgfältiges Lesen aufdeckt. AlphaProof Nexus arbeitet mit Lean, einer Programmiersprache, in der Definitionen, Behauptungen und Beweise so präzise formuliert werden, dass ein Computer sie prüfen kann.

Man kann sich Lean als Prüfer vorstellen, der jede Zeile eines fertigen Beweises liest und feste Regeln anwendet. Auf den Stil kommt es nicht an. Folgt ein Schritt nicht aus den vorherigen, scheitert der Beweis, mag der Rest noch so elegant sein.

Nach Darstellung des Teams sucht der Agent nach Beweisen, die in Lean geschrieben sind. Die Forschenden gaben ihm zudem Zugriff auf AlphaProof, ein älteres DeepMind-System, das eigens für mathematische Beweise entwickelt wurde. In den Tests erzielte jedoch auch eine einfachere Konfiguration dieselben Ergebnisse: Ein Sprachmodell in Verbindung mit Lean, aber ohne AlphaProof, fand alle neun Erdős-Beweise (The Decoder). Bei diesen Aufgaben war die spezialisierte Komponente entbehrlich.

Die Studie berichtet von formal geprüften Beweisen für die neun Erdős-Aussagen und für 44 Vermutungen aus der Online Encyclopedia of Integer Sequences. Vermutungen sind Aussagen, die als wahr gelten, aber noch nicht bewiesen wurden; die Enzyklopädie katalogisiert eine große Zahl von Zahlenfolgen (Science). Zu den Erdős-Ergebnissen gehört eine zweiteilige Frage zu ganzen Zahlen, die Erdős und András Sárközy 1970 gestellt hatten. Sie blieb mehr als ein halbes Jahrhundert offen (ABC).

Was der Prüfer nicht erkennen kann

Leans Garantie reicht genau so weit, wie die Aussage im Code formuliert ist: Das System bestätigt, dass der Beweis diese Aussage herleitet. Drei Fragen kann es nicht beantworten: ob der Code Erdős’ Absicht trifft, ob jemand die Frage längst beantwortet hat und ob die Lösung neue Erkenntnisse bringt.

Das Problem von 1970 zeigt, warum die letzten beiden Fragen wichtig sind. Sein zweiter Teil impliziert den ersten, sodass ein Beweis beide Fragen klärt. Nachdem die Beweise des Agenten bekannt geworden waren, zeigte sich, dass schon eine kleine Änderung an einer Konstruktion im ursprünglichen Aufsatz von 1970 beide Teile beantwortet (arXiv). Die Beweise des Agenten waren korrekt. Das Problem war schlicht näher an einer Lösung, als sein Status als „offen“ vermuten ließ.

Solche Zusammenhänge erkennen Fachleute. Gergely Bérczi, Mathematiker an der Aarhus University in Dänemark und Mitautor der Studie, half bei der Auswahl geeigneter Fragen und bei der Prüfung der Lösungen (Aarhus University). Außerdem wirkte er an Fassungen der Beweise mit, denen Menschen folgen können. Lean bestätigte jeden einzelnen Schritt; Bérczi und seine Kollegen beurteilten, was die Schritte zusammen ergaben.

Diese Arbeitsteilung unterscheidet die Studie von einem Fortschritt des vergangenen Monats. Damals übertrug Anthropics Claude den bereits bekannten Beweis des Fermatschen letzten Satzes in Lean (To Brief). Bei einem berühmten, bekannten Beweis stellt sich die Frage nach seiner Neuheit nicht. Bei der Suche unter Aussagen, die als ungelöst gelten, wird sie zentral.

Das Team hat die Beweisdateien veröffentlicht, sodass andere sie mit demselben Prüfer nachvollziehen können (GitHub). Der Befund der Studie ist klar umrissen: Ein KI-Agent erzeugte maschinenprüfbare Beweise für einige Aussagen, die Mathematiker als ungelöst behandelt hatten. Die formale Garantie gilt für diese Aussagen in ihrer Lean-Fassung. Was die Beweise zur Mathematik beitrugen, mussten weiterhin die Mathematiker beurteilen, die sie lasen.