Gemini atteint le niveau de l’or à l’IMO, une avancée majeure en mathématiques

Résoudre un problème d’olympiade ne consiste pas à écrire le bon nombre au bas d’une feuille. Il faut trouver une idée, choisir les bons outils, puis construire une démonstration que d’autres mathématiciens pourront vérifier ligne à ligne. C’est sur ce terrain particulièrement exigeant que Google DeepMind annonce une avancée : une version avancée de Gemini Deep Think a atteint le niveau d’une médaille d’or à l’Olympiade internationale de mathématiques 2025, avec 35 points sur 42.

L’annonce, publiée le 21 juillet 2025, marque un jalon pour les systèmes d’intelligence artificielle de raisonnement. Gemini a résolu cinq des six problèmes proposés aux candidats et ses démonstrations, formulées en langage naturel, ont été examinées par des correcteurs de l’IMO. Cette réussite ne signifie pas qu’une IA remplace un chercheur en mathématiques. Elle montre en revanche qu’un modèle peut désormais produire, dans certains cas très encadrés, des raisonnements formels assez solides pour satisfaire les critères d’une compétition internationale de très haut niveau.

Un score d’or, pas une médaille remise à une machine

L’Olympiade internationale de mathématiques, plus connue sous son sigle anglais IMO, est le concours mondial de mathématiques destiné aux élèves du secondaire les plus avancés. Chaque délégation nationale y sélectionne ses meilleurs candidats. Les épreuves couvrent notamment l’algèbre, la combinatoire, la géométrie et la théorie des nombres.

Le format explique l’importance de la performance de Gemini. L’examen comporte six problèmes, chacun noté sur sept points, pour un total de 42 points. Les candidats disposent de deux séances de 4 h 30. Une réponse juste mais dépourvue de justification ne suffit pas : l’essentiel de la note dépend de la qualité de la preuve, de la clarté des étapes et de l’absence de faille logique.

Gemini n’a pas participé au concours comme le ferait un élève et ne reçoit donc pas une médaille au sens administratif du terme. Google DeepMind emploie plus précisément l’expression de niveau médaille d’or. Les solutions produites par le système ont été soumises à l’évaluation de coordinateurs de l’IMO, qui ont confirmé le score de 35 points.

Pourquoi l’IMO est un test si difficile pour une IA

Les grands modèles de langage sont déjà capables de répondre à de nombreuses questions scolaires, parfois avec une rapidité impressionnante. Mais les problèmes de l’IMO demandent autre chose qu’une restitution de connaissances ou l’application d’une formule connue. Ils sont courts dans leur formulation, mais exigent souvent une idée inattendue : identifier une invariance, construire un contre-exemple, transformer une figure géométrique ou exploiter une propriété arithmétique discrète.

Cette difficulté est amplifiée pour une IA. Un modèle peut produire un texte qui a l’apparence d’une preuve tout en contenant un saut logique, une hypothèse oubliée ou une généralisation abusive. En mathématiques, une seule étape injustifiée peut invalider toute la démonstration. Les systèmes doivent donc maintenir une cohérence sur de nombreuses étapes, vérifier les contraintes de l’énoncé et choisir des concepts adaptés au niveau du concours.

Le recours au langage naturel est également notable. Les systèmes spécialisés en démonstration automatique travaillent souvent avec des langages formels très stricts, utilisés par des logiciels de vérification de preuves. Gemini a, lui, dû exprimer ses solutions sous une forme lisible par des humains, proche de celle attendue d’un candidat. C’est une capacité utile, car les mathématiciens ne travaillent pas uniquement avec des notations formelles : ils échangent aussi des intuitions, des brouillons et des démonstrations rédigées.

L’enjeu du raisonnement long et structuré

Google DeepMind attribue une partie de ce résultat à l’évolution de ses méthodes d’entraînement. Les approches classiques d’apprentissage par renforcement peuvent récompenser un modèle lorsqu’il atteint la bonne réponse finale. Cette méthode est efficace pour certains exercices, mais elle peut laisser de côté le chemin suivi pour y parvenir.

Or, pour les mathématiques de compétition, le chemin compte. Un raisonnement incomplet peut parfois tomber par chance sur le bon résultat sans fournir une preuve valable. Luong, cité à propos de ces travaux, souligne cette limite : des modèles capables d’atteindre une bonne réponse ne disposent pas nécessairement d’une argumentation assez complète pour convaincre un correcteur.

L’approche mise en avant pour Gemini vise donc à valoriser des réponses plus longues et détaillées. Dans les grandes lignes, l’apprentissage par renforcement consiste à faire produire plusieurs tentatives à un modèle, puis à favoriser les comportements qui mènent aux meilleures évaluations. Appliqué à des solutions mathématiques rédigées, ce principe peut encourager l’IA à expliciter les étapes intermédiaires, à développer une preuve cohérente et à corriger une piste qui aboutit à une contradiction.

Il ne faut pas imaginer pour autant une recette universelle. Une démonstration longue n’est pas automatiquement une bonne démonstration, et une solution élégante peut être très courte. L’enjeu est plutôt de donner au modèle la capacité de consacrer davantage d’effort à un problème difficile, sans s’arrêter à une réponse plausible mais fragile.

Une solution élémentaire plutôt qu’un détour avancé

L’un des exemples mis en avant par les chercheurs illustre ce point. Sur une épreuve, des compétiteurs humains ont mobilisé un théorème de Dirichlet, une notion considérée comme plus avancée que ce qui était attendu pour le concours. Gemini a emprunté une voie différente : il a bâti une preuve complète et indépendante à partir d’outils plus élémentaires de théorie des nombres.

