L'IA à l'Olympiade mathématique internationale : comment AlphaProof et AlphaGeometry 2 ont atteint la médaille d'argent

Le raisonnement mathématique est un aspect essentiel des capacités cognitives humaines, car il stimule les progrès des découvertes scientifiques et des développements technologiques. Alors que nous nous efforçons de développer une intelligence artificielle générale qui corresponde à la cognition humaine, il est essentiel de doter l’IA de capacités avancées de raisonnement mathématique. Même si les systèmes d’IA actuels peuvent résoudre des problèmes mathématiques de base, ils ont du mal à gérer le raisonnement complexe nécessaire aux disciplines mathématiques avancées comme l’algèbre et la géométrie. Cependant, cela pourrait changer, comme l'a fait Google DeepMind des avancées significatives pour faire progresser les capacités de raisonnement mathématique d’un système d’IA. Cette percée est réalisée au Olympiade mathématique internationale (IMO) 2024. Créée en 1959, l'OMI est le concours de mathématiques le plus ancien et le plus prestigieux, défiant les lycéens du monde entier avec des problèmes d'algèbre, de combinatoire, de géométrie et de théorie des nombres. Chaque année, des équipes de jeunes mathématiciens s'affrontent pour résoudre six problèmes très difficiles. Cette année, Google DeepMind a introduit deux systèmes d'IA : AlphaProof, axé sur le raisonnement mathématique formel, et AlphaGeometry 2, spécialisé dans la résolution de problèmes géométriques. Ces systèmes d’IA ont réussi à résoudre quatre problèmes sur six, avec des performances équivalentes à celles d’une médaille d’argent. Dans cet article, nous explorerons comment ces systèmes fonctionnent pour résoudre des problèmes mathématiques.

AlphaProof : combiner l'IA et le langage formel pour la preuve de théorèmes mathématiques

AlphaProof est un système d'IA conçu pour prouver des énoncés mathématiques en utilisant le langage formel "Lean". Il intègre GEMINI, un modèle de langage pré-entraîné, avec AlphaZero, un algorithme d'apprentissage par renforcement réputé pour maîtriser les échecs, le shogi et le Go.

Le modèle Gemini traduit les énoncés de problèmes en langage naturel en énoncés formels, créant ainsi une bibliothèque de problèmes avec différents niveaux de difficulté. Cela sert deux objectifs : convertir un langage naturel imprécis en un langage formel précis pour vérifier des preuves mathématiques et utiliser les capacités prédictives de Gemini pour générer une liste de solutions possibles avec une précision de langage formel.

Lorsqu'AlphaProof rencontre un problème, il génère des solutions potentielles et recherche des étapes de preuve dans Lean pour les vérifier ou les réfuter. Il s'agit essentiellement d'une approche neuro-symbolique, dans laquelle le réseau neuronal Gemini traduit les instructions du langage naturel dans le langage formel symbolique Lean pour prouver ou réfuter l'affirmation. Semblable au mécanisme d'auto-jeu d'AlphaZero, où le système apprend en jouant contre lui-même, AlphaProof s'entraîne en tentant de prouver des énoncés mathématiques. Chaque tentative de preuve affine le modèle de langage d'AlphaProof, avec des preuves réussies renforçant la capacité du modèle à résoudre des problèmes plus difficiles.

Pour l'Olympiade mathématique internationale (OMI), AlphaProof a été formé en prouvant ou en réfutant des millions de problèmes couvrant différents niveaux de difficulté et sujets mathématiques. Cette formation s'est poursuivie pendant le concours, où AlphaProof a peaufiné ses solutions jusqu'à trouver des réponses complètes aux problèmes.

AlphaGeometry 2 : Intégrer des LLM et l'IA symbolique pour résoudre des problèmes de géométrie

AlphaGeometry 2 est la dernière itération du AlphaGéométrie série, conçue pour résoudre les problèmes géométriques avec une précision et une efficacité accrues. S'appuyant sur les fondations de son prédécesseur, AlphaGeometry 2 utilise une approche neuro-symbolique qui fusionne de grands modèles de langage neuronaux (LLM) avec l'IA symbolique. Cette intégration combine une logique basée sur des règles avec la capacité prédictive des réseaux de neurones à identifier des points auxiliaires, essentiels à la résolution de problèmes de géométrie. Le LLM en AlphaGeometry prédit de nouvelles constructions géométriques, tandis que l'IA symbolique applique une logique formelle pour générer des preuves.

