L’IA de DeepMind résout des problèmes de l’Olympiade internationale de mathématiques au niveau médaille d’argent
(deepmind.google)- Lors de l’IMO 2024, référence majeure pour le raisonnement mathématique de haut niveau, AlphaProof et AlphaGeometry 2 de Google DeepMind ont résolu 4 problèmes sur 6, permettant à une IA d’atteindre pour la première fois un niveau équivalent à la médaille d’argent
- Le système a obtenu 28 points sur 42 au total, avec la note maximale sur chacun des problèmes résolus, à seulement 1 point du seuil de la médaille d’or en 2024, fixé à 29 points
- L’évaluation a été menée par des mathématiciens selon les règles de notation de l’IMO ; AlphaProof s’est chargé de l’algèbre et de la théorie des nombres, tandis qu’AlphaGeometry 2 a traité la géométrie, en combinant ainsi des approches de raisonnement différentes
- Les problèmes ont d’abord été traduits manuellement en langage mathématique formel ; alors que les élèves disposent de deux sessions de 4,5 heures, le système a mis quelques minutes pour un problème et jusqu’à 3 jours pour les autres
- Ce résultat montre que l’IA mathématique va au-delà du simple calcul pour s’attaquer à la recherche et à la vérification de preuves, même si l’entrée formalisée et les longs temps de résolution restent des limites importantes
Résultat au niveau médaille d’argent à l’IMO 2024
- Google DeepMind a présenté son système de raisonnement mathématique AlphaProof et AlphaGeometry 2, version améliorée de son système de résolution de problèmes de géométrie
- Les deux systèmes ont résolu 4 des 6 problèmes de l’International Mathematical Olympiad 2024
- AlphaProof : 2 problèmes d’algèbre et 1 problème de théorie des nombres résolus
- AlphaGeometry 2 : démonstration d’1 problème de géométrie
- Les 2 problèmes de combinatoire n’ont pas été résolus
- Chaque problème vaut 7 points, pour un total de 42 points
- Le système a obtenu la note maximale sur les 4 problèmes résolus, soit 28 points
- Cela correspond au haut de la fourchette de la médaille d’argent à l’IMO 2024
- Le seuil de la médaille d’or en 2024 était de 29 points, et 58 participants sur 609 l’ont atteint lors de la compétition officielle
- C’est la première fois qu’un système d’IA obtient à l’IMO un résultat correspondant à un niveau de médaillé d’argent
Méthode d’évaluation et conditions de résolution
- Les problèmes utilisés sont ceux fournis par les organisateurs de l’IMO
- Les réponses ont été évaluées selon les règles d’attribution des points de l’IMO
- Les évaluateurs étaient Prof Sir Timothy Gowers, médaillé d’or de l’IMO et lauréat de la médaille Fields, ainsi que Dr Joseph Myers, double médaillé d’or de l’IMO et président du Problem Selection Committee de l’IMO 2024
- Pour permettre au système de comprendre les problèmes, tous ont d’abord été traduits manuellement en langage mathématique formel
- Dans la compétition officielle, les élèves soumettent leurs réponses sur deux sessions de 4,5 heures
- Le système d’IA a résolu un problème en quelques minutes, tandis que les autres ont demandé jusqu’à 3 jours
- Parmi les problèmes résolus par AlphaProof figurait le plus difficile de l’IMO 2024, que seuls 5 participants ont réussi à résoudre
AlphaProof : raisonnement formel basé sur Lean
- AlphaProof est un système entraîné à démontrer des propositions mathématiques dans le langage formel de Lean
- Il combine un modèle de langage préentraîné avec l’algorithme d’apprentissage par renforcement AlphaZero
- AlphaZero est l’algorithme utilisé pour apprendre seul les échecs, le shogi et le Go
- L’utilisation d’un langage formel permet de vérifier précisément la validité de preuves incluant du raisonnement mathématique
- Jusqu’ici, les données de preuves formelles rédigées par des humains étaient très rares, ce qui limitait l’usage des langages formels en machine learning
- Les approches fondées sur le langage naturel peuvent exploiter bien plus de données, mais elles peuvent aussi produire des étapes intermédiaires ou des réponses plausibles en apparence, mais incorrectes
- DeepMind a affiné un modèle Gemini pour traduire automatiquement des problèmes en langage naturel en propositions formelles, et a constitué une bibliothèque de problèmes formels de difficulté variée
- Lorsqu’un problème est donné, AlphaProof génère des candidats de solution, puis explore dans Lean les étapes de preuve possibles afin de les prouver ou de les réfuter
- Les preuves découvertes et vérifiées servent à renforcer le modèle de langage d’AlphaProof
- Ce processus itératif est utilisé pour améliorer sa capacité à résoudre des problèmes plus difficiles
- Dans la préparation à l’IMO, le système s’est entraîné pendant plusieurs semaines en prouvant ou réfutant des millions de problèmes
- Pendant la compétition également, une boucle d’apprentissage a été utilisée pour renforcer les preuves sur des variantes auto-générées des problèmes afin de trouver une solution complète
AlphaGeometry 2 : extension à des problèmes de géométrie plus difficiles
- AlphaGeometry 2 est une version très améliorée de AlphaGeometry
- Le système repose sur une architecture hybride neuro-symbolique combinant réseau neuronal et raisonnement symbolique
- Le modèle de langage est basé sur Gemini
- Il a été entraîné depuis zéro avec un volume de données synthétiques supérieur d’un ordre de grandeur à celui de la version précédente
- Grâce à davantage de données et à un modèle amélioré, il peut traiter des problèmes de géométrie plus difficiles impliquant le mouvement d’objets, ainsi que des équations d’angles, de rapports et de distances
- Le moteur symbolique d’AlphaGeometry 2 est plus rapide de plusieurs dizaines de fois que celui de la version précédente
- Face à un nouveau problème, un nouveau mécanisme de partage des connaissances lui permet d’exploiter des combinaisons avancées entre différents arbres de recherche pour traiter des problèmes plus complexes
- Taux de résolution des problèmes de géométrie de l’IMO sur les 25 dernières années :
- Avant la compétition 2024, AlphaGeometry 2 pouvait résoudre 83 % des problèmes de géométrie de l’IMO sur les 25 dernières années
- Le taux de résolution d’AlphaGeometry était de 53 %
- À l’IMO 2024, il a résolu la Problem 4 en 19 secondes après formalisation de l’entrée
Raisonnement en langage naturel et usages futurs
- Dans le cadre du travail autour de l’IMO, DeepMind a aussi expérimenté un système de raisonnement en langage naturel basé sur Gemini et sur des recherches récentes
- Ce système n’a pas besoin de traduire les problèmes en langage formel et peut être combiné à d’autres systèmes d’IA
- Cette approche a aussi été testée sur les problèmes de l’IMO 2024, avec des résultats jugés prometteurs
- La méthodologie plus technique d’AlphaProof est publiée dans un article de Nature
- DeepMind vise un futur dans lequel les mathématiciens pourront explorer des hypothèses avec des outils d’IA, tenter de nouvelles approches sur d’anciens problèmes et accélérer les parties les plus chronophages des démonstrations
3 commentaires
Plus il y aura de mathématiciens contribuant au développement de bibliothèques de mathématiques formelles, plus il sera facile de créer une IA mathématique performante. À ma connaissance, il y a actuellement trois Coréens qui transfèrent vers Mathlib, la bibliothèque mathématique de Lean, des théories mathématiques qu’ils ont eux-mêmes formalisées dans le langage de l’assistant de preuve Lean.
L’an dernier, j’ai participé un peu au travail de portage de Mathlib de Lean 3 vers Lean 4, et cette année, j’ai démontré un théorème non résolu de la bibliothèque Batteries de Lean 4.
Commentaires sur Hacker News
J’attends vraiment beaucoup de cette annonce, mais on ne voit pas bien tout ce que recouvre la phrase « d’abord, un humain a directement traduit les problèmes dans un langage mathématique formel pour que le système puisse les comprendre »
Tous les problèmes non géométriques étaient de la forme « trouver tous les X tels que... », et l’énoncé du théorème prenait la forme « montrer que l’ensemble de tous les X est {foo} »
À partir des solutions téléchargeables sur https://storage.googleapis.com/deepmind-media/DeepMind.com/B..., il est difficile de savoir si, à l’étape de traduction, c’est l’humain qui a fixé {foo} ou si l’ordinateur l’a trouvé. J’aimerais croire que l’ordinateur l’a trouvé, mais je ne vois rien qui le confirme
{1,1}, et pour P62, en fournissant dans chaque cas une preuve LeanCela arrive aussi souvent quand des humains manipulent directement des méthodes formelles, donc les chercheurs ont sans doute jugé que, que ce soit avec un LLM ou un autre outil, il fallait de toute façon auditer toutes les traductions
En revanche, on ne voit pas clairement quelle formalisation initiale a été donnée à l’agent pour rendre cette étape possible
Donc AlphaProof reçoit une certaine forme de « problème » et, quelle que soit la manière dont il a formalisé « trouver tous les X tels que... », il semble probablement générer des théorèmes candidats en Lean. Par exemple, l’ensemble pourrait être de la forme
{n: P(n)}pour une certaine formule P. Ensuite il explore la preuveSi AlphaProof n’a pas trouvé {foo} mais l’a reçu d’avance, alors prétendre qu’il a résolu le problème semblerait assez absurde. Cela dit, ce résultat me rend quand même très enthousiaste
C’est clairement impressionnant, mais il faut garder quelques réserves quand on parle de l’IMO. Les médailles sont attribuées aux participants, c’est-à-dire à des lycéens, à hauteur de 50 %, et le ratio or/argent/bronze est de 1:2:3, donc les médaillés d’or ou d’argent représentent le top 25 % de tous les participants
On peut donc dire que « l’IA a mieux résolu les problèmes de l’IMO que 75 % des élèves », ce qui est peut-être encore plus impressionnant en réalité
Mais la condition « un problème en quelques minutes, et chacun des autres en jusqu’à 3 jours » n’est pas comparable aux 9 heures accordées aux élèves, donc il est difficile d’y voir une comparaison honnête. Si les élèves avaient eux aussi eu jusqu’à 15 jours au lieu de 9 heures, davantage de personnes auraient probablement atteint ou dépassé ce score
En pratique, l’IA n’a en quelque sorte résolu qu’un seul problème dans les 9 heures imparties aux élèves, donc elle aurait probablement été loin d’une médaille. Pas sûr qu’il faille brouiller un résultat déjà impressionnant avec une comparaison entre des pommes et des oranges
Plus objectivement, il suffirait d’indiquer qu’elle a résolu X % des problèmes en prenant plus de temps, ou qu’elle a obtenu X points sur N
Le temps n’est pas un axe très intéressant ici. Les humains n’utilisent pas un CPU équivalent à un immense cluster de GPU. La question binaire plus intéressante est : « peut-on atteindre la solution avec suffisamment de ressources ? », et pour GPT/Claude, la réponse était clairement non
C’était très proche du seuil, et en général une petite avancée suffit déjà pour obtenir 1 point. Mais il aurait sans doute été malvenu, pour des raisons techniques, de publier des articles disant que cela avait décroché l’or, donc ils semblent s’être contentés d’un argent sans controverse
C’est du sérieux. AlphaGeometry résolvait un ensemble de problèmes très limité grâce à beaucoup de recherche brute-force
Cette fois, l’approche est bien plus large, et je pense qu’elle va fortement influencer la manière de faire des mathématiques. On passe des mathématiques en langage naturel aux mathématiques formalisées, puis à une implémentation réelle d’un pipeline auto-alimenté capable d’entraîner à la fois la formalisation et la preuve
En principe, ce pipeline pourrait aussi apprendre la construction théorique élémentaire, comme la génération de définitions auxiliaires et de lemmes auxiliaires. C’est proche du Graal de l’assistance à la preuve, et je pense que cela permettra de formaliser la plupart des mathématiques que nous produisons naturellement. Les humains travailleront de façon naturellement rigoureuse a posteriori, et les machines aideront à compléter les détails
À l’inverse, ce type de formalisation ouverte était un domaine où les progrès étaient très lents et graduels. Je travaillais dans un domaine voisin il y a 5 ans, et on peut considérer que ce résultat est hors d’atteinte des techniques traditionnelles de raisonnement automatique
La véritable démonstration automatique de théorèmes est utile bien au-delà des mathématiques pures. Par exemple, on peut écrire la sémantique axiomatique d’un petit langage de programmation en Lean et poser des questions du type « montrer qu’il existe un programme satisfaisant cette spécification »
Si cette approche passe à l’échelle, elle sera plus importante que n’importe quelle application de machine learning apparue ces dernières années
L’évolution qui nous a produits fonctionne elle aussi par une immense recherche faite d’essais quasi brute-force, et la recherche selon la méthode scientifique est fondamentalement une forme de recherche
https://leandojo.org/
https://machine-learning-for-theorem-proving.github.io/
https://www.youtube.com/watch?v=P5ew0BrRm_I
https://paperswithcode.com/task/automated-theorem-proving
https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
https://github.com/RiccardoBiosas/LeanGPT
Pour faire quelque chose d’utile, il n’est pas nécessaire de démontrer des problèmes extrêmement difficiles. Souvent, il suffit de prouver des choses simples. Si l’on demande à un modèle de langage d’accomplir une tâche, de trier des éléments, de coordonner un planning, d’écrire du code qui fait X, etc., il est difficile de faire immédiatement confiance au résultat ; mais si le système peut traduire une partie du problème en logique et trouver une solution, cela devient bien plus fiable
Le point clé est un peu passé au second plan, mais ils utilisent Lean
C’est important bien au-delà des problèmes de maths. Forcer des modèles de machine learning à se confronter à un système de preuve est un bon moyen d’éviter le bullshit générique
J’espère que davantage de gens écriront des types dans Lean ou des systèmes similaires et s’en serviront comme d’une bien meilleure manière d’écrire des prompts
polyrith. J’ai aussi vu AlphaProof utilisernlinarithTim Gowers a publié un bon petit aperçu qui explique les principales réserves et remet le tout en contexte. C’est un médaillé Fields et il a aussi participé à ce travail : https://x.com/wtgowers/status/1816509803407040909
C’est vrai, mais intégrer l’équipe nationale de chaque pays est déjà en soi un processus extrêmement difficile. Olympiades régionales de mathématiques, olympiades nationales de mathématiques : à chaque étape, la sélection est impitoyable
Ensuite, il y a un entraînement supplémentaire pour ce groupe d’élite, et selon les cas il peut même y avoir une sélection supplémentaire
En bref, être sélectionné dans une équipe nationale IMO est déjà un immense accomplissement, et y décrocher l’or ou l’argent relève d’une réussite tout simplement extraordinaire
Source : un ami qui a obtenu une médaille d’argent à l’IMO
J’envie vraiment les gens qui sont payés pour faire ce genre de travail. Ça a l’air extrêmement amusant, et pousser ainsi l’état de l’art doit être très satisfaisant
Pour la satisfaction au travail, je pense que l’environnement de travail compte davantage que le sujet. Même si on travaille sur un sujet censé changer le monde, si l’équipe est catastrophique, on passe un mauvais moment. Certaines personnes ont un talent pour aspirer tout le plaisir, et la politique interne existe partout, en particulier sur les sujets qui sont censés changer le monde
À l’inverse, même un sujet qui paraît des plus ennuyeux, comme mettre des données clients dans une base de données, peut offrir une excellente expérience avec une équipe bienveillante, une architecture bien conçue, du temps pour expérimenter et partager les connaissances. J’en suis venu à apprécier de plus en plus la beauté des choses simples qui fonctionnent bien. C’est parfois plus rare qu’une percée scientifique
Bien sûr, on peut aussi avoir à la fois un excellent environnement de travail et un excellent sujet, et là c’est quasiment le jackpot, donc oui, il y a de quoi envier
Je devrais sans doute être enthousiaste et reconnaissant de pouvoir faire ce travail, mais des outils médiocres enlèvent une bonne partie du plaisir
(/s)
Cela fait des décennies que les machines jouent mieux aux échecs que les humains
Et pourtant, personne ne s’en soucie. Tout le monde est occupé à regarder Magnus Carlsen
Nous sommes humains, donc nous nous intéressons à ce que font les autres humains. Nous ne nous intéressons aux machines que dans la mesure où elles nous sont utiles
Ce principe s’étend largement au travail et à l’art. Tant que les humains existeront, il y aura toujours une place pour l’humain dans ces domaines
En revanche, il est très douteux qu’il reste, dans un avenir proche, des mathématiciens publiant des progrès mathématiques nouveaux que l’IA n’aura pas déjà découverts en majorité ou en totalité. On pourra peut-être encore attribuer le mérite d’une preuve à un humain au motif qu’il a posé la première question, mais il y a peu de chances que le monde insiste pour que des humains résolvent plus lentement et plus cher ce que les ordinateurs peuvent résoudre facilement de façon significative
Ce principe s’applique clairement à l’art, mais au travail seulement en partie, ou dans la plupart des cas
Dans ce cas, nul besoin de comprendre la preuve, et personne ne se soucie de savoir si quelque mathématicien, quelque part, la comprend entièrement. Que les machines soient meilleures que nous pour trouver et vérifier des preuves devient alors non seulement acceptable, mais prévisible
Peu de mathématiciens auront envie de consacrer leur vie à ce genre de travail. Cela dit, il y a encore un grand écart entre l’IMO et la frontière de la recherche en mathématiques
J’ai toujours pensé que la démonstration automatique de théorèmes serait résolue bien avant l’AGI, parce que c’est un jeu en solo avec un espace de recherche absurdement vaste
Personnellement, je pense que les plus grands contributeurs à AlphaProof sont les gens derrière Lean et Mathlib. Parce qu’ils ont pris en charge la tâche titanesque de formaliser l’ensemble des mathématiques
Le manque de formalisation des articles de mathématiques a continuellement fait échouer les tentatives d’automatisation, parce que les chercheurs en IA devaient lutter contre tout ce qu’il y a d’humain chez les auteurs : notation propre à chacun, connaissances implicites, étapes de preuve omises
Je considère que le terme AGI lui-même n’est pas défini, mais je ne vois pas pourquoi on s’attendrait à ce qu’il soit bien plus difficile de créer « quelque chose de généralement intelligent », c’est-à-dire une intelligence de niveau humain médian, que de créer quelque chose de « meilleur en mathématiques que Terrence Tao »
La meilleure discussion est ici : https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...
Cette meilleure discussion est disponible ici : https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learnin…