Ce choix est intéressant à deux titres. D’abord, il suggère que le modèle n’a pas seulement reproduit une référence sophistiquée : il a trouvé une manière de respecter le niveau mathématique approprié au problème. Ensuite, une preuve fondée sur des résultats élémentaires est plus facile à examiner dans le cadre d’une olympiade, où les solutions doivent rester accessibles aux connaissances visées par la compétition.

Junehyuk Jung, chercheur chez Google DeepMind et professeur à l’université Brown, a fait part de son enthousiasme devant cette capacité à résoudre le problème de façon inventive. Cela ne permet pas, à lui seul, de conclure que l’IA possède une compréhension humaine des mathématiques. Mais l’exemple montre pourquoi l’évaluation ne se réduit pas à compter les bonnes réponses : la nature de la preuve produite compte elle aussi.

De l’argent en 2024 à l’or en 2025

La performance de 2025 s’inscrit dans une progression rapide des travaux de DeepMind sur les olympiades. En 2024, le laboratoire avait associé ses systèmes AlphaProof et AlphaGeometry 2 pour atteindre le niveau d’une médaille d’argent, avec 28 points sur 42. Un an plus tard, Gemini Deep Think franchit le seuil de l’or annoncé par Google DeepMind.

La comparaison doit être maniée avec prudence. Les problèmes changent chaque année et la performance ne se résume pas à un unique indicateur. Elle donne néanmoins une mesure concrète de l’ampleur du progrès revendiqué : sept points supplémentaires sur une échelle de 42, soit l’équivalent d’un problème entièrement résolu.

Cette évolution reflète aussi un changement de direction dans l’IA mathématique. Les programmes les plus spécialisés peuvent être extrêmement puissants sur une famille de problèmes ou dans un langage formel donné. Les modèles de langage généralistes, eux, ont l’avantage de pouvoir lire des énoncés ordinaires, discuter des pistes de résolution et rédiger des explications. Le défi consiste à leur apporter la rigueur qui a longtemps fait défaut à leurs réponses.

Quelles applications pour la recherche et l’éducation ?

Un système capable de rédiger des preuves de niveau olympiade pourrait devenir un assistant précieux pour les scientifiques. En recherche, il pourrait aider à explorer des cas particuliers, proposer des reformulations, détecter une étape manquante dans un raisonnement ou comparer plusieurs stratégies. L’intérêt ne se limite pas aux mathématiques pures : la physique théorique, l’informatique, l’ingénierie ou certaines branches de la biologie utilisent elles aussi des raisonnements complexes et des structures formelles.

Dans l’éducation, un tel outil pourrait accompagner un élève face à un exercice difficile, à condition de privilégier l’explication plutôt que la délivrance immédiate d’une solution. Montrer pourquoi une piste échoue, proposer un indice progressif ou présenter deux démonstrations différentes peut avoir une valeur pédagogique réelle. Mais l’usage doit rester encadré : une IA qui donne une solution complète trop tôt peut empêcher l’apprentissage de l’effort de recherche, central dans les mathématiques.

Les concurrents de Google DeepMind, dont Meta et d’autres laboratoires, investissent eux aussi dans des modèles capables de raisonner plus longtemps et plus rigoureusement. La compétition porte désormais moins sur la capacité à produire du texte fluide que sur l’aptitude à résoudre des problèmes nouveaux, à vérifier ses propres résultats et à justifier clairement ses conclusions.

Les limites d’un résultat spectaculaire

La performance de Gemini est impressionnante, mais elle ne doit pas être interprétée comme la preuve qu’une intelligence artificielle est devenue un mathématicien autonome. Une olympiade propose un corpus très particulier : des problèmes courts, soigneusement conçus, avec des règles de notation claires. La recherche mathématique, elle, demande souvent de formuler soi-même les bonnes questions, de travailler pendant des mois sur une conjecture et de juger si un résultat ouvre une piste réellement nouvelle.

La fiabilité reste l’autre enjeu majeur. Même lorsqu’un système fournit une preuve convaincante, celle-ci doit être relue par des experts ou vérifiée à l’aide d’outils formels lorsque les conséquences sont importantes. Les modèles de langage peuvent encore inventer une référence, confondre des hypothèses proches ou présenter avec assurance une conclusion erronée. Leur prose fluide rend ces erreurs parfois difficiles à repérer pour un lecteur non spécialiste.

Enfin, les conditions d’évaluation doivent être transparentes. Le score de Gemini a été vérifié par des coordinateurs de l’IMO, ce qui renforce la crédibilité de l’annonce. Pour comparer durablement les systèmes entre eux, la communauté devra néanmoins disposer de protocoles précis : outils autorisés ou non, durée réelle de calcul, nombre de tentatives, accès éventuel à des données externes et modalités de correction.

Ce qu’il faut surveiller après cette avancée

La question décisive n’est plus seulement de savoir si une IA peut résoudre quelques problèmes d’exception. Il faudra observer si ces capacités de raisonnement se généralisent à d’autres domaines, si elles restent robustes face à des énoncés inédits et si elles peuvent être contrôlées par des méthodes de vérification fiables.

Les prochaines étapes pourraient concerner l’association entre modèles de langage et logiciels de preuve formelle, capables de certifier mécaniquement chaque étape d’une démonstration. Ce rapprochement offrirait le meilleur des deux mondes : une IA qui suggère des idées dans une langue compréhensible et des outils qui contrôlent avec une rigueur absolue leur validité logique.

Pour Google DeepMind, le résultat de l’IMO 2025 est donc moins un point final qu’un test grandeur nature. Gemini Deep Think a démontré qu’une IA pouvait atteindre le niveau de l’or dans une compétition où l’argumentation prime sur l’intuition brute. La prochaine épreuve sera de transformer cette prouesse ponctuelle en aide fiable, vérifiable et réellement utile aux élèves, aux enseignants et aux chercheurs.