nouvelles

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Rapport sur le cœur de la machine

Département éditorial de Machine Heart

Grâce au grand modèle Gemini et à l'algorithme d'apprentissage par renforcement AlphaZero, vous pouvez maîtriser la géométrie, l'algèbre et la théorie des nombres.

Pour l’IA, l’Olympiade mathématique n’est plus un problème.

Jeudi, l'intelligence artificielle DeepMind de Google a réalisé un exploit : utiliser l'IA pour résoudre la vraie question de l'Olympiade mathématique internationale de cette année, l'OMI, et elle n'était qu'à un pas de remporter la médaille d'or.

Le concours de l'OMI qui vient de se terminer la semaine dernière comportait six questions portant sur l'algèbre, la combinatoire, la géométrie et la théorie des nombres. Le système d'IA hybride proposé par Google a répondu correctement à quatre questions et a marqué 28 points, atteignant le niveau de la médaille d'argent.

Plus tôt ce mois-ci, le professeur titulaire de l'UCLA, Terence Tao, venait de promouvoir l'Olympiade mathématique de l'IA (AIMO Progress Award) avec un prix d'un million de dollars. De manière inattendue, le niveau de résolution de problèmes d'IA s'était amélioré à ce niveau avant juillet.

OMI, répondez aux questions simultanément et répondez correctement aux questions les plus difficiles.

L'OMI est le concours le plus ancien, le plus grand et le plus prestigieux destiné aux jeunes mathématiciens, organisé chaque année depuis 1959. Récemment, le concours de l'OMI a également été largement reconnu comme un grand défi dans le domaine de l'apprentissage automatique, devenant une référence idéale pour mesurer les capacités avancées de raisonnement mathématique des systèmes d'intelligence artificielle.

Lors du concours IMO de cette année, AlphaProof et AlphaGeometry 2 développés conjointement par l'équipe DeepMind ont réalisé une avancée majeure.

Parmi eux, AlphaProof est un système d'apprentissage par renforcement pour le raisonnement mathématique formel, et AlphaGeometry 2 est une version améliorée du système de résolution géométrique de DeepMind, AlphaGeometry.

Cette percée démontre le potentiel de l’intelligence artificielle générale (AGI) dotée de capacités avancées de raisonnement mathématique pour ouvrir de nouveaux domaines scientifiques et technologiques.

Alors, comment le système d'IA de DeepMind a-t-il participé au concours de l'OMI ?

Pour faire simple, ces problèmes mathématiques sont d’abord traduits manuellement en langage mathématique formel afin que le système d’IA puisse les comprendre. Dans le concours officiel, les candidats humains soumettent leurs réponses en deux sessions (deux jours), avec un délai de 4,5 heures pour chaque session. Le système d'IA composé d'AlphaProof+AlphaGeometry 2 a résolu un problème en quelques minutes, mais a mis trois jours pour résoudre d'autres problèmes. Cependant, si vous suivez strictement les règles, le système de DeepMind a expiré. Certaines personnes pensent que cela pourrait impliquer beaucoup de craquage par force brute.

AlphaProof a résolu deux problèmes d'algèbre et un problème de théorie des nombres en déterminant les réponses et en prouvant leur exactitude, a déclaré Google. Il s'agit notamment du problème le plus difficile de la compétition, que seuls cinq concurrents ont résolu lors de l'OMI de cette année. Et AlphaGeometry 2 prouve un problème de géométrie.

Solution donnée par l'IA : https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

Le médaillé d'or de l'OMI et médaillé Fields Timothy Gowers et le double médaillé d'or de l'OMI, le Dr Joseph Myers, président du comité de sélection des problèmes de l'OMI 2024, ont noté les solutions données par le système combiné selon les règles de notation de l'OMI.

Chacune des six questions vaut 7 points, pour un score total maximum de 42 points. Le système de DeepMind a reçu une note finale de 28, ce qui signifie que les quatre problèmes résolus ont reçu des notes parfaites, équivalentes à la note la plus élevée dans la catégorie médaille d'argent. Le seuil de médaille d'or de cette année était de 29 points, et 58 des 609 joueurs de la compétition officielle ont remporté des médailles d'or.

Ce graphique montre les performances du système d'intelligence artificielle de Google DeepMind par rapport aux concurrents humains à l'OMI 2024. Le système a marqué 28 points sur un total de 42 points, atteignant le même niveau que le médaillé d'argent de la compétition. De plus, cette année, 29 points peuvent remporter la médaille d'or.

AlphaProof : une méthode de raisonnement formel

Parmi les systèmes d'IA hybrides utilisés par Google, AlphaProof est un système auto-formé qui utilise le langage formel Lean pour prouver des énoncés mathématiques. Il combine un modèle de langage pré-entraîné avec l'algorithme d'apprentissage par renforcement AlphaZero.

Parmi eux, les langages formels offrent des avantages importants pour vérifier formellement l’exactitude des preuves du raisonnement mathématique. Jusqu’à présent, cela a été d’une utilité limitée en apprentissage automatique car la quantité de données écrites par l’homme était très limitée.

En revanche, les méthodes basées sur le langage naturel, même si elles ont accès à de plus grandes quantités de données, produisent des étapes de raisonnement intermédiaires et des solutions qui semblent raisonnables mais incorrectes.

