
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 :
Nous avons beaucoup progressé dans la construction de systèmes d'IA qui aident les mathématiciens à découvrir de nouvelles idées, de nouveaux algorithmes et des réponses à des problèmes ouverts. Mais les systèmes d'IA actuels ont encore du mal à résoudre des problèmes mathématiques généraux en raison des limites des capacités de raisonnement et des données d'entraînement.
Aujourd'hui, nous présentons AlphaProof, un nouveau système basé sur l'apprentissage par renforcement pour le raisonnement mathématique formel, et AlphaGeometry 2, une version améliorée de notre système de résolution de géométrie. Ensemble, ces systèmes ont résolu quatre des six problèmes de l'Olympiade internationale de mathématiques (OIM) de cette année, atteignant pour la première fois le même niveau qu'un médaillé d'argent dans la compétition.
Aujourd'hui, nous présentons AlphaProof, un nouveau système basé sur l'apprentissage par renforcement pour le raisonnement mathématique formel, et AlphaGeometry 2, une version améliorée de notre système de résolution de géométrie. Ensemble, ces systèmes ont résolu quatre des six problèmes de l'Olympiade internationale de mathématiques (OIM) de cette année, atteignant pour la première fois le même niveau qu'un médaillé d'argent dans la compétition.
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 :
Le fait que le programme puisse proposer une construction non évidente comme celle-ci est très impressionnant et va bien au-delà de ce que je pensais être l'état de l'art.
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.
Les performances de l'IA par rapport aux concurrents humains à l'OIM 2024
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 :
Nous avons entraîné AlphaProof pour l'OIM en prouvant ou en réfutant des millions de problèmes, couvrant un large éventail de difficultés et de sujets mathématiques sur une période de plusieurs semaines précédant la compétition. La boucle d'entraînement a également été appliquée pendant le concours, en renforçant les preuves des variations auto-générées des problèmes du concours jusqu'à ce qu'une solution complète puisse être trouvée.
Processus d'apprentissage par renforcement d'AlphaProof
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...
La fin de cet article est réservée aux abonnés. Soutenez le Club Developpez.com en prenant un abonnement pour que nous puissions continuer à vous proposer des publications.