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 :
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 géométrie beaucoup plus complexes, y compris des problèmes concernant les mouvements d'objets et les équations d'angles, de rapports ou de distances.
AlphaGeometry 2 utilise un moteur symbolique deux fois plus rapide que son prédécesseur. Lorsqu'un nouveau problème est présenté, un nouveau mécanisme de partage des connaissances est utilisé pour permettre des combinaisons avancées de différents arbres de recherche afin de résoudre des problèmes plus complexes. Avant la compétition de cette année, AlphaGeometry 2 pouvait résoudre 83 % de tous les problèmes de géométrie de l'OIM des 25 dernières années, contre 53 % pour son prédécesseur. Pour OIM 2024, AlphaGeometry 2 a résolu le problème 4 en 19 secondes après avoir reçu sa formalisation.
Illustration du problème 4
Nouvelles frontières du raisonnement mathématique
Dans le cadre des travaux sur l'OIM, DeepMind annonce également avoir expérimenté un système de raisonnement en langage naturel, basé sur Gemini et sur ces dernières recherches pour permettre des compétences avancées en matière de résolution de problèmes. Ce système ne nécessite pas que les problèmes soient traduits dans un langage formel et pourrait être combiné avec d'autres systèmes d'IA. Ils ont également testé cette approche sur les problèmes de l'OIM de cette année et les résultats se sont révélés très prometteurs.
DeepMind conclue en soulignant :
Nos équipes continuent d'explorer de multiples approches de l'IA pour faire progresser le raisonnement mathématique et prévoient de publier bientôt plus de détails techniques sur AlphaProof.
Nous sommes enthousiastes à l'idée d'un avenir dans lequel les mathématiciens travailleront avec des outils d'IA pour explorer des hypothèses, essayer de nouvelles approches audacieuses pour résoudre des problèmes de longue date et compléter rapidement des éléments de preuves qui prennent du temps - et où les systèmes d'IA comme Gemini deviendront plus performants en mathématiques et en raisonnement plus large.
Nous sommes enthousiastes à l'idée d'un avenir dans lequel les mathématiciens travailleront avec des outils d'IA pour explorer des hypothèses, essayer de nouvelles approches audacieuses pour résoudre des problèmes de longue date et compléter rapidement des éléments de preuves qui prennent du temps - et où les systèmes d'IA comme Gemini deviendront plus performants en mathématiques et en raisonnement plus large.
Et vous ?
Pensez-vous que ces résultats sont crédibles ou pertinents ? Quel est votre avis sur le sujet ?Voir aussi :
Google DeepMind a utilisé un grand modèle de langage pour résoudre un problème mathématique insoluble : "C'est une façon intéressante d'exploiter la puissance des LLM", déclare Terence Tao Google tente de combler les lacunes de son chatbot d'IA Bard avec des capacités mathématiques et logiques avancées, après que Bard est apparu particulièrement stupide aux yeux des premiers testeurs Une recherche sur les tâches simples montrant la décomposition du raisonnement IA dans les LLM de pointe donne OpenAI GPT-4o largement en tête, suivi d'Anthropic Claude 3 
