AlphaProof et AlphaGeometry, deux nouveaux modèles d’IA développés par Google DeepMind, ont résolu avec succès quatre des six problèmes de la prestigieuse Olympiade internationale des mathématiques (IMO). Utilisant un système de raisonnement logique avancé, ils ont remporté l’équivalent d’une médaille d’argent, démontrant un taux de réussite inédit pour la résolution de ce type de problèmes par l’IA.
Organisé une fois par an depuis 1959, l’IMO est le plus grand et le plus ancien concours international de mathématiques. Afin d’y participer, les jeunes mathématiciens d’élite (de niveau préuniversitaire) du monde entier s’entraînent parfois pendant des milliers d’heures. Le concours consiste à résoudre six problèmes extrêmement complexes d’algèbre, de combinatoire (un domaine mathématique axé sur le comptage et l’organisation des objets), de géométrie et de théorie des nombres.
Plus récemment, l’IMO est également devenu une référence pour mesurer les capacités de raisonnement avancé des systèmes d’IA. Cependant, ils étaient jusqu’à présent encore loin d’avoir les capacités de raisonnement logique nécessaires à la résolution de problèmes mathématiques complexes et généraux. En effet, ces derniers nécessitent une planification hiérarchique complexe, ainsi que la définition de sous-objectifs, la vérification des réponses et l’essai de nouvelles méthodes.
D’un autre côté, les IA se heurtent à un énorme manque de données d’entraînement en ce qui concerne les mathématiques. « Il est souvent plus facile d’entraîner un modèle pour les mathématiques si vous avez un moyen de vérifier ses réponses (dans un langage formel), mais il existe comparativement moins de données mathématiques formelles en ligne que de données en langage naturel (langage informel) », explique Katie Collins, chercheuse à l’Université de Cambridge spécialisée dans les mathématiques et l’IA, au MIT Review.
Google DeepMind a développé AlphaProof et AlphaGeometry 2 pour combler ces lacunes. En participant au concours IMO de cette année, les deux modèles ont montré un taux de réussite impressionnant. « Aucun système de ce type développé jusqu’à présent n’a été capable de résoudre des problèmes avec un tel taux de réussite et un tel niveau de généralité », affirme Pushmeet Kohli, vice-président de la recherche chez Google DeepMind.
Un système de vérification complexe
AlphaProof est un système basé sur l’apprentissage par renforcement, s’entraînant à prouver des énoncés mathématiques dans le langage de programmation formel Lean. Afin de pouvoir être traitées plus facilement par l’IA, les données devaient ainsi être traduites en langage mathématique formel. Contrairement aux traitements basés sur le langage naturel, le traitement du langage formel permet de vérifier efficacement l’exactitude d’un raisonnement mathématique. Les approches basées sur le langage naturel peuvent, quant à elles, générer des réponses plausibles, mais généralement incorrectes.
Les données mathématiques en langage naturel ont été traduites automatiquement en langage formel à l’aide d’une version améliorée de Gemini, l’IA générative la plus performante de Google. Cela a permis de créer une grande bibliothèque de problèmes mathématiques formels de difficulté variable. Gemini a ensuite été combiné à l’algorithme d’apprentissage par renforcement AlphaZero, qui a auparavant déjà appris à maîtriser les jeux d’échecs, de shogi et de go.
Les deux modèles combinés ont permis de développer AlphaProof, qui génère des réponses candidates puis effectue un processus de feed-back pour en prouver ou réfuter l’exactitude. Le système gagne en efficacité à mesure qu’il vérifie des réponses, permettant ainsi de résoudre ultérieurement des problèmes plus complexes. Cette boucle d’entraînement a été répétée pendant plusieurs semaines avant la compétition.
Quant à AlphaGeometry 2, il s’agit d’une version améliorée d’AlphaGeometry, un modèle conçu pour la résolution des problèmes mathématiques liés aux mouvements des objets et aux équations impliquant des angles, des rapports et des distances. Le nouveau modèle s’appuie sur un moteur deux fois plus rapide que son prédécesseur et est formé à partir de beaucoup plus de données synthétiques — ce qui permet de traiter des problèmes de géométrie beaucoup plus difficiles.
La médaille d’or ratée de peu, avec un score de 28 points sur 42
Lors du concours, les réponses données par les modèles ont été évaluées et notées par deux éminents mathématiciens : Timothy Gowers, médaillé d’or de l’IMO et lauréat de la médaille Fields, et Joseph Myers, double médaillé d’or de l’IMO et président du comité de sélection des problèmes de l’IMO 2024. À l’instar des étudiants, les systèmes d’IA disposaient de deux sessions de 4,5 heures chacune pour résoudre les six problèmes du concours.
Les systèmes ont résolu l’un des problèmes en quelques minutes, tandis que les autres leur ont nécessité jusqu’à 3 jours. AlphaProof a résolu deux problèmes d’algèbre et un problème de théorie des nombres en déterminant la réponse et en prouvant qu’elle était correcte. Cette dernière était le problème le plus difficile du concours et a été résolue par seulement cinq concurrents. AlphaGeometry 2, quant à lui, a résolu l’un des problèmes de géométrie, tandis que les deux autres problèmes de combinatoire sont restés sans réponse.
Chacun des six problèmes rapportant sept points, le score maximum possible est de 42. La médaille d’or peut être obtenue à partir de 29 points. Ensemble, les deux systèmes ont obtenu un score de 28 points, ratant ainsi de peu la médaille d’or. Il s’agit de la première fois qu’un système d’IA parvient à ce niveau de performance sur le concours IMO. « En tant que mathématicien, je trouve cela très impressionnant et que cela représente un progrès significatif par rapport à ce qui était possible auparavant », a déclaré Gowers lors d’une conférence de presse.
Ces nouvelles performances pourraient ouvrir la voie à des collaborations humain-IA pour les recherches dans le domaine des mathématiques. Cela permettrait peut-être aussi de décrypter la manière dont notre cerveau résout ces problèmes, un aspect qui demeure jusqu’à aujourd’hui en grande partie incompris.