AlphaGeometry, le système d’IA de géométrie de niveau olympiade

AlphaGeometry : un système d’IA de géométrie de niveau olympiade

• AlphaGeometry est un système d’IA qui dépasse les approches de pointe pour résoudre des problèmes de géométrie, illustrant les progrès de l’IA dans le domaine du raisonnement mathématique.
• L’Olympiade internationale de mathématiques est devenue une arène moderne où s’affrontent les meilleurs lycéens mathématiciens du monde, et un terrain d’épreuve pour les capacités mathématiques et de raisonnement des systèmes d’IA.
• AlphaGeometry est un système d’IA capable de résoudre des problèmes de géométrie complexes à un niveau proche de celui des médaillés d’or humains des olympiades, en résolvant 25 des 30 problèmes de géométrie d’olympiade dans le temps imparti.
• Le précédent système de pointe en résolvait 10, tandis qu’un médaillé d’or humain moyen en résout 25,9.
• AlphaGeometry combine la puissance prédictive d’un modèle de langage neuronal avec un moteur de raisonnement fondé sur des règles pour mener le raisonnement nécessaire à la résolution des problèmes.
• Une méthode a été développée pour générer 100 millions d’exemples uniques, permettant d’entraîner AlphaGeometry sans démonstrations humaines.

L’approche neuro-symbolique d’AlphaGeometry

• AlphaGeometry est un système neuro-symbolique composé d’un modèle de langage neuronal et d’un moteur de raisonnement symbolique, qui collaborent pour trouver des preuves de théorèmes géométriques complexes.
• Le modèle de langage prédit rapidement des motifs généraux et des relations dans les données, mais manque de rigueur dans le raisonnement et de capacité à expliquer ses décisions.
• Le moteur de raisonnement symbolique repose sur la logique formelle et utilise des règles explicites pour parvenir à des conclusions ; il est rationnel et explicable, mais pris isolément il est « lent » et manque de souplesse face à des problèmes vastes et complexes.
• Le modèle de langage d’AlphaGeometry prédit de nouveaux éléments de construction utiles à la résolution des problèmes de géométrie et guide ainsi le moteur symbolique vers la solution.

Génération de 100 millions d’exemples de données synthétiques

• La géométrie repose sur la compréhension de l’espace, de la distance, des formes et des positions relatives, et elle est importante dans de nombreux domaines comme l’art, l’architecture et l’ingénierie.
• AlphaGeometry utilise une approche de génération de données synthétiques afin de pouvoir être entraîné dès le départ en imitant à grande échelle le processus de construction des connaissances.
• Le système génère 1 milliard de diagrammes géométriques aléatoires et dérive de manière exhaustive toutes les relations entre les points et les lignes dans chaque diagramme.
• Cet immense réservoir de données aboutit finalement à un jeu d’entraînement composé de 100 millions d’exemples uniques, après exclusion des exemples similaires.

L’IA à l’avant-garde du raisonnement mathématique

• Toutes les solutions aux problèmes d’olympiade fournies par AlphaGeometry sont vérifiées et validées par ordinateur.
• Les résultats sont comparés aux méthodes d’IA précédentes et aux performances humaines aux olympiades.
• AlphaGeometry ne s’applique qu’aux problèmes de géométrie des olympiades, mais il constitue néanmoins le tout premier modèle d’IA à atteindre à lui seul le seuil de la médaille de bronze à l’IMO.
• Ce système s’appuie sur les travaux menés par Google DeepMind et Google Research pour faire progresser le raisonnement mathématique par l’IA, de l’exploration de la beauté des mathématiques pures à la résolution de problèmes en mathématiques et en sciences à l’aide de modèles de langage.

Avis de GN⁺ :

• Les résultats d’AlphaGeometry sont importants en ce qu’ils ouvrent un nouvel horizon pour l’application de l’IA à la résolution de problèmes de géométrie.
• Ce système montre la capacité de l’IA à résoudre des problèmes mathématiques complexes, une aptitude essentielle au développement de futurs systèmes d’IA générale.
• La publication d’AlphaGeometry en open source devrait considérablement élargir les possibilités d’utilisation de l’IA dans la recherche en mathématiques et en sciences.

[GN⁺]

Réactions sur Hacker News

• Résumé des commentaires Hacker News :
  • Cette étude paraît bien plus concrète que les précédents articles de DeepMind sur les maths appliquées à l’IA. L’IA y apprend des théorèmes de géométrie et est utilisée pour trouver des preuves, en ajoutant aléatoirement des constructions géométriques pour tenter d’aboutir à une démonstration.
  • Le modèle pourrait avoir du mal à généraliser, mais l’approche neuro-symbolique semble très prometteuse. Elle relie le système 1 (outils de ML) et le système 2 (génération logique de preuves), ce qui permet un apprentissage auto-supervisé.
  • Certains se demandent à quelle fréquence le modèle de langage génère des constructions réellement utiles. L’article propose plusieurs constructions auxiliaires alternatives et les traite en parallèle pour accélérer le processus.
  • Les lecteurs remercient les auteurs d’avoir publié le code et les poids. Cela fournit une base permettant à d’autres chercheurs de poursuivre les travaux.
  • Il est intéressant de constater que le modèle Transformer utilisé est petit. L’article décrit les spécifications concrètes du Transformer.
  • Une citation d’Evan Chen confirme que les preuves générées par l’IA sont lisibles par des humains. Evan Chen est une figure bien connue de la communauté des mathématiques olympiques.
  • Certains sont surpris que l’état de l’art précédent ait déjà pu résoudre 10 de ces problèmes. Il existe donc des algorithmes pratiques pour résoudre des problèmes de géométrie plane.
  • ChatGPT n’a pas réussi à résoudre des problèmes de style IMO, mais si cette recherche est réelle, c’est une avancée majeure. Trouver des preuves géométriques est une manifestation d’intelligence, et cela semble rapprocher de l’AGI.
  • Des questions sont posées sur le système déductif utilisé pour vérifier les preuves. Les conventions de la géométrie olympique diffèrent de celles d’autres branches des mathématiques, et il n’est pas clair que cette logique puisse être formalisée sans contradiction.

Ce résumé est basé sur les commentaires de Hacker News et condense brièvement les principaux points de chaque intervention. Il couvre les avancées de la recherche sur l’IA et les démonstrations en géométrie, les caractéristiques du modèle, ainsi que le débat sur le degré de proximité de ces travaux avec l’intelligence artificielle générale (AGI).