Google DeepMind établit un pont entre ces deux domaines complémentaires en affinant le modèle Gemini pour traduire automatiquement les énoncés de problèmes en langage naturel en énoncés formels, créant ainsi une vaste bibliothèque de problèmes formels de difficulté variable.

Face à un problème mathématique, AlphaProof génère des solutions candidates puis les prouve en recherchant des étapes de preuve possibles dans Lean. Chaque solution de preuve trouvée et vérifiée est utilisée pour renforcer le modèle de langage d'AlphaProof et améliorer sa capacité à résoudre des problèmes ultérieurs plus difficiles.

Pour former AlphaProof, Google DeepMind a prouvé ou réfuté des millions de problèmes mathématiques couvrant un large éventail de difficultés et de sujets au cours des semaines précédant le concours de l'OMI. Une boucle d'entraînement est également appliquée pendant la compétition pour renforcer la preuve des variantes de problèmes de compétition auto-générées jusqu'à ce qu'une solution complète soit trouvée.

Infographie sur le processus de boucle de formation d'apprentissage par renforcement AlphaProof : environ un million de problèmes mathématiques informels sont traduits en langage mathématique formel par le réseau formel. Le solveur recherche ensuite dans le réseau des preuves ou des réfutations du problème, s'entraînant progressivement à résoudre des problèmes plus difficiles à l'aide de l'algorithme AlphaZero.

AlphaGeometry 2 plus compétitif

AlphaGeometry 2 est une version considérablement améliorée d'AlphaGeometry, l'IA mathématique parue dans le magazine Nature cette année. Il s'agit d'un système hybride neuro-symbolique dans lequel le modèle de langage est basé sur Gemini et formé à partir de zéro sur un ordre de grandeur plus de données synthétiques que son prédécesseur. Cela aide le modèle à résoudre des problèmes géométriques plus complexes, notamment ceux concernant le mouvement des objets et les équations d'angles, de proportions ou de distances.

AlphaGeometry 2 dispose d'un moteur symbolique deux fois plus rapide que son prédécesseur. Lorsque de nouveaux problèmes sont rencontrés, de nouveaux mécanismes de partage des connaissances permettent des combinaisons avancées de différents arbres de recherche pour résoudre des problèmes plus complexes.

Avant le concours de cette année, AlphaGeometry 2 pouvait résoudre 83 % de tous les problèmes de géométrie historiques de l'OMI au cours des 25 dernières années, contre seulement 53 % de son prédécesseur. Dans IMO 2024, AlphaGeometry 2 a résolu le problème 4 dans les 19 secondes suivant sa formalisation.

Un exemple de la question 4 nécessite de prouver que la somme de ∠KIL et ∠XPY est égale à 180°. AlphaGeometry 2 propose de construire le point E sur la droite BI tel que ∠AEB = 90°. Le point E aide à donner une signification au milieu L du segment de droite AB, créant ainsi de nombreuses paires de triangles similaires, tels que ABE ~ YBI et ALE ~ IPC, pour prouver la conclusion.

Google DeepMind rapporte également que dans le cadre des travaux de l'OMI, les chercheurs expérimentent également un nouveau système de raisonnement en langage naturel basé sur Gemini et un système de raisonnement en langage naturel de pointe, dans l'espoir d'obtenir des capacités avancées de résolution de problèmes. Le système ne nécessite pas de traduction des questions dans un langage formel et peut être combiné avec d'autres systèmes d'IA. Lors du test des questions du concours de l'OMI de cette année, il "a montré un grand potentiel".

Google continue d'explorer les méthodes d'IA pour faire progresser le raisonnement mathématique et prévoit de publier prochainement plus de détails techniques sur AlphaProof.

Nous sommes enthousiasmés par un avenir dans lequel les mathématiciens utiliseront les 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 chronophages - et des systèmes d'IA comme Gemini feront une différence en mathématiques. et plus encore. L’aspect général du raisonnement devient encore plus puissant.

l'équipe de recherche

Google a déclaré que la nouvelle recherche était soutenue par l'Olympiade mathématique internationale et en outre :

Le développement d'AlphaProof a été dirigé par Thomas Hubert, Rishi Mehta et Laurent Sartran. Parmi les principaux contributeurs figurent Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland et Grace Margand.

Parmi eux, Aja Huang, Julian Schrittwieser, Yannick Schroecker et d'autres membres étaient également des membres principaux du journal AlphaGo il y a 8 ans (2016). Il y a huit ans, AlphaGo, qu'ils ont construit sur la base de l'apprentissage par renforcement, est devenu célèbre. Huit ans plus tard, l’apprentissage par renforcement brille à nouveau dans AlphaProof. Quelqu'un a déploré dans le cercle d'amis : RL est tellement de retour !

Les travaux d'AlphaGeometry 2 et d'inférence en langage naturel sont dirigés par Thang Luong. Le développement d'AlphaGeometry 2 a été dirigé par Trieu Trinh et Yuri Chervonyi, avec d'importantes contributions de Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang et Marcelo Menegali.

De plus, David Silver, Quoc Le, Hassabis et Pushmeet Kohli sont responsables de la coordination et de la gestion de l'ensemble du projet.

Contenu de référence :

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/