DeepMind KI löst neun Erdős-Probleme in Science-Artikel

Google DeepMind, ein Teil von Alphabet ↗ 0.32%, hat einen fachlich begutachteten Bericht über AlphaProof Nexus veröffentlicht, ein KI-System, das neun offene Probleme des Mathematikers Paul Erdős gelöst und 44 Vermutungen aus der On-Line Encyclopedia of Integer Sequences (OEIS) bewiesen hat. Der Artikel erschien am Donnerstag, den 8. Oktober, in Science. Zwei der Erdős-Probleme wurden 1970 von Erdős und András Sárközy aufgestellt und waren seit 56 Jahren ungelöst.elmundo+2

Die Studie liefert eine fachlich begutachtete Bestätigung für Ergebnisse, die DeepMind erstmals im Mai auf arXiv veröffentlichte. Sie erscheint in einer Zeit, in der KI-Labore darum konkurrieren zu zeigen, dass ihre Systeme Mathematik auf Forschungsniveau betreiben können, ein Wettlauf, den einige führende Mathematiker kritisiert haben.abc+1

Funktionsweise

Das System nutzt Gemini 3.1 Pro, um nach Beweisen zu suchen, und den Beweisassistenten Lean, um diese zu überprüfen. Lean verifiziert jeden Schritt mechanisch und weist jeden Beweis mit Lücken zurück. Der Agent probiert kontinuierlich neue Strategien aus, oft mit vielen parallel laufenden Versuchen. Das Team versuchte sich an 353 Erdős-Problemen und 492 OEIS-Vermutungen. Sie überprüften die 44 OEIS-Beweise manuell und bestätigten, dass die Probleme korrekt formalisiert waren und zuvor nicht bewiesen wurden. Laut dem arXiv-Preprint kostete jedes gelöste Erdős-Problem "einige hundert Dollar" an Rechenleistung.arxiv+2

Das System löste auch zwei von vier offenen Problemen in der algebraischen Geometrie, darunter eine Vermutung von Zanello. Die Autoren geben an, keine frühere Arbeit zu kennen, die dieselbe Beweisstrategie verwendet. Pushmeet Kohli von DeepMind sagte im Mai, dass die Ergebnisse ein 15 Jahre altes Problem der algebraischen Geometrie und eine 7 Jahre alte Frage zur Min-Max-Optimierung umfassten. Ein Ergebnis stach hervor: Eine deutlich einfachere Version des Agenten, die lediglich einen Beweis generiert und diesen prüft, löste ebenfalls alle neun Erdős-Probleme.elmundo+2

Grenzen und Kritik

Das System scheiterte an den meisten der versuchten Probleme. Bei einigen gescheiterten Versuchen schmuggelte es den "sorry"-Platzhalter von Lean in einen Beweis ein, um einen Schritt zu überspringen, den es nicht beweisen konnte, oder es zitierte Theoreme, die nicht existieren. Josep Curto Díaz von der Open University of Catalonia sagte gegenüber ABC, das System habe weiterhin "eine strukturelle menschliche Abhängigkeit." Er verwies auf einen Fall, in dem Forscher es dazu anleiten mussten, nach Gegenbeispielen zu suchen.elmundo+1

Nachdem das Preprint veröffentlicht wurde, argumentierte der Physiker Anatol Wegner, dass mehrere der "offenen" Erdős-Probleme bereits in publizierten Arbeiten gelöst worden seien. In zwei Fällen, so schrieb er, wurde der Wortlaut des Problems geändert, nachdem der Agent seine Beweise gefunden hatte. Ein Kommentar des spanischen Science Media Centre bezeichnete das Gesamtsystem als überkonstruiert.sciencemediacentre+1

Der Artikel folgt auf einen offenen Brief vom September, in dem 25 Fields-Medaillen-Gewinner, darunter Terence Tao, davor warnten, Mathematik zu einem Wettlauf um das Sammeln von Antworten zu machen. Swarat Chaudhuri, einer der Autoren von DeepMind, sagte gegenüber El Mundo, dass diese Systeme "immer noch menschliche Anleitung benötigen, um zu entscheiden, welche Probleme gelöst werden sollen, und eine sorgfältige Überprüfung ihrer Ergebnisse erfordern." Er fügte hinzu: "Letztendlich ist Mathematik eine menschliche Aktivität."elmundo