AlphaGéométrie

AlphaGeometry est un programme d' intelligence artificielle (IA) capable de résoudre des problèmes complexes de géométrie euclidienne . Le système comprend un modèle de langage étendu (LLM) basé sur les données et un moteur symbolique à base de règles ( raisonnement arithmétique déductif par base de données ) . Il a été développé par DeepMind , une filiale de Google . Le programme a résolu 25 problèmes de géométrie sur 30 lors des Olympiades internationales de mathématiques (OIM), dans les délais impartis — une performance presque aussi bonne que celle d'un champion humain moyen. À titre de comparaison, le précédent programme d'IA, appelé méthode de Wu , n'avait réussi à résoudre que 10 problèmes.

DeepMind a publié un article sur AlphaGeometry dans la revue scientifique à comité de lecture Nature le 17 janvier 2024. AlphaGeometry a été présenté dans MIT Technology Review le même jour.

Les programmes de géométrie traditionnels sont des moteurs symboliques qui s'appuient exclusivement sur des règles codées manuellement pour générer des démonstrations rigoureuses, ce qui les rend peu flexibles dans les situations inhabituelles. AlphaGeometry combine un tel moteur symbolique avec un modèle de langage spécialisé de grande taille, entraîné sur des données synthétiques de démonstrations géométriques. Lorsque le moteur symbolique ne parvient pas à trouver par lui-même une démonstration formelle et rigoureuse, il sollicite le modèle de langage, qui suggère une construction géométrique pour poursuivre le raisonnement. Cependant, l'applicabilité de cette méthode à d'autres domaines des mathématiques ou du raisonnement reste incertaine, car les moteurs symboliques reposent sur des règles spécifiques à chaque domaine et nécessitent des données synthétiques.

AlphaGeometry 2 est une version améliorée d'AlphaGeometry, publiée le 5 février 2025. Elle intègre de nouvelles fonctionnalités au langage de représentation afin de décrire davantage de problèmes géométriques impliquant des mouvements d'objets, ainsi que des problèmes contenant des équations linéaires d'angles, de rapports et de distances. Conçue pour couvrir les questions de géométrie des Olympiades internationales de mathématiques (OIM) de 2000 à 2024, cette version bénéficie d'un langage de représentation étendu permettant de traiter 88 % des questions.

Il utilise Gemini, affiné sur un ensemble de données synthétiques de problèmes et de solutions dans le langage de représentation. Le modèle sert à créer des éléments auxiliaires, tels que des lignes et des points, pour faciliter la recherche dans l'arbre. Il est également utilisé pour l'autoformalisation , c'est-à-dire la conversion d'un problème en anglais en un problème dans le langage de représentation.