KI bei der Internationalen Mathematik-Olympiade: Wie AlphaProof und AlphaGeometry 2 die Silbermedaille erreichten

Mathematisches Denken ist ein wesentlicher Aspekt der menschlichen kognitiven Fähigkeiten und treibt den Fortschritt wissenschaftlicher Entdeckungen und technologischer Entwicklungen voran. Da wir danach streben, künstliche Intelligenz zu entwickeln, die der menschlichen Kognition entspricht, ist es unerlässlich, KI mit fortgeschrittenen mathematischen Denkfähigkeiten auszustatten. Während aktuelle KI-Systeme grundlegende mathematische Probleme bewältigen können, haben sie Schwierigkeiten mit dem komplexen Denken, das für fortgeschrittene mathematische Disziplinen wie Algebra und Geometrie erforderlich ist. Dies könnte sich jedoch ändern, wie Google DeepMind gezeigt hat. bedeutende Fortschritte bei der Weiterentwicklung der mathematischen Denkfähigkeiten eines KI-Systems. Dieser Durchbruch wird bei der Internationale Mathematik-Olympiade (IMO) 2024. Die IMO wurde 1959 ins Leben gerufen und ist der älteste und renommierteste Mathematikwettbewerb, der Gymnasiasten weltweit mit Problemen aus Algebra, Kombinatorik, Geometrie und Zahlentheorie herausfordert. Jedes Jahr treten Teams junger Mathematiker gegeneinander an und müssen sechs sehr anspruchsvolle Probleme lösen. In diesem Jahr stellte Google DeepMind zwei KI-Systeme vor: AlphaProof, das sich auf formales mathematisches Denken konzentriert, und AlphaGeometry 2, das auf das Lösen geometrischer Probleme spezialisiert ist. Diese KI-Systeme konnten vier von sechs Problemen lösen und erreichten damit die Leistung eines Silbermedaillengewinners. In diesem Artikel werden wir untersuchen, wie diese Systeme bei der Lösung mathematischer Probleme funktionieren.

AlphaProof: Kombination von KI und formaler Sprache zum Beweisen mathematischer Theoreme

AlphaProof ist ein KI-System, das mathematische Aussagen mithilfe der formalen Sprache beweisen soll Lehnen. Es integriert Gemini, ein vorab trainiertes Sprachmodell, mit AlphaZero, ein Verstärkungslernalgorithmus, der für die Beherrschung von Schach, Shogi und Go bekannt ist.

Das Gemini-Modell übersetzt Problemstellungen in natürlicher Sprache in formale und erstellt so eine Bibliothek von Problemen mit unterschiedlichen Schwierigkeitsgraden. Dies dient zwei Zwecken: der Umwandlung unpräziser natürlicher Sprache in präzise formale Sprache zur Überprüfung mathematischer Beweise und der Nutzung der Vorhersagefähigkeiten von Gemini zur Generierung einer Liste möglicher Lösungen mit formaler Sprachpräzision.

Wenn AlphaProof auf ein Problem stößt, generiert es mögliche Lösungen und sucht nach Beweisschritten in Lean, um diese zu verifizieren oder zu widerlegen. Dies ist im Wesentlichen ein neurosymbolischer Ansatz, bei dem das neuronale Netzwerk Gemini Anweisungen in natürlicher Sprache in die symbolische formale Sprache Lean übersetzt, um die Aussage zu beweisen oder zu widerlegen. Ähnlich wie AlphaZeros Selbstspielmechanismus, bei dem das System lernt, indem es Spiele gegen sich selbst spielt, trainiert sich AlphaProof selbst, indem es versucht, mathematische Aussagen zu beweisen. Jeder Beweisversuch verfeinert das Sprachmodell von AlphaProof, wobei erfolgreiche Beweise die Fähigkeit des Modells verstärken, anspruchsvollere Probleme anzugehen.

Für die Internationale Mathematik-Olympiade (IMO) wurde AlphaProof durch das Beweisen oder Widerlegen von Millionen von Problemen verschiedener Schwierigkeitsgrade und mathematischer Themen trainiert. Dieses Training wurde während des Wettbewerbs fortgesetzt, wobei AlphaProof seine Lösungen verfeinerte, bis es vollständige Antworten auf die Probleme gefunden hatte.

AlphaGeometry 2: Integration von LLMs und symbolischer KI zur Lösung geometrischer Probleme

AlphaGeometry 2 ist die neueste Version des AlphaGeometry Serie, die darauf ausgelegt ist, geometrische Probleme mit verbesserter Präzision und Effizienz anzugehen. Aufbauend auf den Grundlagen seines Vorgängers verwendet AlphaGeometry 2 einen neurosymbolischen Ansatz, der neuronale Large Language Models (LLMs) mit symbolischer KI verbindet. Diese Integration kombiniert regelbasierte Logik mit der Vorhersagefähigkeit neuronaler Netzwerke, Hilfspunkte zu identifizieren, die für die Lösung geometrischer Probleme unerlässlich sind. Das LLM in AlphaGeometry sagt neue geometrische Konstrukte voraus, während die symbolische KI formale Logik anwendet, um Beweise zu generieren.

