DeepMind, le laboratoire de R&D en IA de Google, estime que la clé de systèmes IA plus performants pourrait résider dans la découverte de nouvelles méthodes pour résoudre des problèmes de géométrie délicats. Dans cet esprit, DeepMind a dévoilé aujourd’hui AlphaGeometry, un système que le laboratoire affirme capable de résoudre autant de problèmes de géométrie que le médaillé d’or moyen de l’Olympiade Internationale de Mathématiques. AlphaGeometry, dont le code a été distribué ce matin, résout 25 problèmes de géométrie de l’Olympiade dans le temps standard, battant les 10 du précédent système de pointe.
“Résoudre des problèmes de géométrie de niveau Olympiade est une étape importante dans le développement du raisonnement mathématique profond sur la voie vers des systèmes IA plus avancés et généraux”, ont écrit Trieu Trinh et Thang Luong, chercheurs scientifiques en IA chez Google, dans un billet de blog publié ce matin. “[Nous] espérons que… AlphaGeometry contribue à ouvrir de nouvelles possibilités à travers les mathématiques, la science et l’IA”. Mais pourquoi cet accent sur la géométrie ? DeepMind affirme que prouver des théorèmes mathématiques, ou expliquer logiquement pourquoi un théorème (comme le théorème de Pythagore) est vrai, nécessite à la fois du raisonnement et la capacité de choisir parmi une série d’étapes possibles vers une solution. Cette approche de résolution de problèmes pourrait, si DeepMind a raison, se révéler utile un jour dans des systèmes IA à usage général.
“Démontrer qu’une conjecture particulière est vraie ou fausse dépasse les capacités des systèmes d’IA les plus avancés d’aujourd’hui”, peut-on lire dans les documents de presse de DeepMind partagés avec TechCrunch.
“Vers cet objectif, être capable de prouver des théorèmes mathématiques… est une étape importante car cela démontre la maîtrise du raisonnement logique et la capacité à découvrir de nouvelles connaissances”. Cependant, former un système d’IA à résoudre des problèmes de géométrie pose des défis uniques. En raison des complexités de la traduction des preuves dans un format que les machines peuvent comprendre, il y a une pénurie de données d’entraînement en géométrie utilisables. Et beaucoup des modèles d’IA génératifs les plus avancés d’aujourd’hui, bien qu’excellents pour identifier les motifs et les relations dans les données, manquent de capacité à raisonner logiquement à travers les théorèmes.
La solution de DeepMind a été double. Dans la conception d’AlphaGeometry, le laboratoire a couplé un “modèle de langage neuronal” – un modèle architecturalement du genre ChatGPT – avec un “moteur déductif symbolique”, un moteur qui utilise des règles (par exemple, des règles mathématiques) pour déduire des solutions aux problèmes. En l’absence de données d’entraînement, DeepMind a créé ses propres données synthétiques, générant 100 millions de “théorèmes synthétiques” et des preuves de complexité variable. Le laboratoire a alors entrainé AlphaGeometry à partir de zéro sur les données synthétiques – et l’a évalué sur des problèmes de géométrie de l’Olympiade.
Les problèmes de géométrie de l’Olympiade sont basés sur des diagrammes auxquels il faut ajouter des “constructs” avant qu’ils puissent être résolus, comme des points, des lignes ou des cercles. Appliqué à ces problèmes, le modèle neuronal d’AlphaGeometry prédit quels constructs pourraient être utiles à ajouter – des prédictions que le moteur symbolique d’AlphaGeometry utilise pour faire des déductions sur les diagrammes pour identifier des solutions similaires. “Avec tant d’exemples montrant comment ces constructs ont conduit à des preuves, le modèle de langage d’AlphaGeometry est capable de faire de bonnes suggestions pour de nouveaux constructs lorsqu’il est présenté avec des problèmes de géométrie de l’Olympiade”, écrivent Trinh et Luong.
