Von Silber zu Gold: Wie DeepMinds KI den Mathematik-Olympiad-Wettbewerb gewann

DeepMinds KI hat in nur einem Jahr bemerkenswerte Fortschritte in der mathematischen Argumentation gemacht. Nachdem sie 2024 eine Silbermedaille bei der Internationalen Mathematik-Olympiade (IMO) gewonnen hatte, gewann ihr KI-System 2025 die Goldmedaille. Diese schnelle Verbesserung unterstreicht die wachsenden Fähigkeiten der künstlichen Intelligenz bei der Lösung komplexer, abstrakter Probleme, die menschliche Kreativität und Einsicht erfordern. Dieser Artikel wird zeigen, wie DeepMind diese Transformation erreicht hat, die technischen und strategischen Entscheidungen dahinter und die breiteren Auswirkungen dieser Fortschritte.

Die Bedeutung der IMO

Die Internationale Mathematik-Olympiade, die 1959 gegründet wurde, gilt weltweit als der wichtigste Mathematikwettbewerb für Schüler. Jedes Jahr müssen die besten Schüler aus der ganzen Welt sechs herausfordernde Probleme in Algebra, Geometrie, Zahlentheorie und Kombinatorik lösen. Das Lösen dieser Probleme erfordert mehr als nur Berechnungen; die Teilnehmer müssen echte mathematische Kreativität, strenge logisches Denken und die Fähigkeit zeigen, elegante Beweise zu konstruieren.

Für die künstliche Intelligenz stellt die IMO eine einzigartige Herausforderung dar. Während die KI Mustererkennung, Datenanalyse und sogar komplexe Spiele wie Go und Schach beherrscht, erfordert die Mathematik-Olympiade kreative, abstrakte Argumentation und die Synthese neuer Ideen, Fähigkeiten, die traditionell als Merkmale der menschlichen Intelligenz gelten. Daher ist die IMO zu einem natürlichen Testfeld für die Bewertung der Fähigkeiten der KI geworden, um wirklich menschliche Argumentation zu erreichen.

Der Silber-Medaillen-Durchbruch von 2024

2024 stellte DeepMind zwei KI-Systeme vor, um IMO-niveau-Probleme zu lösen: AlphaProof und AlphaGeometry 2. Beide Systeme sind Beispiele für “neuro-symbolische” KI, die die Stärken von großen Sprachmodellen (LLM) mit der Strenge von symbolischer Logik kombinieren.

AlphaProof wurde entwickelt, um mathematische Aussagen mit Lean, einer formalen mathematischen Sprache, zu beweisen. Es kombinierte Gemini, DeepMinds großes Sprachmodell, mit AlphaZero, einem Reinforcement-Learning-Engine, der für seine Erfolge in Brettspielen bekannt ist. In diesem Setting war die Rolle von Gemini, natürliche Sprachprobleme in Lean zu übersetzen und Beweise durch die Generierung logischer Schritte zu versuchen. AlphaProof wurde auf Millionen von Beispielproblemen aus verschiedenen mathematischen Disziplinen und Schwierigkeitsgraden trainiert. Das System verbesserte sich selbst, indem es versuchte, immer komplexere Aussagen zu beweisen, ähnlich wie AlphaZero durch das Spielen gegen sich selbst lernte.

AlphaGeometry 2 wurde entwickelt, um Geometrie-Probleme zu lösen. Hier ermöglichte Geminis Sprachverständnis dem KI-System, hilfreiche Hilfskonstruktionen vorherzusagen, während ein symbolischer Reasoning-Engine die logischen Deduktionen verwaltete. Dieser hybride Ansatz ermöglichte es AlphaGeometry, Geometrie-Probleme zu lösen, die weit über den Bereich traditioneller maschineller Argumentation hinausgingen.

Zusammen lösten diese Systeme vier von sechs IMO-Problemen: zwei in Algebra, eines in Zahlentheorie und eines in Geometrie, und erreichten eine Punktzahl von 28 von 42. Diese Leistung war ein bedeutender Meilenstein, da es das erste Mal war, dass eine KI die Silbermedaille bei der IMO erreicht hatte. Allerdings basierte dieser Erfolg stark auf menschlichen Experten, die Probleme in formale mathematische Sprachen übersetzten. Sie erforderten auch massive Rechenressourcen, die Tage der Verarbeitungszeit für jedes Problem benötigten.

