- Le modèle Gemini Deep Think de Google DeepMind a atteint en 2025 le score correspondant à la médaille d’or à l’Olympiade internationale de mathématiques (IMO), avec 35 points
- Le modèle a résolu parfaitement 5 problèmes sur 6 et a été salué par le jury officiel de l’IMO pour la clarté et la précision de ses démonstrations mathématiques
- Il s’agit d’un bond majeur par rapport au niveau médaille d’argent de l’an dernier (28 points) obtenu par AlphaProof et AlphaGeometry 2 : le modèle comprend désormais les problèmes officiels en langage naturel et produit des démonstrations comme un humain en 4 h 30
- Le mode Deep Think applique la pensée parallèle (parallel thinking) et les techniques les plus récentes d’apprentissage par renforcement afin d’explorer et de combiner plusieurs pistes de résolution en même temps, avec une optimisation pour les problèmes de style IMO
- Google prévoit d’étendre sa collaboration avec les mathématiciens et de progresser vers le développement d’une prochaine génération d’AGI combinant raisonnement mathématique et vérification formelle
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- Gemini Deep Think de Google DeepMind a obtenu 35 points au total à l’IMO 2025 (5 problèmes sur 6 résolus parfaitement), atteignant ainsi officiellement le seuil de la médaille d’or
- Le jury officiel de l’IMO a particulièrement apprécié la clarté, la précision et l’accessibilité des solutions. Le président de l’IMO, le Prof. Dr. Gregor Dolinar, a publié une déclaration officielle affirmant : « Je confirme que Google DeepMind a atteint le score de 35 points correspondant à la médaille d’or »
- L’an dernier, AlphaGeometry et AlphaProof exigeaient que des experts traduisent les problèmes du langage naturel vers un langage spécialisé du domaine (Lean, etc.), et les calculs prenaient plus de deux jours. Cette année, Gemini a mené l’ensemble du processus en langage naturel, de la compréhension du problème à la rédaction de la preuve, dans le temps de l’épreuve de l’IMO (4 h 30)
Making the most of Deep Think mode
- Gemini Deep Think est un mode de raisonnement amélioré qui applique les techniques de recherche les plus récentes, notamment la pensée parallèle (parallel thinking), afin d’explorer simultanément plusieurs chemins de résolution et d’en tirer la meilleure solution
- Le modèle a été entraîné à l’aide de techniques d’apprentissage par renforcement pour résoudre des problèmes mathématiques complexes, ainsi que sur divers jeux de données de démonstrations de style IMO ; des indications générales et conseils sur l’approche des problèmes de l’IMO lui ont aussi été fournis
- Une version de test de ce modèle Deep Think sera d’abord proposée à certains mathématiciens et experts de confiance, avant une ouverture ultérieure aux abonnés Google AI Ultra
The Future of AI and Mathematics
- Google DeepMind poursuit sa collaboration avec la communauté mathématique tout en menant en parallèle des travaux fondés sur des systèmes formels, comme AlphaGeometry et AlphaProof, en plus du raisonnement en langage naturel
- À l’avenir, les IA combinant compréhension du langage naturel et capacité de raisonnement mathématique formel et vérifiable devraient devenir des outils clés pour les mathématiques, la science, l’ingénierie et la recherche
- DeepMind considère cette avancée comme une étape importante sur la voie de l’AGI (intelligence artificielle générale) et prévoit de s’attaquer à l’avenir à des problèmes mathématiques encore plus complexes et d’un niveau plus élevé
Vérification des réponses et position officielle de l’IMO
- Le comité d’organisation de l’IMO a officiellement confirmé que les réponses soumises constituaient des solutions complètes et exactes
- Il précise toutefois que l’examen mené par l’IMO ne couvre pas la validation du système, du processus ni du modèle de base lui-même
- Pour plus de détails et pour éviter toute interprétation excessive, il est possible de consulter la déclaration officielle de l’IMO (En savoir plus)
5 commentaires
OpenAI annonce avoir atteint un niveau médaille d’or à l’Olympiade internationale de mathématiques (IMO) 2025
OpenAI l’ayant annoncé en premier il y a deux jours, cela a un peu coupé l’élan, et certains disent aussi qu’Alexander Wei d’OpenAI a manqué d’étiquette en en parlant avant même d’en discuter avec l’IMO.
Comme cela a été annoncé alors que l’IMO ne l’avait pas encore reconnu officiellement, on lui reproche d’avoir éclipsé les félicitations et le mérite revenant aux participants humains, et non à l’IA.
Du coup, OAI a seulement fait valider cela par son propre panel, sans même recevoir la correction officielle de l’IMO. En plus, quand on voit que beaucoup estiment que la qualité des réponses de Gemini est un peu meilleure... j’ai l’impression que cela les met encore plus dans l’embarras. Ne prendre aucun risque pour sa réputation, annoncer le succès si ça marche (et encore, sans correction officielle), puis se retirer si le résultat est mauvais, c’est peut-être acceptable pour un benchmark, mais cela ne me semble pas être l’attitude appropriée à afficher dans une compétition où les participants concourent en engageant leur propre nom.
Même si les performances des LLM de Google et d’OpenAI se valent, c’est là qu’on voit la différence de maturité des entreprises.
Avis sur Hacker News
AlphaGeometry et AlphaProof passaient d’abord par une traduction des problèmes en langage naturel vers un langage spécialisé comme Lean, puis reconvertissaient les résultats de preuve en langage naturel, et le calcul prenait 2 à 3 jours ; le modèle Gemini de cette année a utilisé une approche end-to-end qui génère directement des preuves mathématiques à partir de l’énoncé officiel en langage naturel, ce qui signifie qu’il n’y a pas eu de traduction préalable vers Lean, mais on ne sait pas clairement s’il a utilisé en interne des outils comme Lean, la recherche sur Internet, une calculatrice ou Python ; OpenAI a indiqué que son propre modèle n’avait pas utilisé ce type d’outils, mais je ne sais pas si cela s’applique exactement à Gemini ; j’aimerais aussi connaître l’ordre de grandeur du calcul utilisé par les deux systèmes, donc du coût ; si le prix est énorme, cela signifie que ce n’est pas encore très pratique ; comme aucune information n’a encore été publiée, je suppose que c’est extrêmement cher ; et partage un lien confirmant « pas d’usage d’outils, pas de connexion Internet » https://x.com/FredZhang0/status/1947364744412758305
Le modèle Gemini de cette année génère des preuves mathématiques à partir de l’énoncé officiel en langage naturel uniquement, et tout s’est déroulé dans le temps de concours de 4,5 heures, sans utiliser d’outils externes
Officiellement, des outils de vérification formelle comme Lean ne sont pas utilisés pour résoudre concrètement les problèmes de l’IMO, mais je me demande s’ils sont utilisés dans le processus d’entraînement du modèle ; dans les travaux 2024 de Google sur l’IMO, il existe une technique qui convertit une preuve en langage naturel vers un langage formel pouvant être vérifié officiellement ; il me semble naturel d’exploiter cela pour l’entraînement RLVR (verification-reward via apprentissage par renforcement) ; si l’on pouvait traduire et vérifier tout le raisonnement produit par un LLM mathématique pour l’utiliser comme signal de récompense, ce signal deviendrait bien plus dense ; obtenir une preuve formelle parfaite resterait difficile, mais cela aiderait à éviter les raisonnements faux ou les phrases ininterprétables ; avec une quantité énorme de calcul, on pourrait même résoudre des problèmes du niveau IMO ; AlphaProof a déjà montré qu’en naviguant entre des preuves Lean et les sorties d’un LLM, on pouvait explorer efficacement l’espace de raisonnement et résoudre des problèmes de niveau IMO ; je me demande si, en supprimant l’étape intermédiaire et en apprenant au LLM à imiter le raisonnement formel via RLVR, on ne pourrait pas obtenir une efficacité et une capacité de résolution comparables
Je me demande aussi pourquoi ils n’utilisent pas Lean : est-ce que cela signifie qu’avec Lean, résoudre ce type de problème est désormais trop facile, ou bien est-ce que Lean constitue au contraire un frein ?
Je me demande si « pas d’usage d’outils, pas de connexion Internet » signifie réellement que cela pourrait fonctionner hors ligne, sans l’infrastructure de Google, donc éventuellement être déployé en local si besoin
On dit que cette année, une version avancée de Gemini a généré directement des preuves mathématiques à partir des énoncés officiels uniquement en langage naturel, mais je trouve au contraire un peu regrettable cet éloignement des techniques de formalisation ; si l’on veut vraiment automatiser les mathématiques, ou par exemple arriver à produire mécaniquement des preuves de plusieurs milliers de pages, je pense qu’il n’y a pas d’autre voie que la formalisation ; sinon il faudra toujours un relecteur humain, et il n’y aura aucun vrai moyen de faire confiance à la preuve
Si un LLM peut produire en langage naturel une preuve rigoureuse, alors prouver la même chose dans un langage formel comme Lean ne devrait pas être très difficile ; dans AlphaProof, l’usage de Lean était assez limité et spécialisé pour certains problèmes mathématiques précis ; en revanche, si l’on atteint le même résultat par approche RL et en langage naturel, cela pourrait s’étendre à des domaines variés où la vérification est plus délicate
Partage aussi le fait que DeepMind rassemble actuellement des dépôts où des problèmes officiellement non résolus sont formalisés et archivés https://github.com/google-deepmind/formal-conjectures
Je suis mathématicien, mais je ne fais plus de recherche, et je voudrais donner un peu de contexte sur la raison pour laquelle beaucoup de mathématiciens restent tièdes face aux méthodes formelles ; concrètement, pour produire des preuves de milliers de pages, c’est évidemment impossible sans formalisation, et je suis d’accord sur le fait que pour « faire confiance » à quelque chose, il faut une vérification formelle ; mais en pratique, ce que veulent vraiment les mathématiciens, c’est une explication du « pourquoi » ce résultat est vrai ; le vrai produit, ce n’est pas la réponse oui-non, mais son interprétation et sa raison d’être ; par exemple, tout le monde pense sans doute que l’hypothèse de Riemann est vraie, mais personne n’attend simplement la bonne réponse ; il existe même beaucoup de résultats du type « si l’hypothèse de Riemann est vraie, alors tel nouveau théorème s’ensuit » ; ce qu’on attend d’une preuve, c’est fondamentalement une intuition nouvelle ou une manière d’apporter une compréhension profonde de la théorie des nombres ; si un système comme Lean se contente de certifier formellement qu’une affirmation est vraie sans que les humains puissent même la comprendre, cela n’a presque aucun intérêt
Une formalisation exacte est plutôt plus facile que la résolution du problème lui-même, donc on peut aussi résoudre le problème d’abord, puis le formaliser ensuite pour vérification
Les problèmes de l’IMO sont, à l’origine, conçus pour être résolus par des humains sans outils ; si l’on demande au modèle de résoudre des problèmes plus difficiles, on pourra alors lui fournir suffisamment d’outils ; au minimum, reproduire d’abord les capacités humaines sans outils me semble une bonne direction
Quand on compare les réponses d’OpenAI et de Gemini, le style de rédaction de Gemini me paraît beaucoup plus clair ; la présentation pourrait être un peu meilleure, mais le contenu de la preuve lui-même est facile à suivre, et c’est composé de phrases plus courtes et mieux structurées que la réponse d’OpenAI
La preuve de Google est peut-être un résultat résumé a posteriori, et il est aussi possible qu’un mécanisme comme Tree of Thoughts fasse partie du processus de résumé ; cela ne ressemble pas à la simple conséquence d’un ordre passif et direct du type « donne la réponse finale »
Les résultats de preuve IMO mentionnés pour OpenAI et Google sont visibles respectivement dans le PDF des preuves Google et le repository d’exemples de preuves d’OpenAI
OpenAI comme Google ont insisté sur le fait que « tout le processus s’est terminé dans les 4,5 heures du concours », mais je doute de l’importance réelle de cette limite ; en pratique, ils ont très bien pu lancer simultanément des millions de processus de raisonnement parallèles pour trouver une preuve ; bien sûr, cela aurait aussi nécessité beaucoup de calcul pour un modèle d’évaluation chargé de juger les résultats et de choisir la preuve finale à soumettre ; cela a peut-être en réalité consommé des centaines d’années-GPU ; malgré tout, le fait que cette méthode trouve une solution, et qu’elle soit parallélisable à ce point, reste impressionnant ; qu’on atteigne ou non l’AGI via davantage de calcul, le cerveau humain ne se met pas à l’échelle aussi facilement, donc la portée du résultat est évidente
Il est très intéressant de voir le passage, par rapport au système spécialisé Lean de l’an dernier, à un LLM généraliste en langage naturel + RL ; je m’attends à ce que cette approche améliore aussi les performances au-delà des compétitions de mathématiques ; j’ai hâte de voir jusqu’où cela pourra s’étendre à l’avenir, et ce système ne semble pas non plus très différent du modèle/de la fonctionnalité « DeepThink » qui doit être publié cet été
J’ai l’impression qu’on vit en ce moment un moment à la Deep Blue contre Kasparov dans la compétition mathématique avec les machines ; les progrès par rapport à il y a seulement quelques années sont énormes, mais on est encore très loin d’un véritable mathématicien IA ; malgré tout, c’est une époque vraiment incroyable
Dans un podcast récent, Terrence Tao s’est lui aussi montré très intéressé par le travail avec ce type d’outils ; il a expliqué que, pour le moment, le meilleur usage consistait sans doute à ce qu’un humain fixe les idées ou les paramètres, pendant que le LLM explore en parallèle et tente des preuves ; l’analogie avec les moteurs d’échecs est pertinente : autrefois, même les meilleurs joueurs d’échecs s’appuyaient sur des équipes d’experts pour l’analyse, alors qu’aujourd’hui, des supercalculateurs et des logiciels analysent un grand nombre de positions, en extraient les meilleures idées et les transmettent au joueur
Je pense que cela ressemble davantage à Deep Blue affrontant un enfant prodige, car les participants à l’IMO ne sont pas des mathématiciens de rang mondial, mais des lycéens
La différence ici, c’est qu’un simple brute force ne suffit pas à obtenir un score élevé dans le temps imparti ; c’est une véritable étape technique, différente du « possible en principe » de l’époque de Deep Blue
Le problème 6 m’intrigue : ni OpenAI ni DeepMind n’ont réussi à fournir de réponse ; les humains arrivent pourtant à produire au moins des solutions partielles, donc il est étrange que l’IA n’ait rien ; je me demande si le LLM a lui-même compris qu’il n’avait pas réussi à résoudre le problème ; l’une des limites des LLM est qu’ils « ne savent pas qu’ils ne savent pas », et dans ce cas il me semble presque impossible de vérifier la cohérence logique sans solveur
Il est probable qu’il n’ait simplement pas fini de « réfléchir » dans le temps imparti du concours, et qu’il ne soit jamais passé à l’étape de « sortie »
Cette limite ne concerne que la génération de texte des LLM préentraînés les plus basiques ; on peut aussi entraîner un linear probe (une simple couche de réseau de neurones) pour produire un score de confiance ; bien sûr, ce ne sera pas fiable à 100 %, mais dans un domaine limité comme les mathématiques, cela pourrait tout de même devenir assez crédible
Sans outil de vérification formelle, l’usage réel peut encore être très risqué ; l’ancien o3, même s’il n’est plus le plus récent, était déjà bon pour trouver des références et proposer de nouvelles inégalités ; mais au stade de la preuve, il pouvait fournir des réponses apparemment convaincantes tout en contenant des affirmations fausses dans les détails ou des erreurs algébriques ; plus les modèles s’améliorent, plus ce type d’erreurs subtiles risque paradoxalement d’être difficile à détecter
Je me demande pourquoi ils insistent sur le fait qu’ils n’ont pas utilisé de démonstrateur de théorèmes ; après tout, n’est-il pas préférable d’utiliser n’importe quel outil qui améliore les performances du modèle ? D’autant plus que Gemini a lui aussi été spécialisé pour l’IMO ; le modèle a été entraîné par apprentissage par renforcement sur des données de raisonnement multi-étapes / résolution de problèmes / démonstration de théorèmes, et on lui a aussi fourni des recueils de solutions mathématiques de haute qualité ainsi que des indices sur la manière d’aborder les problèmes de l’IMO
J’imagine que la « version avancée de Gemini DeepThink » est en réalité différente du DeepThink qui sera intégré au produit sur abonnement Gemini Ultra lors de sa sortie, ou bien qu’elle a utilisé beaucoup plus de calcul au moment du test ; quoi qu’il en soit, c’est amusant de voir OpenAI et Google se disputer ce terrain
Je vais partager le lien vers le system prompt de context engineering qui résout les problèmes 1 à 6 en entier ; il suffit de l’utiliser avec o3 ou Gemini 2.5, d’insérer tout le prompt puis de lui demander de résoudre le problème. https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf