Jeudi, Google DeepMind a annoncé que les systèmes d’IA AlphaProof et AlphaGeometry 2 auraient résolu quatre des six problèmes de l’Olympiade internationale de mathématiques (IMO) de cette année, obtenant un score équivalent à une médaille d’argent. Le géant de la technologie affirme que c’est la première fois qu’une IA atteint ce niveau de performance dans la prestigieuse compétition de mathématiques. Mais comme d’habitude en matière d’IA, les affirmations ne sont pas aussi claires qu’elles le paraissent.
Google affirme 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 plus difficiles. En attendant, AlphaGeometry 2 est décrit comme une version améliorée du précédent mode d’IA de résolution de géométrie de Google, désormais alimenté par un modèle de langage basé sur Gemini formé sur beaucoup plus de données.
Selon Google, les mathématiciens Sir Timothy Gowers et Dr Joseph Myers ont évalué les solutions du modèle d’IA en utilisant les règles officielles de l’OMI. L’entreprise indique que son système combiné a obtenu 28 points sur 42 possibles, soit un peu moins que le seuil de 29 points pour la médaille d’or. Cela comprenait un score parfait sur le problème le plus difficile de la compétition, que Google affirme que seuls cinq concurrents humains ont résolu cette année.
Un concours de mathématiques pas comme les autres
L’IMO, organisé chaque année depuis 1959, confronte les mathématiciens d’élite du pré-universitaire à des problèmes exceptionnellement difficiles d’algèbre, de combinatoire, de géométrie et de théorie des nombres. Les résultats obtenus aux problèmes de l’IMO sont devenus une référence reconnue pour évaluer les capacités de raisonnement mathématique d’un système d’IA.
Google affirme 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é la question de géométrie. Le modèle d’IA n’aurait pas réussi à résoudre les deux problèmes de combinatoire. L’entreprise affirme que ses systèmes ont résolu un problème en quelques minutes, tandis que d’autres ont mis jusqu’à trois jours.
Google affirme avoir 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 sur les énoncés des problèmes au cours de deux sessions de 4,5 heures.
Google indique qu’avant la compétition de cette année, AlphaGeometry 2 était capable de résoudre 83 % des problèmes de géométrie historiques de l’OMI des 25 dernières années, contre 53 % de réussite pour son prédécesseur. L’entreprise affirme 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 Google DeepMind dans un fil de discussion publié sur X. Tout en reconnaissant que cette réussite est « bien au-delà de ce que les démonstrateurs automatiques de théorèmes pouvaient faire auparavant », Gowers a souligné plusieurs réserves clés.
« Le principal point négatif est que le programme a nécessité beaucoup plus de temps que ses concurrents humains – plus de 60 heures pour certains problèmes – et bien sûr une vitesse de traitement bien plus rapide que le pauvre cerveau humain », a écrit Gowers. « Si les concurrents humains avaient eu droit à ce genre de temps par problème, ils auraient sans aucun doute obtenu de meilleurs résultats. »
Gowers a également noté que les humains traduisaient manuellement les problèmes dans le langage formel Lean avant que le modèle d’IA ne commence son travail. Il a souligné que si l’IA effectuait le raisonnement mathématique de base, cette étape d’« autoformalisation » était 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 point où les mathématiciens seront redondants ? C’est difficile à dire. Je suppose que nous sommes encore à une ou deux percées de ce niveau », 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 quand il fonctionne ».
Malgré ces limites, Gowers a émis l’hypothèse que de tels systèmes d’IA pourraient devenir de précieux outils de recherche. « Nous pourrions donc être sur le point de mettre au point 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. Ce serait un outil de recherche extrêmement utile, même s’il n’était pas lui-même capable de résoudre des problèmes ouverts. »