L’IA au concours international de mathématiques : Comment AlphaProof et AlphaGeometry 2 ont atteint le niveau de médaille d’argent

La raison mathématique est un aspect vital des capacités cognitives humaines, qui impulse 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 égale la cognition humaine, il est essentiel de doter l’IA de capacités de raisonnement mathématique avancées. Bien que les systèmes d’IA actuels puissent résoudre des problèmes mathématiques de base, ils ont du mal avec le raisonnement complexe nécessaire pour les disciplines mathématiques avancées comme l’algèbre et la géométrie. Cependant, cela pourrait changer, car Google DeepMind a fait des progrès significatifs dans l’amélioration des capacités de raisonnement mathématique d’un système d’IA. Cette avancée a été réalisée au concours international de mathématiques (IMO) 2024. Créé en 1959, l’IMO est le plus ancien et le plus prestigieux concours de mathématiques, qui met au défi les élèves du secondaire 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 concourent pour résoudre six problèmes très difficiles. Cette année, Google DeepMind a présenté deux systèmes d’IA : AlphaProof, qui se concentre sur le raisonnement mathématique formel, et AlphaGeometry 2, qui se spécialise dans la résolution de problèmes géométriques. Ces systèmes d’IA ont réussi à résoudre quatre des six problèmes, performant au niveau d’un médaillé d’argent. Dans cet article, nous allons explorer comment ces systèmes fonctionnent pour résoudre des problèmes mathématiques.

AlphaProof : Combinaison de l’IA et du 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 avoir maîtrisé 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 une bibliothèque de problèmes avec des niveaux de difficulté variés. Cela sert deux objectifs : convertir le langage naturel imprécis en langage formel précis pour vérifier les 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.

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

Pour le concours international de mathématiques (IMO), AlphaProof a été entraîné en prouvant ou en réfutant des millions de problèmes couvrant différents niveaux de difficulté et des sujets mathématiques. Cette formation s’est poursuivie pendant la compétition, où AlphaProof a affiné ses solutions jusqu’à ce qu’il trouve des réponses complètes aux problèmes.

AlphaGeometry 2 : Intégration de LLM et d’IA symbolique pour la résolution de problèmes géométriques

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

Lorsqu’il est confronté à un problème géométrique, le LLM d’AlphaGeometry évalue de nombreuses possibilités, prédit des constructions cruciales pour la résolution du problème. Ces prédictions servent de précieuses indices, guidant le moteur symbolique vers des déductions précises et avançant vers une solution. Cette approche innovante permet à AlphaGeometry de relever des défis géométriques complexes qui dépassent les scénarios conventionnels.

Une des améliorations clés d’AlphaGeometry 2 est l’intégration du LLM Gemini. Ce modèle est formé à partir de zéro sur beaucoup plus de données synthétiques que son prédécesseur. Cette formation intensive lui permet de gérer des problèmes géométriques plus difficiles, y compris ceux qui impliquent des mouvements d’objets et des équations d’angles, de ratios ou de distances. De plus, AlphaGeometry 2 dispose d’un moteur symbolique qui fonctionne deux ordres de grandeur plus rapidement, lui permettant d’explorer des solutions alternatives avec une vitesse sans précédent. Ces progrès font d’AlphaGeometry 2 un outil puissant pour résoudre des problèmes géométriques complexes, établissant un nouveau standard dans le domaine.

AlphaProof et AlphaGeometry 2 à l’IMO

Cette année, au concours international de mathématiques (IMO), les participants ont été testés avec six problèmes divers : deux en algèbre, un en théorie des nombres, un en géométrie et deux en combinatoire. Les chercheurs de Google ont traduit ces problèmes en langage mathématique formel pour AlphaProof et AlphaGeometry 2. AlphaProof a résolu deux problèmes d’algèbre et un problème de théorie des nombres, y compris le problème le plus difficile de la compétition, résolu par seulement cinq concurrents humains cette année. Pendant ce temps, AlphaGeometry 2 a résolu avec succès le problème de géométrie, bien qu’il n’ait pas résolu les deux défis de combinatoire.

Chaque problème à l’IMO vaut sept points, pour un total maximum de 42 points. AlphaProof et AlphaGeometry 2 ont obtenu 28 points, réalisant des scores parfaits sur les problèmes qu’ils ont résolus. Cela les a placés à la limite supérieure de la catégorie de médaille d’argent. Le seuil de médaille d’or cette année était de 29 points, atteint par 58 des 609 concurrents.

Prochain bond : Langage naturel pour les défis mathématiques

AlphaProof et AlphaGeometry 2 ont montré des progrès impressionnants dans les capacités de résolution de problèmes mathématiques de l’IA. Cependant, ces systèmes dépendent encore de l’expertise humaine pour traduire les problèmes mathématiques en langage formel pour le traitement. De plus, il est peu clair comment ces compétences mathématiques spécialisées pourraient être intégrées dans d’autres systèmes d’IA, tels que l’exploration d’hypothèses, la mise à l’essai de solutions innovantes à des problèmes persistants et la gestion efficace des aspects chronophages des preuves.

Pour surmonter ces limites, 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 de langage formel et est conçu pour s’intégrer en douceur avec d’autres systèmes d’IA.

En résumé

La performance d’AlphaProof et d’AlphaGeometry 2 au concours international de mathématiques est un saut notable en avant dans la capacité de l’IA à résoudre des problèmes mathématiques complexes. Les deux systèmes ont démontré des performances au niveau de la médaille d’argent en résolvant quatre des six problèmes difficiles, montrant des progrès significatifs dans la preuve formelle et la résolution de problèmes géométriques. Malgré leurs réalisations, ces systèmes d’IA dépendent encore de l’entrée humaine pour la traduction des problèmes en langage formel et font face à des défis d’intégration avec d’autres systèmes d’IA. Les recherches futures visent à améliorer ces systèmes, en intégrant potentiellement le raisonnement en langage naturel pour étendre leurs capacités à un éventail plus large de défis mathématiques.