L'IA obtient la médaille d'argent en résolvant les problèmes des Olympiades internationales de mathématiques

Avec les systèmes AlphaProof et AlphaGeometry 2 de Google DeepMind

Google DeepMind annonce que ses modèles AlphaProof et AlphaGeometry 2 ont permis à l'IA d'obtenir la médaille d'argent en résolvant les problèmes des Olympiades internationales de mathématiques. AlphaProof est un nouveau système d'apprentissage par renforcement pour le raisonnement mathématique formel, tandis qu'AlphaGeometry 2 est un système de résolution de géométrie. Les systèmes d'IA ont résolu un problème en quelques minutes et ont mis jusqu'à trois jours pour résoudre les autres.

L'intelligence artificielle (IA), dans son sens le plus large, est l'intelligence dont font preuve les machines, en particulier les systèmes informatiques. Les objectifs de la recherche en IA comprennent le raisonnement, la représentation des connaissances, l'apprentissage, le traitement du langage naturel, ainsi que l'intelligence artificielle générale (AGI), c'est-à-dire la capacité d'accomplir toute tâche réalisable par un humain à un niveau au moins égal. Pour atteindre ces objectifs, les chercheurs en IA ont adapté et intégré un large éventail de techniques, notamment la recherche et l'optimisation mathématique, la logique formelle, les réseaux neuronaux artificiels et les méthodes fondées sur les statistiques, la recherche opérationnelle et l'économie.

Parmi les acteurs majeurs de la recherche en IA, il y a Google DeepMind, un laboratoire de recherche en IA qui sert de filiale à Google. DeepMind a introduit les machines de Turing neuronales (réseaux neuronaux qui peuvent accéder à la mémoire externe comme une machine de Turing conventionnelle), ce qui a permis de créer un ordinateur qui ressemble vaguement à la mémoire à court terme du cerveau humain.

Avec ses modèles AlphaProof et AlphaGeometry 2, Google DeepMind annonce que l'IA a obtenu la médaille d'argent en résolvant les problèmes des Olympiades internationales de mathématiques. Cela confirme que l'intelligence artificielle générale (AGI) dotée d'un raisonnement mathématique avancé a le potentiel d'ouvrir de nouvelles frontières dans les domaines de la science et de la technologie.


DeepMind déclare pour l'annonce :

Des systèmes d'IA pour résoudre des problèmes mathématiques complexes

L'OIM est le concours le plus ancien, le plus important et le plus prestigieux pour les jeunes mathématiciens, organisé chaque année depuis 1959. Chaque année, des mathématiciens d'élite s'entraînent, parfois pendant des milliers d'heures, pour résoudre six problèmes exceptionnellement difficiles d'algèbre, de combinatoire, de géométrie et de théorie des nombres. De nombreux lauréats de la médaille Fields, l'une des plus hautes distinctions accordées aux mathématiciens, ont représenté leur pays à l'OIM.

Plus récemment, le concours annuel de l'OIM a également été largement reconnu comme un grand défi dans le domaine de l'apprentissage automatique et comme une référence idéale pour mesurer les capacités de raisonnement mathématique avancé d'un système d'intelligence artificielle. DeepMind a donc appliqué son système d'IA combiné aux problèmes du concours, fournis par les organisateurs de l'OIM. Les solutions ont été notées conformément aux règles d'attribution des points de l'OIM par d'éminents mathématiciens, le professeur Sir Timothy Gowers, médaillé d'or de l'OIM et lauréat de la médaille Fields, et le Dr Joseph Myers, deux fois médaillé d'or de l'OIM et président du comité de sélection des problèmes de l'OIM 2024.

Le professeur Sir Timothy Gowers a commenté la participation de l'IA en déclarant :


Tout d'abord, les problèmes ont été traduits manuellement en langage mathématique formel pour que les systèmes puissent les comprendre. Dans la compétition officielle, les étudiants soumettent leurs réponses en deux sessions de 4 heures et demie chacune. Les systèmes d'IA ont résolu un problème en quelques minutes et ont mis jusqu'à trois jours pour résoudre les autres.

AlphaProof a résolu deux problèmes d'algèbre et un problème de théorie des nombres en déterminant la réponse et en prouvant qu'elle était correcte. Il s'agissait notamment du problème le plus difficile de la compétition, qui n'a été résolu que par cinq concurrents lors de l'OIM de cette année. AlphaGeometry 2 a résolu le problème de géométrie, tandis que les deux problèmes de combinatoire sont restés sans réponse.

Chacun des six problèmes peut rapporter sept points, avec un maximum total de 42. Les systèmes ont obtenu un score final de 28 points, soit un score parfait pour chaque problème résolu, ce qui équivaut à l'extrémité supérieure de la catégorie de la médaille d'argent. Cette année, le seuil de la médaille d'or commence à 29 points et a été atteint par 58 des 609 participants à la compétition officielle.


AlphaProof : une approche formelle du raisonnement

AlphaProof est un système qui s'entraîne à prouver des énoncés mathématiques dans le langage formel Lean. Il associe un modèle de langage préformé à l'algorithme d'apprentissage par renforcement AlphaZero, qui s'est déjà auto-appris à maîtriser les jeux d'échecs, de shogi et de Go.

Les langages formels présentent l'avantage essentiel de permettre la vérification formelle de l'exactitude des preuves impliquant un raisonnement mathématique. Leur utilisation dans l'apprentissage automatique a toutefois été limitée par la quantité très restreinte de données humaines disponibles. En revanche, les approches basées sur le langage naturel peuvent halluciner des étapes de raisonnement et des solutions intermédiaires plausibles mais incorrectes, bien qu'elles aient accès à des ordres de grandeur de données plus importants.

Les chercheurs de DeepMind ont établi un pont entre ces deux sphères complémentaires en affinant un modèle Gemini pour traduire automatiquement les énoncés de problèmes en langage naturel en énoncés formels, créant ainsi une grande bibliothèque de problèmes formels de difficulté variable. Lorsqu'on lui présente un problème, AlphaProof génère des solutions candidates et les prouve ou les réfute en recherchant les étapes de preuve possibles dans Lean. Chaque preuve trouvée et vérifiée est utilisée pour renforcer le modèle de langage d'AlphaProof, améliorant ainsi sa capacité à résoudre des problèmes ultérieurs plus difficiles.

Les chercheurs commentent :


AlphaGeometry 2 : une version améliorée pour être plus compétitive

AlphaGeometry 2 est une version considérablement améliorée d'AlphaGeometry. Il s'agit d'un système hybride neuro-symbolique dans lequel le modèle de langage est basé sur Gemini et entraîné à partir de zéro sur un ordre de grandeur de données synthétiques plus important que son prédécesseur. Cela a permis au modèle de s'attaquer à des problèmes de...