Google AI manque de peu la médaille d'or aux IMO : résolution en 19 secondes stupéfie le jury, capacités géométriques surpassant l'humain

Le dernier modèle mathématique de DeepMind a obtenu une médaille d'argent aux Olympiades internationales de mathématiques (IMO), avec une performance exceptionnelle. Le modèle a parfaitement résolu 4 des 6 problèmes, manquant la médaille d'or d'un seul point. En particulier, pour le problème 4, le modèle a fourni une solution en seulement 19 secondes, une vitesse et une qualité de résolution qui ont stupéfié les juges humains.

AlphaProof

AlphaProof est un système capable de prouver des propositions mathématiques dans le langage formel Lean. Il combine un grand modèle de langage pré-entraîné avec l'algorithme d'apprentissage par renforcement AlphaZero.

Pour surmonter les limitations des langages formels dans l'apprentissage automatique en raison des données limitées écrites par l'homme, les chercheurs ont comblé le fossé entre le langage naturel et les énoncés formels en :

  1. Affinant le modèle Gemini pour traduire automatiquement les énoncés de problèmes en langage naturel en énoncés formels
  2. Créant une grande bibliothèque de problèmes formalisés de difficulté variable

Lors de la résolution de problèmes, AlphaProof génère des solutions candidates et les prouve ou les réfute en recherchant des étapes de preuve possibles dans Lean.

AlphaGeometry 2

AlphaGeometry 2 est un système hybride neuro-symbolique entraîné à partir de zéro en utilisant le modèle de langage Gemini. Il peut résoudre des problèmes de géométrie plus difficiles que son prédécesseur, y compris ceux impliquant le mouvement des objets, les angles, les ratios et les équations de distance.

Les améliorations clés comprennent :

  1. Un entraînement sur des données synthétiques d'un ordre de grandeur plus important que la version précédente
  2. Un moteur symbolique deux ordres de grandeur plus rapide qu'auparavant
  3. Un nouveau mécanisme de partage des connaissances permettant des combinaisons avancées de différents arbres de recherche pour résoudre des problèmes plus complexes

AlphaGeometry 2 a démontré des capacités impressionnantes, résolvant 83% des problèmes de géométrie des IMO des 25 dernières années, contre 53% pour son prédécesseur. Lors des IMO de cette année, il a résolu le Problème 4 en seulement 19 secondes après avoir reçu la question formalisée.

Les performances de l'IA aux IMO démontrent des progrès significatifs dans les capacités de raisonnement mathématique, rapprochant l'IA de la résolution de problèmes de niveau humain en mathématiques avancées.