Silbermedaille für Google-KI bei Mathematik-Olympiade
AlphaProof und AlphaGeometry 2 lösten vier von sechs Aufgaben. Damit erreichten sie bei dem prestigeträchtigen Wettbewerb das Niveau einer Silbermedaille.
(Bild: Phonlamai Photo/Shutterstock.com)
Mathematische Aufgaben zu lösen, gehört zu einer der großen Herausforderungen für künstliche Intelligenzen. Googles Tochterunternehmen DeepMind testete nun ihre KIs mit den Aufgaben der diesjährigen internationalen Mathematikolympiade (IMO). Dabei konnten die Modelle vier von sechs Aufgaben korrekt lösen und erreichten so das Niveau einer Silbermedaille, wie DeepMind in einem Blog-Beitrag verkündet.
An der IMO nehmen jedes Jahr Schülerinnen und Schüler aus über 100 Ländern teil. Sie haben zweimal viereinhalb Stunden Zeit, um die insgesamt sechs anspruchsvollen Aufgaben zu lösen. Dabei sammeln die Teilnehmenden Punkte und je nach Punktzahl können sie dabei eine Bronze-, Silber- oder Goldmedaillen gewinnen. Die Aufgaben stammen aus den mathematischen Teilgebieten der Algebra, Kombinatorik, Geometrie und Zahlentheorie. Die IMO 2024 fand Mitte Juli im englischen Bath statt.
DeepMind testete ihre KI-Modelle AlphaProof und AlphaGeometry 2 mit den Aufgaben der diesjährigen IMO. Die zwei Modelle konnten vier von sechs Aufgaben korrekt lösen: AlphaProof löste zwei algebraische Probleme und eines aus der Zahlentheorie – darunter das schwierigste Problem der Olympiade, das nur von fünf Teilnehmenden gelöst wurde. AlphaGeometry2 löste das geometrische Problem. Beide scheiterten aber an den zwei kombinatorischen Aufgaben. Damit erzielten die KIs gemeinsam 28 von 42 Punkten. Das entspricht einer Silbermedaille, für Gold fehlte nur ein Punkt. Allerdings hätten die KI-Modelle im Wettbewerb das Zeitlimit gerissen: Für eine der Lösungen benötigten die KIs drei Tage, eine andere lösten sie hingegen in wenigen Minuten.
Die Lösungen der KI begutachteten die Mathematiker Prof. Sir Timothy Gowers, IMO-Gold- und Fields-Medaillengewinner, und Dr. Joseph Myers, zweifacher IMO-Goldmedaillengewinner und Vorsitzender des Problemauswahlkomitees der IMO 2024. "Die Tatsache, dass das Programm mit einer nicht offensichtlichen Konstruktion wie dieser aufwarten kann, ist sehr beeindruckend und geht weit über das hinaus, was ich für den Stand der Technik hielt", sagt Gowers im DeepMind-Blog.
Kombinierte Sprachmodelle
AlphaProof formalisiert mathematische Sprache, um Probleme zu lösen. Zuerst werden mathematische Probleme mithilfe eines Gemini-basierten Sprachmodells in die Programmiersprache Lean übersetzt. Dabei handelt es sich um einen Assistenten für mathematische Beweise. Dann erzeugt AlphaZero – ein Algorithmus, der bestärkendes Lernen (reinforcement learning) benutzt und sich zuvor Schach und Go beigebracht hat – einen Beweisvorschlag. Dieser wird schließlich mithilfe von Lean überprüft. Dies hat den Vorteil, dass von der KI halluzinierte Lösungen überprüft und aussortiert werden können.
AlphaGeometry2 ist die Weiterentwicklung des Tools AlphaGeometry zum Lösen geometrischer Probleme. Letztere löste Anfang des Jahres bereits Aufgaben früherer IMO. Bei AlphaGeometry2 handelt sich um eine neuro-symbolische KI: Sie verbindet also neuronale Netzwerke mit symbolischer KI. Während das Sprachmodell schnell potenzielle Lösungen identifiziert, kann es seine Entscheidungen nicht begründen. Das verwendete Sprachmodell basiert auf Gemini, wurde aber mit zehnmal mehr Daten als sein Vorgänger neu trainiert. Symbolische KIs hingegen basieren auf formaler Logik und verwenden klare Regeln, um zu Schlussfolgerungen zu gelangen. Mit dieser Kombination konnte AlphaGeometry2 83 Prozent der Geometrieaufgaben der IMO der letzten 25 Jahre lösen – sein Vorgänger nur 53 Prozent.
Lesen Sie auch
Künstliche Allgemeine Intelligenz: Wissen, was wahr ist
KI-Training mit synthetischen Daten: "Das Internet kommt ans Fördermaximum"
Künstliche Intelligenz: Der schwere Kampf gegen Halluzinationen
Anthropics Claude drängt in KI-Geschäftskundenmarkt
Freitag: Kriegsschiff mit heimlichem Starlink, China bringt Marsproben zur Erde
Zuletzt entwickelten sich die Aufgaben der IMO als Herausforderung für maschinelles Lernen und sie gelten als ein Maßstab für die Fähigkeit einer KI, fortgeschrittene mathematische Aufgaben zu lösen. Eine Künstliche Allgemeine Intelligenz (AGI, für Artificial General Intelligence), die in der Lage wäre, komplexe, mathematische Probleme zu lösen, hätte zahlreiche Einsatzgebiete in der Forschung und Entwicklung von Technologie.
Ihr könnt die c't auch bei WhatsApp abonnieren: Wir schicken werktäglich Einordnungen zu aktuellen Themen und Einblicke in den Redaktionsalltag.
(spa)