Künstliche Intelligenz löst mathematische Probleme auf Niveau von Silbermedaillengewinnern

Wir haben große Fortschritte bei der Entwicklung von KI-Systemen gemacht, die Mathematikern helfen, neue Erkenntnisse, innovative Algorithmen und Antworten auf offene Probleme zu entdecken. Aber aktuelle KI-Systeme haben immer noch Schwierigkeiten, allgemeine mathematische Probleme zu lösen, aufgrund von Einschränkungen in den Denkfähigkeiten und Trainingsdaten. AlphaProof, ein neues auf Verstärkungslernen basierendes System für formales mathematisches Denken, und AlphaGeometry 2, eine verbesserte Version eines Geometrielösungssystems. Gemeinsam lösten diese Systeme vier von sechs Problemen der diesjährigen Internationalen Mathematikolympiade (IMO) und erreichten zum ersten Mal das Niveau eines Silbermedaillengewinners im Wettbewerb.

Der jährliche Wettbewerb der Internationalen Mathematikolympiade (IMO) hat sich auch als eine große Herausforderung im Bereich des maschinellen Lernens etabliert und als ein inspirierender Maßstab zur Messung der fortgeschrittenen mathematischen Denkfähigkeiten eines KI-Systems. In diesem Jahr wandte Deep Mind ihr kombiniertes KI-System auf die vom IMO-Veranstalter bereitgestellten Wettbewerbsprobleme an. Die Lösungen wurden nach den Punktvergaberegeln der IMO von prominenten Mathematikern bewertet: Prof. Sir Timothy Gowers, ein IMO-Goldmedaillengewinner und Fields-Medaillenträger, sowie Dr. Joseph Myers, zweimaliger IMO-Goldmedaillengewinner und Vorsitzender des IMO 2024 Problem Selection Committee.

Die Tatsache, dass das Programm eine nicht offensichtliche Konstruktion wie diese entwickeln kann, ist sehr beeindruckend und weit über das hinaus, was ich für den Stand der Technik hielt. AlphaProof ist ein System, das sich selbst darauf trainiert, mathematische Aussagen in der formalen Sprache Lean zu beweisen. Es koppelt ein vorab trainiertes Sprachmodell mit dem AlphaZero-Verstärkungslernalgorithmus, der sich zuvor selbst beigebracht hat, die Spiele Schach, Shogi und Go zu beherrschen.

Formale Sprachen bieten den entscheidenden Vorteil, dass Beweise mit mathematischer Argumentation formal auf Korrektheit überprüft werden können. Ihr Einsatz im maschinellen Lernen war jedoch bisher durch die sehr begrenzte Menge an menschlich geschriebenen Daten eingeschränkt. Im Gegensatz dazu können sprachbasierte Ansätze plausible aber falsche Zwischenschritte und Lösungen halluzinieren, obwohl sie Zugriff auf Größenordnungen mehr Daten haben.

Wir haben eine Brücke zwischen diesen beiden komplementären Bereichen geschlagen, indem wir ein Gemini-Modell feinabgestimmt haben, um natürlichsprachliche Problemstellungen automatisch in formale Aussagen zu übersetzen und eine große Bibliothek formaler Probleme unterschiedlicher Schwierigkeitsgrade zu erstellen.

AlphaProof generiert Lösungskandidaten für ein Problem und beweist oder widerlegt sie dann durch die Suche nach möglichen Beweisschritten in Lean. Jeder gefundene und überprüfte Beweis wird verwendet, um das Sprachmodell von AlphaProof zu verstärken und seine Fähigkeit zur Lösung anschließender schwierigerer Probleme zu verbessern.