Bei geometrischen Problemen evaluiert AlphaGeometrys LLM zahlreiche Möglichkeiten und prognostiziert Konstrukte, die für die Problemlösung entscheidend sind. Diese Vorhersagen dienen als wertvolle Hinweise, die die symbolische Engine zu präzisen Schlussfolgerungen führen und sie der Lösung näherbringen. Dieser innovative Ansatz ermöglicht es AlphaGeometry, komplexe geometrische Herausforderungen zu bewältigen, die über konventionelle Szenarien hinausgehen.

Eine wichtige Verbesserung in AlphaGeometry 2 ist die Integration des Gemini LLM. Dieses Modell wird von Grund auf mit deutlich mehr synthetischen Daten trainiert als sein Vorgänger. Dieses umfangreiche Training befähigt es, schwierigere Geometrieprobleme zu bewältigen, darunter solche mit Objektbewegungen und Gleichungen von Winkeln, Verhältnissen oder Entfernungen. Darüber hinaus verfügt AlphaGeometry 2 über eine symbolische Engine, die zwei Größenordnungen schneller arbeitet und es ermöglicht, alternative Lösungen mit beispielloser Geschwindigkeit zu erkunden. Diese Fortschritte machen AlphaGeometry 2 zu einem leistungsstarken Werkzeug zur Lösung komplexer geometrischer Probleme und setzen einen neuen Standard in diesem Bereich.

AlphaProof und AlphaGeometry 2 bei IMO

Bei der diesjährigen Internationalen Mathematik-Olympiade (IMO) wurden die Teilnehmer mit sechs unterschiedlichen Aufgaben geprüft: zwei aus Algebra, eine aus Zahlentheorie, eine aus Geometrie und zwei aus Kombinatorik. Google-Forscher übersetzt diese Probleme in eine formale mathematische Sprache für AlphaProof und AlphaGeometry 2. AlphaProof befasste sich mit zwei Algebra-Problemen und einem Zahlentheorie-Problem, darunter dem schwierigsten Problem des Wettbewerbs, das dieses Jahr nur von fünf menschlichen Teilnehmern gelöst wurde. Unterdessen löste AlphaGeometry 2 erfolgreich das Geometrieproblem, obwohl es die beiden kombinatorischen Herausforderungen nicht knackte.

Jedes Problem bei der IMO ist sieben Punkte wert, insgesamt also maximal 42. AlphaProof und AlphaGeometry 2 erhielten 28 Punkte und erreichten die volle Punktzahl für die von ihnen gelösten Probleme. Damit erreichten sie das obere Ende der Silbermedaillenkategorie. Die Goldmedaillenschwelle lag dieses Jahr bei 29 Punkten, die 58 der 609 Teilnehmer erreichten.

Nächster Schritt: Natürliche Sprache für mathematische Herausforderungen

AlphaProof und AlphaGeometry 2 haben beeindruckende Fortschritte bei der Lösung mathematischer Probleme durch KI gezeigt. Diese Systeme sind jedoch immer noch auf menschliche Experten angewiesen, die mathematische Probleme zur Verarbeitung in eine formale Sprache übersetzen. Darüber hinaus ist unklar, wie diese speziellen mathematischen Fähigkeiten in andere KI-Systeme integriert werden können, beispielsweise zur Untersuchung von Hypothesen, zum Testen innovativer Lösungen für langjährige Probleme und zur effizienten Bewältigung zeitaufwändiger Aspekte von Beweisen.

Um diese Einschränkungen zu überwinden, entwickeln Google-Forscher ein System zur natürlichen Spracherkennung auf der Grundlage von Gemini und ihrer neuesten Forschung. Dieses neue System zielt darauf ab, Problemlösungsfähigkeiten zu verbessern, ohne dass eine formale Sprachübersetzung erforderlich ist, und ist so konzipiert, dass es sich problemlos in andere KI-Systeme integrieren lässt.

Fazit

Die Leistung von AlphaProof und AlphaGeometry 2 bei der Internationalen Mathematik-Olympiade stellt einen bemerkenswerten Fortschritt in der Fähigkeit der KI dar, komplexe mathematische Denkprozesse zu bewältigen. Beide Systeme erreichten mit der Lösung von vier von sechs anspruchsvollen Problemen eine Leistung auf Silbermedaillenniveau und stellten damit bedeutende Fortschritte bei formalen Beweisen und der Lösung geometrischer Probleme dar. Trotz ihrer Erfolge sind diese KI-Systeme weiterhin auf menschliche Eingaben angewiesen, um Probleme in formale Sprache zu übersetzen, und stehen vor Herausforderungen bei der Integration mit anderen KI-Systemen. Zukünftige Forschung zielt darauf ab, diese Systeme weiter zu verbessern und möglicherweise natürliche Sprachschlüsse zu integrieren, um ihre Fähigkeiten auf ein breiteres Spektrum mathematischer Herausforderungen auszudehnen.