- Das Modell Gemini Deep Think von Google DeepMind hat bei der Internationalen Mathematik-Olympiade (IMO) 2025 die Goldmedaillen-Punktzahl (35 Punkte) erreicht
- Das Modell löste 5 von 6 Aufgaben vollständig und erhielt von der offiziellen IMO-Jury Anerkennung für klare und präzise mathematische Lösungswege
- Gegenüber dem Vorjahresniveau von AlphaProof·AlphaGeometry 2 mit Silbermedaille (28 Punkte) ist dies ein großer Sprung: Es versteht offizielle Aufgaben in natürlicher Sprache und vervollständigt Beweise innerhalb von 4,5 Stunden wie ein Mensch
- Der Deep-Think-Modus nutzt paralleles Denken (parallel thinking) und aktuelles Reinforcement Learning, um mehrere Lösungswege gleichzeitig zu erkunden und zusammenzuführen, und ist damit für das Lösen von Problemen im IMO-Stil optimiert
- Google plant, die Zusammenarbeit mit Mathematikern auszuweiten und auf die Entwicklung einer nächsten AGI-Generation hinzuarbeiten, die mathematisches Schlussfolgern mit formaler Verifikation verbindet
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- Gemini Deep Think von Google DeepMind erhielt bei der Internationalen Mathematik-Olympiade (IMO) 2025 insgesamt 35 Punkte (5 von 6 Aufgaben vollständig gelöst) und erreichte damit offiziell das Goldmedaillen-Niveau
- Die offizielle IMO-Jury bewertete insbesondere Klarheit, Präzision und gut verständliche Lösungsdarstellungen hoch, und der IMO-Vorsitzende Prof. Dr. Gregor Dolinar veröffentlichte eine offizielle Erklärung mit den Worten: „Google DeepMind hat die Gold-Punktzahl von 35 Punkten erreicht“
- Im vergangenen Jahr mussten bei AlphaGeometry·AlphaProof Experten die Aufgaben von natürlicher Sprache in domänenspezifische Sprachen (wie Lean) übersetzen, und die Berechnungen dauerten mehr als zwei Tage. In diesem Jahr absolvierte Gemini den gesamten Prozess von der Aufgabenverständnis bis zur Beweisausarbeitung auf Basis natürlicher Sprache innerhalb der IMO-Wettbewerbszeit (4,5 Stunden)
Making the most of Deep Think mode
- Gemini Deep Think ist ein verbesserter Inferenzmodus, der aktuelle Forschungstechniken wie paralleles Denken (parallel thinking) anwendet und mehrere Lösungswege gleichzeitig untersucht, um die beste Lösung zu finden
- Das Modell wurde mit Reinforcement-Learning-Verfahren zur Lösung komplexer mathematischer Probleme sowie mit verschiedenen Beweisdaten im IMO-Stil trainiert; zusätzlich wurden allgemeine Hinweise und Tipps zum Vorgehen bei IMO-Aufgaben eingebracht
- Diese Deep-Think-Version soll zunächst vertrauenswürdigen Mathematikern und Fachleuten als Testversion bereitgestellt werden und später für Abonnenten von Google AI Ultra verfügbar werden
The Future of AI and Mathematics
- Google DeepMind setzt die Zusammenarbeit mit der Mathematik-Community fort und verfolgt neben sprachbasiertem Schlussfolgern auch weiterhin forschungsbasierte Arbeiten in formalen Systemen wie AlphaGeometry·AlphaProof
- Künftig dürften AIs, die Sprachverständnis mit formalem und verifizierbarem mathematischem Schlussfolgern verbinden, zu zentralen Werkzeugen in Mathematik, Naturwissenschaft, Technik und Forschung werden
- DeepMind bewertet diesen Erfolg als wichtigen Fortschritt auf dem Weg zu AGI (Artificial General Intelligence) und plant, sich künftig noch komplexeren und anspruchsvolleren mathematischen Problemen zu stellen
Verifikation der Antworten und die offizielle Position der IMO
- Das IMO-Organisationskomitee hat offiziell bestätigt, dass die eingereichten Antworten vollständige und korrekte Lösungen sind
- Es stellt jedoch klar, dass die IMO-Prüfung keine Verifikation des Systems, des Prozesses oder des zugrunde liegenden Modells selbst umfasst
- Weitere Details und den genauen Wortlaut finden Sie in der offiziellen IMO-Erklärung (Mehr dazu)
5 Kommentare
OpenAI kündigt Leistungen auf Goldmedaillen-Niveau bei der Internationalen Mathematik-Olympiade (IMO) 2025 an
Da OpenAI das schon vor zwei Tagen zuerst angekündigt hatte, war ein wenig die Luft raus; man hörte aber auch Stimmen, dass es unhöflich gewesen sei, dass OpenAIs Alexander Wei dies ohne jede Absprache mit der IMO vorab öffentlich gemacht habe.
Da es von Seiten der IMO noch nicht einmal offiziell anerkannt worden war, habe man es trotzdem angekündigt und damit den Glückwünschen und Verdiensten der normalen Teilnehmerinnen und Teilnehmer statt der KI die Show gestohlen.
Dadurch hat OAI es letztlich nur durch ein eigenes Panel verifizieren lassen und die IMO hat es nicht einmal offiziell bewertet. Wenn man außerdem sieht, dass viele die Qualität der Antworten von Gemini für etwas besser halten, wirkt die Situation für sie nur noch peinlicher. Kein Reputationsrisiko eingehen, im Erfolgsfall veröffentlichen (noch dazu ohne offizielle Bewertung), und wenn das Ergebnis schlecht ist, einen Rückzieher machen — bei Benchmarks mag so etwas noch angehen, aber bei einem Wettbewerb, in dem die Teilnehmer unter ihrem eigenen Namen antreten, scheint mir das nicht das richtige Verhalten zu sein.
Auch wenn sich Google und OpenAI bei der LLM-Leistung kaum etwas nehmen, zeigt sich hier der Unterschied in der unternehmerischen Erfahrung.
Hacker-News-Meinungen
AlphaGeometry und AlphaProof gingen so vor, dass sie Probleme in natürlicher Sprache zunächst in eine domänenspezifische Sprache wie Lean übersetzten und die Beweisergebnisse anschließend wieder in natürliche Sprache zurückverwandelten; zudem dauerte die Berechnung 2–3 Tage. Das diesjährige Gemini-Modell verwendete hingegen einen End-to-End-Ansatz, der mathematische Beweise direkt aus der offiziellen Aufgabenbeschreibung in natürlicher Sprache erzeugte, also nicht erst nach Lean übersetzte. Unklar ist allerdings, ob intern Tools wie Lean, Internetsuche, Taschenrechner oder Python verwendet wurden. OpenAI sagte, dass das eigene Modell solche Werkzeuge nicht genutzt habe, aber ich weiß nicht, ob diese Aussage auch exakt auf Gemini zutrifft. Ich würde außerdem gern die ungefähre Größenordnung des verwendeten Compute, also der Kosten, für beide Systeme kennen. Falls der Preis enorm ist, bedeutet das, dass die praktische Nutzbarkeit noch gering ist. Da es dazu noch keine veröffentlichten Informationen gibt, vermute ich, dass es extrem teuer war. Dazu wurde auch ein Link geteilt, der bestätigt, dass „keine Tool-Nutzung, keine Internetverbindung“ vorlag: https://x.com/FredZhang0/status/1947364744412758305
Das diesjährige Gemini-Modell erzeugt mathematische Beweise direkt aus den offiziellen Aufgabenbeschreibungen allein in natürlicher Sprache, und der gesamte Prozess lief innerhalb der Wettbewerbszeit von 4,5 Stunden ab. Externe Tools wurden nicht verwendet.
Offiziell heißt es, dass formale Verifikationswerkzeuge wie Lean beim tatsächlichen Lösen von IMO-Problemen nicht verwendet werden, aber ich frage mich, ob sie im Trainingsprozess des Modells eingesetzt werden. In Googles IMO-Forschung von 2024 gibt es eine Technik, natürliche Beweise in formal verifizierbare Formsprachen zu überführen. Ich halte es für den naheliegenden nächsten Schritt, dies für RLVR-Training (Verification-as-Reward durch Reinforcement Learning) zu nutzen. Wenn sich jede von einem Mathematik-LLM erzeugte Argumentation übersetzen und verifizieren ließe, um sie als Belohnungssignal zu verwenden, wäre das Belohnungssignal viel dichter. Perfekte formale Beweise zu erhalten wäre weiterhin schwierig, aber es wäre nützlich, um falsche Argumentationsschritte oder unentzifferbare Sätze zu vermeiden. Mit enormem Compute dürfte damit selbst Probleme auf IMO-Niveau lösbar werden. Systeme wie AlphaProof haben bereits gezeigt, dass sich der Suchraum effizient durchsuchen lässt, wenn man zwischen Lean-Beweisen und LLM-Ausgaben hin- und herwechselt. Wenn man den Zwischenschritt auslässt und dem LLM per RLVR beibringt, formale Schlussfolgerungen nachzuahmen, könnte man vielleicht ähnliche Effizienz und Problemlösungsfähigkeit erreichen.
Ich frage mich auch, warum man Lean nicht verwendet. Bedeutet das, dass das Lösen der Aufgaben mit Lean heutzutage zu einfach wäre, oder ist Lean selbst eher ein Hindernis?
Ich frage mich, ob „keine Tool-Nutzung, keine Internetverbindung“ in der Praxis bedeutet, dass das System ohne Google-Infrastruktur offline laufen könnte, also ob es bei Bedarf lokal ausgerollt werden kann.
Es heißt zwar, dass das fortgeschrittene Gemini-Modell dieses Jahr mathematische Beweise direkt aus offiziellen Aufgabenbeschreibungen allein in natürlicher Sprache erzeugt habe, aber ich finde es eher bedauerlich, wenn man sich von Formalisierungstechniken entfernt. Wenn man Mathematik wirklich automatisieren oder etwa maschinell Beweise von tausenden Seiten erzeugen will, gibt es meiner Meinung nach keinen anderen Weg als Formalisierung. Andernfalls braucht man immer noch menschliche Gutachter, und es gibt keine echte Möglichkeit, einem Beweis wirklich zu vertrauen.
Wenn ein LLM in natürlicher Sprache einen strengen Beweis erzeugen kann, dann dürfte auch ein Beweis in einer formalen Sprache wie Lean keine große Schwierigkeit sein. Der Einsatz von Lean bei AlphaProof war ziemlich begrenzt und auf bestimmte mathematische Problemtypen spezialisiert. Wenn man dagegen mit RL und natürlicher Sprache dasselbe erreicht, lässt sich das auch auf verschiedene Bereiche ausweiten, in denen Verifikation schwierig ist.
Es wurde auch darauf hingewiesen, dass DeepMind derzeit ein Repository sammelt, in dem formalisierte offene Probleme dokumentiert werden: https://github.com/google-deepmind/formal-conjectures
Ich bin Mathematiker, forsche aber nicht mehr, und möchte etwas Kontext dazu geben, warum viele Mathematiker formalen Methoden eher zurückhaltend gegenüberstehen. Praktisch gesehen ist es natürlich unmöglich, Beweise von tausenden Seiten ohne Formalisierung zu erstellen, und ich stimme zu, dass man etwas formell verifizieren muss, wenn man ihm wirklich „vertrauen“ will. Aber was Mathematiker tatsächlich wissen wollen, ist eine Erklärung dafür, „warum“ ein Resultat wahr ist. Das eigentliche Produkt ist nicht die Ja-Nein-Antwort, sondern ihre Interpretation und Begründung. Beim Riemann-Hypothese etwa glauben viele vermutlich, dass sie wahr ist, aber niemand wartet bloß auf das richtige Ja oder Nein. Es gibt sogar viele Resultate der Form „Wenn die Riemann-Hypothese wahr ist, dann gilt dieser neue Satz“. Was man sich von einem Beweis erhofft, ist im Kern neue Einsicht oder eine tiefere Art, Zahlentheorie zu verstehen. Wenn Lean nur formal verifiziert, dass etwas stimmt, Menschen es aber nicht einmal nachvollziehen können, dann hat das fast keinen Wert.
Exakte Formalisierung ist eher leichter als das eigentliche Lösen des Problems, daher kann man ein Problem zuerst lösen und es anschließend formalisieren, um das Ergebnis zu prüfen.
IMO-Probleme sind von vornherein so konzipiert, dass Menschen sie ohne Werkzeuge lösen. Wenn man Modelle schwierigere Probleme lösen lassen will, kann man ihnen dann durchaus ausreichend Tools geben. Zumindest zunächst Fähigkeiten auf Menschenniveau ohne Tools zu reproduzieren, halte ich für einen guten Ansatz.
Wenn man die Antworten von OpenAI und Gemini vergleicht, wirkt der Schreibstil von Gemini deutlich klarer. Die Präsentation könnte zwar noch besser sein, aber der Beweisinhalt selbst ist leicht nachzuvollziehen und besteht aus kürzeren, geordneteren Sätzen als die Antwort von OpenAI.
Googles Beweis könnte auch eine nachträgliche Zusammenfassung des Ergebnisses sein, und es ist möglich, dass der Zusammenfassungsprozess Teil eines Mechanismus wie Tree of Thoughts ist. Es wirkt jedenfalls nicht wie das bloße Resultat eines einfachen, passiven Befehls vom Typ „gib die Endantwort aus“.
Die erwähnten IMO-Beweisergebnisse von OpenAI und Google sind hier zu sehen: Google-Beweis-PDF und OpenAIs Repository mit Beweisbeispielen
Sowohl OpenAI als auch Google betonten, dass „der gesamte Prozess innerhalb der 4,5 Stunden des Wettbewerbs abgeschlossen wurde“, aber ich frage mich, ob diese Begrenzung wirklich eine wichtige Bedeutung hat. Im Grunde hätten sie vielleicht Millionen paralleler Denkprozesse gleichzeitig laufen lassen können, um einen Beweis zu finden. Natürlich würde das dann auch für ein Bewertungsmodell, das die Ergebnisse evaluiert und den schließlich einzureichenden Beweis auswählt, viel Compute erfordern. Tatsächlich könnten Hunderte Jahre GPU-Zeit hineingeflossen sein. Trotzdem ist es bemerkenswert, dass diese Art von Vorgehen überhaupt eine Lösung findet und dass Parallelisierung in diesem Ausmaß möglich ist. Ob man AGI am Ende nun mit mehr Compute erreicht oder nicht: Das menschliche Gehirn skaliert nicht so leicht, daher ist die Bedeutung des Ergebnisses klar.
Ich finde es sehr interessant, dass der Ansatz vom Lean-spezialisierten System des letzten Jahres zu einem auf natürlicher Sprache basierenden allgemeinen LLM + RL gewechselt ist. Ich erwarte, dass dieser Ansatz auch außerhalb des Bereichs mathematischer Wettbewerbe zu Leistungsverbesserungen beitragen wird. Ich bin gespannt, wie weit sich das künftig ausdehnen lässt. Außerdem scheint sich dieses System nicht stark von dem Modell bzw. der Funktion „DeepThink“ zu unterscheiden, das bzw. die im Sommer veröffentlicht werden soll.
Im Moment fühlt es sich an, als würden wir in der Mathematik-Konkurrenz zwischen Mensch und Maschine einen Moment wie zu Zeiten von Deep Blue und Kasparow erleben. Gegenüber vor nur wenigen Jahren gab es enorme Fortschritte, aber ich denke immer noch, dass wir von einem wirklich brauchbaren KI-Mathematiker weit entfernt sind. Trotzdem leben wir in einer bemerkenswerten Zeit.
In einem aktuellen Podcast zeigte auch Terrence Tao großes Interesse daran, mit solchen Tools zu arbeiten. Er sagte, dass die beste Nutzung in nächster Zeit wohl darin bestehen werde, dass Menschen Ideen oder Parameter vorgeben und LLMs dann Exploration, Beweise usw. parallel ausprobieren. Auch die Schachengine-Analogie passt gut: Früher wurden selbst Top-Schachspieler von Teams aus Experten bei der Analyse unterstützt, heute analysieren Supercomputer und Software unzählige Stellungen und liefern dem Spieler die besten Ideen.
Ich denke eher, dass es näher an Deep Blue gegen ein Wunderkind ist. IMO-Teilnehmer sind schließlich keine weltberühmten Mathematiker, sondern Gymnasiasten.
Der Unterschied hier ist, dass man allein mit einfachem Brute Force in der verfügbaren Zeit keine hohe Punktzahl erreichen kann. Das ist ein echter technischer Meilenstein und nicht wie bei Deep Blue bloß „prinzipiell möglich“.
Aufgabe 6 ist merkwürdig: Weder OpenAI noch DeepMind konnten eine Antwort liefern. Menschen geben zumindest Teilantworten, aber bei KI ist gar keine Antwort seltsam. Man fragt sich, ob ein LLM vielleicht selbst erkannt hat, dass es beim Lösen gescheitert ist. Eine der Grenzen von LLMs ist ja, dass sie „nicht wissen, dass sie etwas nicht wissen“, und dann scheint es fast unmöglich zu sein, ohne Solver die logische Konsistenz zu überprüfen.
Wahrscheinlich lag es daran, dass innerhalb der Wettbewerbszeit das „Denken“ nicht abgeschlossen wurde und der Prozess deshalb gar nicht erst in die „Ausgabe“-Phase überging.
Diese Grenze gilt nur für die grundlegendste Textgenerierung eines vortrainierten LLM. Zusätzlich könnte man einen linear probe, also eine einfache neuronale Netzwerkschicht, trainieren, um einen Confidence Score auszugeben. Natürlich wäre das nicht zu 100 % verlässlich, aber zumindest in einem begrenzten Bereich wie Mathematik könnte es durchaus recht vertrauenswürdig sein.
Ohne formale Verifikationswerkzeuge könnte der praktische Einsatz weiterhin riskant sein. Auch das ältere o3 war zwar nicht mehr ganz aktuell, hatte aber Stärken beim Finden von Referenzen und beim Vorschlagen neuer Ungleichungen. Im eigentlichen Beweisschritt konnte es jedoch Antworten liefern, die überzeugend wirkten, aber im Detail falsche Aussagen oder algebraische Fehler enthielten. Je besser Modelle werden, desto schwerer könnte es sogar werden, solche subtilen Fehler zu entdecken.
Ich frage mich, warum sie so betonen, dass kein Theorembeweiser verwendet wurde. Sollte man nicht jedes Tool nutzen, das die Modellleistung verbessert? Außerdem wurde auch Gemini in einer Weise spezialisiert, die auf IMO abgestimmt war: Das Modell wurde mit Reinforcement Learning auf mehrstufiges Schlussfolgern, Problemlösen und Theorembeweisdaten trainiert, und es bekam hochwertige Sammlungen mathematischer Musterlösungen sowie Hinweise auf Herangehensweisen an IMO-Probleme.
Ich vermute, dass die „fortgeschrittene Version von Gemini DeepThink“ in Wirklichkeit anders ist als das DeepThink, das in das kommende Gemini-Ultra-Abonnementprodukt integriert wird, oder dass dafür deutlich mehr Test-Time-Compute eingesetzt wurde. Trotzdem macht es Spaß zu beobachten, wie OpenAI und Google miteinander konkurrieren.
Ich teile den Link zum Context-Engineering-Systemprompt, mit dem alle Probleme 1 bis 6 gelöst wurden. Man kann ihn mit o3 oder Gemini 2.5 verwenden: Einfach den gesamten Prompt einfügen, die Frage eingeben und darum bitten, die Probleme zu lösen. https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf