L'IA DeepMind décroche une médaille d'argent à l'Olympiade Internationale de Mathématiques 2024

AlphaProof et AlphaGeometry 2

Deux systèmes d'IA spécialisés ont été développés par Google DeepMind pour résoudre des problèmes mathématiques complexes. AlphaProof combine un modèle linguistique pré-entraîné avec l'algorithme d'apprentissage par renforcement AlphaZero, lui permettant de résoudre et de prouver des problèmes en algèbre et en théorie des nombres. AlphaGeometry 2, une version améliorée de son prédécesseur, se concentre sur les problèmes de géométrie et a été entraîné sur un vaste ensemble de données de 100 millions d'exemples synthétiques. Cette approche innovante de génération de données a permis de surmonter la rareté des données d'entraînement écrites par des humains, un obstacle courant dans le développement de l'IA pour les tâches de raisonnement mathématique.

Méthodologies d'entraînement d'AlphaProof et AlphaGeometry 2

AlphaProof et AlphaGeometry 2 utilisent des méthodologies d'entraînement innovantes pour atteindre leurs impressionnantes capacités de raisonnement mathématique. AlphaProof utilise une approche d'auto-jeu, résolvant des millions de problèmes de différents niveaux de difficulté et de sujets mathématiques sur plusieurs semaines. Il génère des candidats de solutions et recherche des étapes de preuve dans le langage formel Lean, renforçant son modèle linguistique à chaque preuve vérifiée. AlphaGeometry 2 s'appuie sur cela en intégrant un modèle linguistique Gemini entraîné sur un ensemble de données plus vaste contenant 100 millions d'exemples synthétiques. Pour combler le fossé entre les langages naturels et formels, les chercheurs ont affiné un modèle Gemini pour traduire des énoncés de problèmes en langage naturel en langage mathématique formel, créant une vaste bibliothèque de problèmes formels. Cette approche a permis aux systèmes de s'attaquer à un large éventail de défis mathématiques.

Performance à l'OIM 2024

À l'Olympiade Internationale de Mathématiques 2024, AlphaProof a résolu avec succès deux problèmes d'algèbre et un problème de théorie des nombres, tandis qu'AlphaGeometry 2 a résolu un problème de géométrie. Leurs solutions combinées ont obtenu un total de 28 points sur 42 possibles, ce qui équivaut à une performance de médaille d'argent et à un seul point du seuil de la médaille d'or. Notamment, AlphaGeometry 2 a résolu son problème en seulement 19 secondes, démontrant son efficacité remarquable. Les problèmes ont été traduits manuellement en langage mathématique formel pour les systèmes d'IA, et les solutions ont mis de quelques minutes à trois jours à être générées.

Signification de cette réussite

Cette étape représente un bond en avant significatif dans la capacité de l'IA à gérer le raisonnement mathématique complexe, une tâche auparavant difficile pour les machines. Le succès d'AlphaProof et d'AlphaGeometry 2 démontre que l'IA peut désormais effectuer le raisonnement logique de haut niveau, l'abstraction et la planification hiérarchique nécessaires pour résoudre les problèmes de l'OIM. Il est particulièrement remarquable que les systèmes d'IA aient produit des preuves lisibles par l'homme et utilisé des règles de géométrie classiques, similaires à celles des concurrents humains. Cette réussite a été reconnue par des mathématiciens experts, dont le médaillé Fields Tim Gowers, qui s'est dit surpris de la capacité de l'IA à trouver les « clés magiques » qui débloquent des problèmes complexes. Les performances des systèmes approchent celles des médaillés d'or humains, AlphaGeometry 2 résolvant 83 % de tous les problèmes de géométrie de l'OIM historiques des 25 dernières années, une amélioration significative par rapport au taux de réussite de 53 % de son prédécesseur.

Potentiel futur de l'IA en mathématiques

La performance réussie d'AlphaProof et d'AlphaGeometry 2 à l'OIM ouvre de nouvelles possibilités pour la recherche mathématique et la résolution de problèmes assistées par l'IA. Ces systèmes pourraient potentiellement aider les mathématiciens à découvrir de nouvelles perspectives, à résoudre des problèmes ouverts et à accélérer la découverte scientifique. Dans le même temps, les chercheurs de DeepMind reconnaissent que l'IA manque encore de la créativité et de l'intuition de résolution de problèmes des mathématiciens humains, ce qui suggère qu'un développement supplémentaire est nécessaire pour que l'IA puisse égaler pleinement les capacités humaines en mathématiques. À mesure que ces systèmes continuent d'évoluer, ils pourraient devenir de puissants outils de calcul, semblables à des calculatrices, aidant les humains à formuler des preuves mathématiques et à explorer des hypothèses complexes.