Les équipes de Google DeepMind ont réussi un défi majeur en gagnant un concours mondial de mathématiques grâce l’IA AlphaProof. Ce modèle voit le jour huit ans après le lancement de l’AlphaGo, l’IA qui a fait ses promesses au Go, le jeu de société, de 2016.
En 2017, DeepMind a fait face à un échec sans précédent. Mais il revient aujourd’hui en force et dévoile le premier IA à réussir à répondre à des questions de l’Olympiade international de mathématiques.
Numéro un à l’Olympiade International de Mathématiques ?
Pas plus tard que la semaine dernière, Google DeepMind a fait une nouvelle démonstration impressionnante dans le domaine de l’intelligence artificielle appliquée aux mathématiques.
Alex Davies, responsable de l’initiative mathématique chez Google DeepMind, a qualifié la victoire d’AlphaProof d’avancée majeure dans le raisonnement mathématique par un système d’IA.
Deux modèles de Google DeepMind ont participé à l’Olympiade Internationale de Mathématiques 2024.
Le concours s’est déroulé du 11 au 22 juillet dernier à Londres, à l’Université de Bath pour être précis.
L’IMO ou l’International Mathematics Olympiad, est en effet considérée comme la principale compétition de mathématiques au monde.
Elle attire les mathématiciens les plus brillants selon les communications promotionnelles de l’événement sur les réseaux sociaux.
Victoire d’AlphaProof face aux participants humains
L’Olympiade Internationale de Mathématiques 2024 a réuni 609 lycéens venant de 108 pays différents.
Lors de cette compétition, les participants humains ont obtenu un total de 326 médailles. Soit 58 médailles d’or, 123 médailles d’argent et 145 médailles de bronze.
Quant à AlphaProof de Google DeepMind, sa performance a été remarquable. Le modèle a réussi à résoudre quatre problèmes sur les six proposés, totalisant 28 points.
Ce score correspond au niveau requis pour obtenir une médaille d’argent dans cette compétition.
C’est d’ailleurs la première fois qu’un système d’intelligence artificielle atteint un niveau de performance équivalent à une médaille lors d’une Olympiade de mathématiques.
Quand les champions de l’IMO témoignent de la prouesse de l’AlphaProof
Pour prouver les performances de l’AlphaProof lors de l’IMO, Google DeepMind a sollicité l’expertise de deux évaluateurs indépendants.
Il s’agit de Timothy Gowers, mathématicien à l’université de Cambridge et lauréat de la médaille Fields, et de Joseph Myers, développeur de logiciels également basé à Cambridge. Tous deux sont d’anciens médaillés d’or de l’IMO.
Joseph Myers a affirmé avoir évalué les tentatives de l’IA selon les mêmes critères que ceux appliqués aux participants humains cette année.
Timothy Gowers, quant à lui, a exprimé son admiration pour les performances de l’IA dans un courriel.
Bien qu’ayant été informé des ambitions de DeepMind quelques semaines avant l’événement, ce qui avait élevé ses attentes, il a déclaré que le programme avait non seulement répondu à ces attentes, mais les avait même largement dépassées dans certains cas.
Selon lui, les IA telles qu’AlphaProof ont la capacité de trouver les clés magiques nécessaires à la résolution des problèmes posés dans un concours de type Olympiade Mathématiques.
Mais comment ça se fait ?
AlphaProof est un système développé par DeepMind qui combine un modèle de langage avec la technique d’apprentissage par renforcement.
Il utilise le moteur AlphaZero, déjà employé avec succès par l’entreprise pour résoudre des jeux comme le Go et certains problèmes mathématiques spécifiques.
L’apprentissage par renforcement permet à un réseau neuronal d’apprendre par essais et erreurs.
C’est une méthode particulièrement efficace lorsque les réponses peuvent être évaluées selon des critères objectifs.
Dans cette optique, AlphaProof a été entraîné à lire et à écrire des preuves dans un langage formel appelé Lean.
Ce langage est utilisé dans un logiciel d’assistance à la preuve du même nom, qui est populaire parmi les mathématiciens.
Pour vérifier l’exactitude de ses résultats, AlphaProof les a exécutés dans le package Lean.
Cette approche a permis de compléter certaines étapes du code de preuve. Ce qui assure par la suite la validité des démonstrations produites par le système.
Les défis auxquels DeepMind ont dû se confronter
L’entraînement d’un modèle de langage comme AlphaProof nécessite une quantité considérable de données.
Mais le nombre de preuves mathématiques disponibles dans le langage Lean était limité.
Pour résoudre ce problème, l’équipe de DeepMind a développé un réseau supplémentaire.
Ce réseau avait pour tâche de traduire en Lean un corpus existant d’un million de problèmes écrits en langage naturel. Mais sans inclure de solutions rédigées par des humains.
Thomas Hubert, chercheur en apprentissage automatique chez DeepMind et coresponsable du développement d’AlphaProof, explique leur approche.
« Nous nous sommes demandés si nous pouvions apprendre à prouver, même sans nous être entraînés initialement sur des preuves écrites par des humains », a-t-il déclaré.
Cette méthode s’inspire de celle utilisée par DeepMind pour le jeu de Go. Dans ce cas, leur système d’IA avait appris à jouer en s’affrontant lui-même, plutôt qu’en observant des parties jouées par des humains.
De la même manière, AlphaProof a été conçu pour apprendre à élaborer des preuves mathématiques de façon autonome.
Ce qui rappelle comment on joue aux jeux de société et comment on apprend de nos propres erreurs. Quitte à dire que l’IA se rapproche de plus en plus de l’intelligence humaine.
- Partager l'article :
