De l’argent au gold : Comment l’IA de DeepMind a conquis l’Olympiade mathématique

L’IA de DeepMind a réalisé des progrès remarquables dans le raisonnement mathématique en l’espace d’un an seulement. Après avoir obtenu une médaille d’argent à l’Olympiade mathématique internationale (IMO) en 2024, leur système d’IA a remporté la médaille d’or en 2025. Cette avancée rapide met en évidence les capacités croissantes de l’intelligence artificielle pour résoudre des problèmes complexes et abstraits qui nécessitent de la créativité et de l’insight humaines. Cet article présentera comment DeepMind a réalisé cette transformation, les choix techniques et stratégiques qui se cachent derrière, et les implications plus larges de ces progrès.

La signification de l’IMO

L’Olympiade mathématique internationale, créée en 1959, est reconnue mondialement comme la principale compétition de mathématiques pour les élèves du secondaire. Chaque année, les meilleurs élèves du monde entier sont confrontés à six problèmes redoutables dans les domaines de l’algèbre, de la géométrie, de la théorie des nombres et de la combinatoire. Résoudre ces problèmes nécessite beaucoup plus que des calculs ; les participants doivent faire preuve de créativité mathématique, de pensée logique rigoureuse et de capacité à construire des preuves élégantes.

Pour l’intelligence artificielle, l’IMO présente un défi unique. Alors que l’IA a maîtrisé la reconnaissance de modèles, l’analyse de données et même des jeux complexes comme le Go et les échecs, les mathématiques olympiques exigent une raison et une synthèse créatives, des capacités traditionnellement considérées comme des marques de l’intelligence humaine. En conséquence, l’IMO est devenu un terrain d’essai naturel pour évaluer à quel point l’IA est proche de réaliser un raisonnement vraiment similaire à celui de l’homme.

La percée de la médaille d’argent de 2024

En 2024, DeepMind a présenté deux systèmes d’IA pour résoudre des problèmes de niveau IMO : AlphaProof et AlphaGeometry 2. Ces deux systèmes sont des exemples de “neuro-symbolic” AI, combinant les forces des grands modèles de langage (LLM) avec la rigueur de la logique symbolique.

AlphaProof a été conçu pour prouver des énoncés mathématiques en utilisant Lean, un langage mathématique formel. Il a combiné Gemini, le grand modèle de langage de DeepMind, avec AlphaZero, un moteur d’apprentissage par renforcement connu pour son succès dans les jeux de plateau. Dans ce contexte, le rôle de Gemini était de traduire les problèmes de langage naturel en Lean et d’essayer de prouver des étapes logiques. AlphaProof a été formé sur des millions de problèmes d’exemple couvrant différentes disciplines et difficultés mathématiques. Le système s’est amélioré en essayant de prouver des énoncés de plus en plus complexes, similairement à la façon dont AlphaZero a appris en jouant contre lui-même.

AlphaGeometry 2 a été conçu pour résoudre des problèmes de géométrie. Ici, la compréhension du langage de Gemini a permis à l’IA de prédire des constructions auxiliaires utiles, tandis qu’un moteur de raisonnement symbolique gérait les déductions logiques. Cette approche hybride a permis à AlphaGeometry de résoudre des problèmes géométriques bien au-delà de la portée de la raison machine traditionnelle.

Ensemble, ces systèmes ont résolu quatre des six problèmes de l’IMO : deux en algèbre, un en théorie des nombres et un en géométrie, obtenant un score de 28 sur 42. Cette performance était un jalon important, car c’était la première fois qu’un système d’IA avait atteint le niveau de la médaille d’argent à l’IMO. Cependant, ce succès reposait lourdement sur des experts humains pour traduire les problèmes en langages mathématiques formels. Ils ont également nécessité des ressources computationnelles massives, qui ont pris des jours de temps de traitement pour chaque problème.

Les innovations techniques derrière la médaille d’or

La transition de DeepMind d’une médaille d’argent à une médaille d’or a été motivée par plusieurs améliorations techniques importantes.

1. Le langage naturel comme moyen de preuve

Le changement le plus significatif a été le passage de systèmes qui nécessitaient des traductions d’experts en langages formels à traiter le langage naturel comme moyen de preuve. Ce changement est réalisé grâce à une version améliorée de Gemini équipée de capacités Deep Think. Au lieu de convertir les problèmes en Lean, le modèle traite le texte directement, génère des esquisses informelles, formalise internement les étapes critiques et produit une preuve anglaise raffinée. L’apprentissage par renforcement à partir de la rétroaction humaine (RLHF) a été utilisé pour récompenser les solutions qui étaient logiquement cohérentes, brèves et présentées.

Gemini Deep Think diffère de la version publique de Gemini de deux manières principales. Premièrement, il alloue des fenêtres de contexte plus longues et plus de jetons de calcul par requête, ce qui permet au modèle de maintenir des chaînes de pensée multi-pages. Deuxièmement, il utilise un raisonnement parallèle, où des centaines de fils spéculatifs sont générés pour différentes solutions potentielles. Un superviseur léger classe et promeut ensuite les chemins les plus prometteurs, empruntant des concepts à la recherche d’arbre de Monte Carlo mais appliqués au texte. Cette approche imite la façon dont les équipes humaines brainstorming, éliminent les idées improductives et convergent vers des solutions élégantes.

