Jeudi, Google DeepMind a annoncé que ses systèmes d’IA, AlphaProof et AlphaGeometry 2, ont apparemment résolu quatre des six problèmes de la Olympiade Internationale de Mathématiques (IMO) de cette année, atteignant un score équivalent à une médaille d’argent. Le géant technologique affirme que c’est la première fois qu’une IA atteint ce niveau de performance dans cette compétition mathématique prestigieuse, mais comme souvent dans le domaine de l’IA, les affirmations ne sont pas aussi claires qu’elles paraissent.
Google précise qu’AlphaProof utilise l’apprentissage par renforcement pour prouver des énoncés mathématiques dans le langage formel appelé Lean. Le système s’entraîne en générant et en vérifiant des millions de preuves, s’attaquant progressivement à des problèmes de plus en plus difficiles. Pendant ce temps, AlphaGeometry 2 est décrit comme une version améliorée de l’ancien modèle de résolution de géométrie de Google, désormais propulsée par un modèle de langage basé sur Gemini, entraîné sur une quantité de données significativement plus importante.
Selon Google, des mathématiciens de renom tels que Sir Timothy Gowers et Dr. Joseph Myers ont évalué les solutions du modèle d’IA en utilisant les règles officielles de l’IMO. La société rapporte que son système combiné a obtenu 28 des 42 points possibles, juste en dessous du seuil de la médaille d’or, fixé à 29 points. Cela incluait un score parfait sur le problème le plus difficile de la compétition, que Google affirme n’avoir été résolu que par cinq candidats humains cette année.
Une compétition mathématique sans pareille
L’IMO, tenue chaque année depuis 1959, oppose les meilleurs étudiants en mathématiques avant l’université à des problèmes d’une extrême difficulté en algèbre, combinatoire, géométrie et théorie des nombres. La performance sur les problèmes de l’IMO est devenue un critère reconnu pour évaluer les capacités de raisonnement mathématique d’un système d’IA.
Google indique qu’AlphaProof a résolu deux problèmes d’algèbre et un problème de théorie des nombres, tandis qu’AlphaGeometry 2 a abordé le problème de géométrie. Le modèle d’IA n’a apparemment pas réussi à résoudre les deux problèmes de combinatoire. La société affirme que ses systèmes ont résolu un problème en quelques minutes, tandis que d’autres ont pris jusqu’à trois jours.
Google explique qu’il a d’abord traduit les problèmes de l’IMO en langage mathématique formel pour que son modèle d’IA puisse les traiter. Cette étape diffère de la compétition officielle, où les concurrents humains travaillent directement avec les énoncés des problèmes lors de deux sessions de 4,5 heures.
Avant la compétition de cette année, Google indique qu’AlphaGeometry 2 pouvait résoudre 83 % des problèmes de géométrie de l’IMO des 25 dernières années, contre 53 % pour son prédécesseur. La société prétend que le nouveau système a résolu le problème de géométrie de cette année en 19 secondes après avoir reçu la version formalisée.
Limites
Malgré les affirmations de Google, Sir Timothy Gowers a offert une perspective plus nuancée sur les modèles de Google DeepMind dans un fil de discussion sur X. Tout en reconnaissant l’accomplissement comme étant “bien au-delà de ce que les provers de théorèmes automatiques pouvaient faire auparavant”, Gowers a souligné plusieurs qualifications importantes.
“La principale qualification est que le programme a mis beaucoup plus de temps que les concurrents humains — pour certains problèmes, plus de 60 heures — et bien sûr une vitesse de traitement beaucoup plus rapide que le pauvre cerveau humain,” a écrit Gowers. “Si les concurrents humains avaient eu ce genre de temps par problème, ils auraient sans doute obtenu un score plus élevé.”
Gowers a également noté que les humains ont manuellement traduit les problèmes en utilisant le langage formel Lean avant que le modèle d’IA ne commence son travail. Il a souligné que, même si l’IA a réalisé le raisonnement mathématique de base, cette étape de “l’auto-formalisation” a été réalisée par des humains.
En ce qui concerne les implications plus larges pour la recherche mathématique, Gowers a exprimé son incertitude. “Sommes-nous proches du moment où les mathématiciens deviennent superflus ? Il est difficile de le dire. Je devinerais que nous en sommes encore à une ou deux avancées de là,” a-t-il écrit. Il a suggéré que les longs temps de traitement du système indiquent qu’il n’a pas “résolu les mathématiques”, mais a reconnu qu'”il se passe clairement quelque chose d’intéressant lorsqu’il fonctionne”.
Malgré ces limites, Gowers a émis l’hypothèse que de tels systèmes d’IA pourraient devenir des outils de recherche précieux. “Nous pourrions donc être proches d’avoir un programme qui permettrait aux mathématiciens d’obtenir des réponses à un large éventail de questions, à condition que ces questions ne soient pas trop difficiles — le genre de choses que l’on peut faire en quelques heures. Cela serait extrêmement utile comme outil de recherche, même si ce n’était pas capable de résoudre des problèmes ouverts.”
En tant que journaliste, je ne peux m’empêcher de réfléchir à la manière dont ces avancées technologiques pourraient transformer notre approche de l’enseignement et de la recherche en mathématiques. La collaboration entre humains et IA pourrait ouvrir de nouvelles voies, qui sait quelles découvertes passionnantes cela pourrait apporter dans le futur.