Technische Innovationen hinter der Goldmedaille

DeepMinds Übergang von einer Silber- zu einer Goldmedaille wurde durch mehrere bedeutende technische Verbesserungen getrieben.

1. Natürliche Sprache als Medium für Beweise

Die bedeutendste Änderung war der Wechsel von Systemen, die Expertenübersetzungen in formale Sprachen erforderten, zu Systemen, die natürliche Sprache als Medium für Beweise behandelten. Dieser Wechsel wurde durch eine verbesserte Version von Gemini mit Deep-Think-Fähigkeiten erreicht. Anstatt Probleme in Lean zu übersetzen, verarbeitet das Modell den Text direkt, generiert informelle Skizzen, formalisiert interne kritische Schritte und produziert einen verfeinerten englischen Beweis. Reinforcement-Learning von menschlichem Feedback (RLHF) wurde verwendet, um Lösungen zu belohnen, die logisch konsistent, knapp und präsentabel waren.

Gemini Deep Think unterscheidet sich von der öffentlichen Version von Gemini in zwei Hauptaspekten. Erstens weist es längere Kontextfenster und mehr Rechentoken pro Abfrage zu, was es dem Modell ermöglicht, mehrseitige Denkprozesse aufrechtzuerhalten. Zweitens verwendet es paralleles Reasoning, bei dem Hunderte von spekulativen Threads für verschiedene potenzielle Lösungen generiert werden. Ein leichter Supervisor bewertet und fördert dann die vielversprechendsten Pfade, indem er Konzepte aus Monte-Carlo-Baum-Suche übernimmt, aber auf Text anwendet. Dieser Ansatz ahmt nach, wie menschliche Teams Ideen brainstormen, unproduktive Ideen verwerfen und sich auf elegante Lösungen konzentrieren.

2. Training und Reinforcement-Learning

Das Training von Gemini Deep Think umfasste die Feinabstimmung des Modells, um nächste Schritte vorherzusagen, anstatt endgültige Antworten. Zu diesem Zweck wurde ein Korpus von 100.000 hochwertigen Olympiad- und Hochschulwettbewerbslösungen zusammengestellt. Der Korpus wurde hauptsächlich aus öffentlichen Mathematik-Foren, arXiv-Preprints und College-Problem-Sätzen gesammelt. Menschliche Mentoren überprüften Trainingsbeispiele, um illogische oder unvollständige Beweise zu filtern. Reinforcement-Learning half, das Modell zu verfeinern, indem es es in Richtung präziser und knapper Beweise lenkte. Frühe Versionen produzierten übermäßig umfangreiche Beweise, aber Strafen für redundante Phrasen halfen, die Ausgabe zu kürzen.

Anders als herkömmliche Feinabstimmung, die oft mit sparsamen Belohnungen zu kämpfen hat, wo das Feedback binär ist, entweder ist der Beweis korrekt oder nicht. DeepMind implementierte ein schrittweises Belohnungssystem, bei dem jeder verifizierte Sub-Lemma zum Gesamtpunktestand beitrug. Dieses Belohnungssystem leitet Gemini, selbst wenn ein vollständiger Beweis selten ist. Der Trainingsprozess dauerte drei Monate und nutzte etwa 25 Millionen TPU-Stunden.

3. Massive Parallelisierung

Parallelisierung spielte auch eine entscheidende Rolle bei DeepMinds Fortschritt von Silber zu Gold. Jedes Problem generierte mehrere Reasoning-Branchen in Parallel, wobei Ressourcen dynamisch auf vielversprechendere Wege umgeschaltet wurden, wenn andere ins Stocken gerieten. Diese dynamische Planung war besonders vorteilhaft für Kombinatorik-Probleme, die große Lösungsräume haben. Der Ansatz ist ähnlich wie bei Menschen, die Hilfsungleichungen testen, bevor sie sich für eine vollständige Induktion entscheiden. Obwohl dieser Ansatz rechenintensiv war, war er mit DeepMinds TPU-v5-Clustern machbar.

