Les nouveaux systèmes d'IA de Google DeepMind peuvent désormais résoudre des problèmes mathématiques complexes
infohightech ·
Les modèles d'IA peuvent facilement générer des essais et d'autres types de textes. En revanche, ils sont loin d'être aussi performants pour résoudre des problèmes mathématiques, qui impliquent généralement un raisonnement logique, ce qui dépasse les capacités de la plupart des systèmes d'IA actuels.
Mais les choses sont peut-être enfin en train de changer. Google DeepMind affirme avoir formé deux systèmes d'IA spécialisés à la résolution de problèmes mathématiques complexes impliquant un raisonnement avancé. Ces systèmes, appelés AlphaProof et AlphaGeometry 2, ont travaillé ensemble pour résoudre avec succès quatre des six problèmes de l'Olympiade internationale de mathématiques (OIM) de cette année, une compétition prestigieuse destinée aux élèves du secondaire. Ils ont remporté l'équivalent d'une médaille d'argent.
C'est la première fois qu'un système d'intelligence artificielle obtient un taux de réussite aussi élevé pour ce type de problèmes. "Il s'agit d'un progrès considérable dans le domaine de l'apprentissage automatique et de l'IA", déclare Pushmeet Kohli, vice-président de la recherche chez Google DeepMind, qui a travaillé sur le projet. "Aucun système de ce type n'a été développé jusqu'à présent pour résoudre des problèmes avec un tel taux de réussite et un tel niveau de généralité."
Il y a quelques raisons pour lesquelles les problèmes mathématiques qui impliquent un raisonnement avancé sont difficiles à résoudre pour les systèmes d'IA. Ces types de problèmes nécessitent souvent la formation et l'utilisation d'abstractions. Ils impliquent également une planification hiérarchique complexe, ainsi que la définition de sous-objectifs, le retour en arrière et l'essai de nouveaux chemins. Tous ces éléments constituent un défi pour l'IA.
Les systèmes d'IA capables de résoudre des problèmes mathématiques complexes pourraient nous permettre de construire des outils d'IA plus puissants.
"Il est souvent plus facile de former un modèle mathématique si l'on dispose d'un moyen de vérifier ses réponses (par exemple, dans un langage formel), mais il y a comparativement moins de données mathématiques formelles en ligne que de données en langage naturel libre (langage informel)", explique Katie Collins, chercheuse à l'université de Cambridge spécialisée dans les mathématiques et l'IA, mais qui n'a pas été impliquée dans le projet.
C'est pour combler ce fossé que Google DeepMind a créé AlphaProof, un système basé sur l'apprentissage par renforcement qui s'entraîne à prouver des énoncés mathématiques dans le langage de programmation formel Lean. La clé est une version de l'IA Gemini de DeepMind qui a été affinée pour traduire automatiquement les problèmes mathématiques formulés dans un langage naturel et informel en énoncés formels, plus faciles à traiter par l'IA. Cela a permis de créer une vaste bibliothèque de problèmes mathématiques formels présentant divers degrés de difficulté.
L'automatisation du processus de traduction des données en langage formel est un grand pas en avant pour la communauté mathématique, déclare Wenda Li, maître de conférences en IA hybride à l'université d'Édimbourg, qui a évalué la recherche mais n'a pas participé au projet.
"Nous pouvons avoir une plus grande confiance dans l'exactitude des résultats publiés s'ils sont capables de formuler ce système de preuve, et cela peut aussi devenir plus collaboratif", ajoute-t-il.
Le modèle Gemini travaille aux côtés d'AlphaZero - le modèle d'apprentissage par renforcement que Google DeepMind a entraîné à maîtriser des jeux tels que le jeu de Go et les échecs - pour prouver ou réfuter des millions de problèmes mathématiques. Plus il a résolu de problèmes avec succès, plus AlphaProof est devenu performant pour s'attaquer à des problèmes de complexité croissante.
Bien qu'AlphaProof ait été entraîné à résoudre des problèmes portant sur un large éventail de sujets mathématiques, AlphaGeometry 2-une version améliorée d'un système que Google DeepMind a annoncé en janvier - a été optimisé pour résoudre des problèmes liés aux mouvements d'objets et aux équations impliquant des angles, des ratios et des distances. Parce qu'il a été entraîné sur des données synthétiques beaucoup plus nombreuses que son prédécesseur, il a été en mesure de répondre à des questions de géométrie beaucoup plus difficiles.
Pour tester les capacités des systèmes, les chercheurs de Google DeepMind leur ont demandé de résoudre les six problèmes posés aux humains participant à l'OIM de cette année et de prouver que les réponses étaient correctes. AlphaProof a résolu deux problèmes d'algèbre et un problème de théorie des nombres, dont l'un était le plus difficile de la compétition. AlphaGeometry 2 a réussi à résoudre une question de géométrie, mais deux questions de combinatoire (un domaine des mathématiques axé sur le comptage et la disposition des objets) n'ont pas été résolues.
Ils ont dû jeter la plupart des résultats, mais il y avait « de l'or dans les ordures ».
"En général, AlphaProof obtient de bien meilleurs résultats en algèbre et en théorie des nombres qu'en combinatoire", explique Alex Davies, ingénieur de recherche au sein de l'équipe AlphaProof. "Nous cherchons encore à en comprendre les raisons, ce qui nous permettra, nous l'espérons, d'améliorer le système. »
Deux mathématiciens renommés, Tim Gowers et Joseph Myers, ont vérifié les soumissions des systèmes. Ils ont attribué à chacune des quatre réponses correctes une note complète (sept sur sept), ce qui donne aux systèmes un total de 28 points sur un maximum de 42. Un participant humain obtenant ce score se verrait décerner une médaille d'argent et manquerait de peu la médaille d'or, dont le seuil commence à 29 points.
C'est la première fois qu'un système d'IA est capable de réaliser une performance de niveau « médaillable » sur des questions OIM. "En tant que mathématicien, je trouve que c'est très impressionnant et que c'est un bond en avant par rapport à ce qui était possible auparavant", a déclaré Tim Gowers.
Joseph Myers a reconnu que les réponses mathématiques des systèmes représentaient une avancée substantielle par rapport à ce que l'IA pouvait réaliser auparavant. "Il sera intéressant de voir comment les choses évoluent et s'il est possible de les rendre plus rapides, et si cela peut s'étendre à d'autres types de mathématiques", a-t-il déclaré.
La création de systèmes d'IA capables de résoudre des problèmes mathématiques plus complexes pourrait ouvrir la voie à des collaborations passionnantes entre l'homme et l'IA, en aidant les mathématiciens à résoudre et à inventer de nouveaux types de problèmes, selon Katie Collins. Cela pourrait à son tour nous aider à mieux comprendre comment nous, les humains, abordons les mathématiques.
"Nous ignorons encore beaucoup de choses sur la manière dont les humains résolvent les problèmes mathématiques complexes", déclare-t-elle.