Face à un problème géométrique, le LLM d'AlphaGeometry évalue de nombreuses possibilités, prédisant les constructions cruciales pour la résolution du problème. Ces prédictions constituent des indices précieux, guidant le moteur symbolique vers des déductions précises et se rapprochant d’une solution. Cette approche innovante permet à AlphaGeometry de relever des défis géométriques complexes qui vont au-delà des scénarios conventionnels.

Une amélioration clé d’AlphaGeometry 2 est l’intégration du Gemini LLM. Ce modèle est formé à partir de zéro sur beaucoup plus de données synthétiques que son prédécesseur. Cette formation approfondie lui permet de traiter des problèmes de géométrie plus difficiles, notamment ceux impliquant des mouvements d'objets et des équations d'angles, de rapports ou de distances. De plus, AlphaGeometry 2 dispose d'un moteur symbolique qui fonctionne deux fois plus rapidement, lui permettant d'explorer des solutions alternatives à une vitesse sans précédent. Ces avancées font d'AlphaGeometry 2 un outil puissant pour résoudre des problèmes géométriques complexes, établissant ainsi une nouvelle norme dans le domaine.

AlphaProof et AlphaGeometry 2 à l'OMI

Cette année, à l'Olympiade internationale de mathématiques (OMI), les participants ont été testés sur six problèmes divers : deux en algèbre, un en théorie des nombres, un en géométrie et deux en combinatoire. Chercheurs Google traduit ces problèmes en langage mathématique formel pour AlphaProof et AlphaGeometry 2. AlphaProof a abordé deux problèmes d'algèbre et un problème de théorie des nombres, y compris le problème le plus difficile du concours, résolu par seulement cinq candidats humains cette année. Pendant ce temps, AlphaGeometry 2 a résolu avec succès le problème de géométrie, sans toutefois résoudre les deux défis combinatoires.

Chaque problème à l'OMI vaut sept points, pour un maximum de 42. AlphaProof et AlphaGeometry 2 ont obtenu 28 points, obtenant des scores parfaits pour les problèmes qu'ils ont résolus. Cela les a placés au sommet de la catégorie des médailles d’argent. Cette année, le seuil de la médaille d'or était de 29 points, atteint par 58 des 609 concurrents.

Prochaine étape : le langage naturel pour les défis mathématiques

AlphaProof et AlphaGeometry 2 ont présenté des progrès impressionnants dans les capacités de résolution de problèmes mathématiques de l'IA. Cependant, ces systèmes s'appuient toujours sur des experts humains pour traduire les problèmes mathématiques en langage formel en vue du traitement. De plus, on ne sait pas clairement comment ces compétences mathématiques spécialisées pourraient être intégrées à d’autres systèmes d’IA, par exemple pour explorer des hypothèses, tester des solutions innovantes à des problèmes de longue date et gérer efficacement les aspects chronophages des preuves.

Pour surmonter ces limitations, les chercheurs de Google développent un système de raisonnement en langage naturel basé sur Gemini et leurs dernières recherches. Ce nouveau système vise à améliorer les capacités de résolution de problèmes sans nécessiter de traduction linguistique formelle et est conçu pour s'intégrer facilement à d'autres systèmes d'IA.

En résumé

La performance d'AlphaProof et d'AlphaGeometry 2 à l'Olympiade mathématique internationale constitue un bond en avant notable dans la capacité de l'IA à aborder un raisonnement mathématique complexe. Les deux systèmes ont démontré des performances de niveau médaille d'argent en résolvant quatre problèmes difficiles sur six, démontrant ainsi des progrès significatifs en matière de preuve formelle et de résolution de problèmes géométriques. Malgré leurs réalisations, ces systèmes d’IA dépendent toujours de l’apport humain pour traduire les problèmes en langage formel et sont confrontés à des défis d’intégration avec d’autres systèmes d’IA. Les recherches futures visent à améliorer davantage ces systèmes, en intégrant potentiellement le raisonnement en langage naturel pour étendre leurs capacités à un plus large éventail de défis mathématiques.