Les systèmes d’intelligence artificielle (IA) possèdent de nombreuses compétences, mais ne sont pas à la hauteur lorsqu’il s’agit de s’attaquer à des problèmes mathématiques complexes.
C’est pourquoi Google se réjouit que deux de ses systèmes d’IA DeepMind aient pu résoudre plusieurs problèmes difficiles posés dans le cadre d’un prestigieux concours de mathématiques.
Dans un nouveau billet publié la semaine dernière, Google vante l’intelligence et les réalisations de ses modèles d’IA DeepMind AlphaProof et AlphaGeometry 2. Lors de leur participation aux Olympiades internationales de mathématiques (OIM) de 2024, les deux systèmes ont résolu quatre problèmes sur six. De quoi permettre à l’IA de Google d’obtenir le même niveau qu’un médaillé d’argent pour la première fois dans ce concours, qui s’adresse aux jeunes mathématiciens.
Algèbre, combinatoire, géométrie, théorie des nombres
Chaque année, l’IMO invite l’élite des mathématiciens à résoudre six problèmes extrêmement difficiles en :
- Algèbre
- Combinatoire (compter, sélectionner et arranger un grand nombre d’objets)
- Géométrie
- Théorie des nombres
Au-delà des performances des humains, le concours est également devenu un moyen de tester et de mesurer l’apprentissage automatique (Machine Learning) et les systèmes d’intelligence artificielle dans le domaine du raisonnement mathématique.
Echec de Google sur les combinatoires
Une fois les problèmes traduits dans un langage formel compris par l’IA de Google, AlphaProof a résolu deux problèmes d’algèbre et un problème de théorie des nombres, non seulement en trouvant la réponse, mais aussi en prouvant qu’elle était correcte.
Google indique que le problème de théorie des nombres était le plus difficile de la compétition. Il n’a été résolu que par cinq concurrents humains. AlphaGeometry 2 a résolu le problème de géométrie. Mais aucun des deux modèles n’a été en mesure de résoudre les deux problèmes de combinatoire.
AlphaProof est un système qui peut s’entraîner à prouver des énoncés mathématiques à l’aide du langage formel Lean. En combinant un modèle de langage pré-entraîné avec l’algorithme d’apprentissage par renforcement AlphaZero, AlphaProof a déjà appris à jouer et à gagner aux échecs, au shogi et au Go.
Test d’un système de raisonnement en langage naturel basé sur Gemini
AlphaGeometry 2 est une version améliorée d’AlphaGeometry. Basé sur l’IA Gemini de Google, ce modèle peut traiter des problèmes de géométrie très complexes, notamment ceux qui concernent les mouvements d’objets et les équations d’angles, de rapports et de distances.
En plus de tester les compétences mathématiques d’AlphaProof et d’AlphaGeometry 2, Google a profité de l’IMO pour tester un système de raisonnement en langage naturel basé sur Gemini. Contrairement aux deux autres modèles, celui-ci n’exige pas que les problèmes soient traduits dans un langage formel.
Bien que la réalisation de ces modèles puisse sembler abstraite, Google la considère comme une nouvelle étape vers l’avenir de l’IA.
« Nous sommes enthousiastes à l’idée d’un avenir dans lequel les mathématiciens travailleront avec des outils d’IA pour explorer des hypothèses, essayer de nouvelles approches audacieuses pour résoudre des problèmes de longue date, et compléter rapidement des éléments de preuve qui prennent du temps », a déclaré l’entreprise.