2. Formation et apprentissage par renforcement

La formation de Gemini Deep Think a impliqué l’ajustement fin du modèle pour prédire les prochaines étapes plutôt que les réponses finales. À cette fin, un corpus de 100 000 solutions de haute qualité d’Olympiade et de concours universitaires a été compilé. Le corpus a été principalement collecté à partir de forums mathématiques publics, de prépublications arXiv et de séries de problèmes universitaires. Des mentors humains ont examiné les exemples de formation pour filtrer les preuves illogiques ou incomplètes. L’apprentissage par renforcement a aidé à affiner le modèle, le poussant à produire des preuves concises et précises. Les premières versions produisaient des preuves trop verbales, mais des pénalités sur les phrases redondantes ont aidé à élaguer la sortie.

Contrairement à la formation conventionnelle, qui lutte souvent avec des récompenses rares où la rétroaction est binaire, soit la preuve est correcte ou non. DeepMind a mis en œuvre un système de récompense étape par étape, où chaque sous-lemme vérifié contribuait au score global. Ce mécanisme de récompense guide Gemini même lorsque la preuve complète est rare. Le processus de formation a duré trois mois et a utilisé environ 25 millions d’heures de TPU.

3. Parallélisation massive

La parallélisation a également joué un rôle crucial dans les progrès de DeepMind de l’argent à l’or. Chaque problème a généré plusieurs branches de raisonnement en parallèle, avec des ressources qui se déplaçaient dynamiquement vers des voies plus prometteuses lorsque les autres stallaient. Cette planification dynamique a été particulièrement bénéfique pour les problèmes de combinatoire, qui ont de grands espaces de solution. L’approche est similaire à la façon dont les humains testent les inégalités auxiliaires avant de s’engager dans une induction complète. Même si cette technique était coûteuse en termes de calcul, elle était gérable en utilisant les grappes TPU v5 de DeepMind.

DeepMind à l’IMO 2025

Pour maintenir l’intégrité de la compétition, DeepMind a gelé les poids du modèle trois semaines avant l’IMO pour empêcher la fuite de problèmes officiels dans l’ensemble de formation. Ils ont également filtré les données contenant des solutions à des questions d’Olympiade non publiées.

Pendant la compétition, Gemini Deep Think a reçu les six problèmes officiels au format texte brut, sans accès à Internet. Le système a fonctionné sur un cluster configuré pour simuler la puissance de calcul d’un ordinateur portable standard par processus. L’ensemble du processus de résolution de problèmes a été terminé en moins de trois heures, bien dans les limites de temps. Les preuves générées ont été soumises aux coordinateurs de l’IMO sans altération.

Gemini Deep Think a obtenu des scores parfaits sur les cinq premiers problèmes. La dernière question, qui était un puzzle de combinatoire difficile, a cependant déjoué à la fois l’IA et 94 % des participants humains. Malgré cela, l’IA a terminé avec un score total de 35/42 pour remporter la médaille d’or. Ce score était sept points supérieur à la performance d’argent de l’année précédente. Les observateurs ont plus tard décrit les preuves de l’IA comme « diligent » et « complète », notant qu’elles suivaient les justifications rigoureuses attendues des concurrents humains.

Implications pour l’IA et les mathématiques

La réalisation de DeepMind est un jalon important pour l’IA et les mathématiques. Pour l’IA, maîtriser l’IMO est un pas vers l’intelligence artificielle générale (IAG), où les systèmes peuvent effectuer toute tâche intellectuelle que peut effectuer un humain. Résoudre des problèmes mathématiques complexes nécessite de la raison et de la compréhension, qui sont des composants fondamentaux de l’intelligence générale. Ce succès indique que l’IA fait des progrès vers des capacités cognitives plus humaines.

Pour les mathématiques, les systèmes d’IA comme Gemini Deep Think peuvent devenir des outils inestimables pour les mathématiciens. Ils peuvent aider à explorer de nouveaux domaines, à vérifier des conjectures et même à découvrir de nouveaux théorèmes. En automatisant les aspects plus fastidieux de la construction de preuves, l’IA libère les mathématiciens humains pour se concentrer sur des travaux conceptuels de niveau supérieur. De plus, les techniques développées pour ces systèmes d’IA pourraient inspirer de nouvelles méthodes dans la recherche mathématique qui pourraient ne pas être possibles grâce à l’effort humain seul.

Cependant, les progrès de l’IA dans les mathématiques soulèvent également des questions sur le rôle de l’IA dans les contextes éducatifs et les compétitions. À mesure que les capacités de l’IA continuent de croître, il y aura des débats sur la façon dont son implication pourrait altérer la nature de l’éducation et de la compétition mathématiques.

Regard vers l’avenir

Remporter la médaille d’or de l’IMO est un jalon important, mais de nombreux défis mathématiques restent hors de portée des systèmes d’IA actuels. Cependant, la progression rapide de l’argent à l’or en un an seulement met en évidence le rythme accéléré des innovations et des développements de l’IA. Si ce rythme se poursuit, les systèmes d’IA pourraient bientôt aborder certains des problèmes mathématiques les plus célèbres non résolus. Même si la question de savoir si l’IA remplacera ou améliorera la créativité humaine reste sans réponse, l’IMO 2025 est une indication claire que l’intelligence artificielle a fait des progrès significatifs dans le raisonnement logique.