DeepMind bei der IMO 2025

Um die Integrität des Wettbewerbs zu wahren, frierte DeepMind die Gewichte des Modells drei Wochen vor der IMO ein, um zu verhindern, dass offizielle Probleme in das Trainingsset gelangen. Sie filterten auch Daten heraus, die Lösungen für zuvor unveröffentlichte Olympiad-Fragen enthielten.

Während des Wettbewerbs erhielt Gemini Deep Think die sechs offiziellen Probleme im Klartext-Format, ohne Zugang zum Internet. Das System operierte auf einem Cluster, der so konfiguriert war, dass er die Rechenleistung eines Standard-Laptops pro Prozess simulieren konnte. Der gesamte Problemlösungsprozess wurde in weniger als drei Stunden abgeschlossen, gut innerhalb der Zeitbegrenzung. Die generierten Beweise wurden den IMO-Koordinatoren ohne Änderungen vorgelegt.

Gemini Deep Think erzielte perfekte Punktzahlen bei den ersten fünf Problemen. Das letzte Problem, ein herausforderndes Kombinatorik-Rätsel, überforderte jedoch sowohl die KI als auch 94 % der menschlichen Teilnehmer. Trotzdem beendete die KI den Wettbewerb mit einer Gesamtpunktzahl von 35/42 und sicherte sich die Goldmedaille. Diese Punktzahl war sieben Punkte höher als die Leistung des Vorjahres. Beobachter beschrieben die Beweise der KI später als “gründlich” und “vollständig”, wobei sie die strengen Begründungen hervorhoben, die von menschlichen Teilnehmern erwartet werden.

Auswirkungen auf KI und Mathematik

DeepMinds Erfolg ist ein bedeutender Meilenstein für sowohl KI als auch Mathematik. Für die KI ist das Beherrschen der IMO ein Schritt in Richtung künstlicher allgemeiner Intelligenz (AGI), bei der Systeme jede intellektuelle Aufgabe ausführen können, die ein Mensch kann. Das Lösen komplexer mathematischer Probleme erfordert Argumentation und Verständnis, die grundlegende Bestandteile der allgemeinen Intelligenz sind. Dieser Erfolg zeigt, dass die KI Fortschritte in Richtung menschlicher kognitiver Fähigkeiten macht.

Für die Mathematik können KI-Systeme wie Gemini Deep Think zu wertvollen Werkzeugen für Mathematiker werden. Sie können bei der Erforschung neuer Bereiche, der Überprüfung von Vermutungen und sogar der Entdeckung neuer Theoreme helfen. Indem die KI die eher mühsamen Aspekte der Beweiskonstruktion automatisiert, befreit sie menschliche Mathematiker, um sich auf höhere konzeptionelle Arbeiten zu konzentrieren. Darüber hinaus könnten die für diese KI-Systeme entwickelten Techniken neue Methoden in der mathematischen Forschung inspirieren, die möglicherweise nicht durch menschliche Anstrengungen allein erreicht werden können.

Allerdings wirft der Fortschritt der KI in der Mathematik auch Fragen über die Rolle der KI in Bildungseinrichtungen und Wettbewerben auf. Wenn die Fähigkeiten der KI weiter wachsen, wird es Debatten darüber geben, wie ihre Beteiligung die Natur der mathematischen Bildung und des Wettbewerbs verändern könnte.

Ausblick

Der Gewinn der Goldmedaille bei der IMO ist ein bedeutender Meilenstein, aber viele mathematische Herausforderungen bleiben für aktuelle KI-Systeme unerreichbar. Dennoch unterstreicht der schnelle Fortschritt von Silber zu Gold in nur einem Jahr das beschleunigte Tempo der KI-Innovationen und -Entwicklungen. Wenn dieser Trend anhält, könnten KI-Systeme bald einige der berühmtesten ungelösten mathematischen Probleme angehen. Während die Frage, ob die KI menschliche Kreativität ersetzen oder ergänzen wird, ungeklärt bleibt, ist die IMO 2025 ein klarer Hinweis darauf, dass die künstliche Intelligenz bedeutende Fortschritte in der logischen Argumentation gemacht hat.