Le point de vue d’un mathématicien sur les capacités de l’IA en mathématiques

• Le nouveau modèle de langage o3 d’OpenAI a obtenu 25 % sur le difficile benchmark mathématique FrontierMath, relançant les interrogations sur la possibilité pour l’IA en mathématiques de dépasser le niveau universitaire de premier cycle
• FrontierMath est un jeu de données privé créé par Epoch AI, composé de centaines de problèmes mathématiques difficiles qui demandent une réponse numérique vérifiable automatiquement plutôt qu’une « démonstration de théorème »
• Les 5 exemples publiés n’étaient pas faciles même pour des mathématiciens de recherche ; Tao les a qualifiés d’« extrêmement stimulants », mais Borcherds estime que produire une réponse numérique n’équivaut pas à une démonstration originale
• Elliot Glazer d’Epoch AI a indiqué que 25 % des problèmes relevaient d’un style « IMO/premier cycle », ce qui rend difficile de savoir jusqu’à quel niveau réel correspond le score de 25 % de o3, étant donné le caractère privé du jeu de données
• Pour les mathématiciens, l’objectif le plus important reste non pas « trouver ce nombre », mais démontrer correctement un théorème et l’expliquer de façon compréhensible pour les humains ; les modèles de langage et les approches fondées sur Lean ont des limites différentes

---

o3 et FrontierMath ont bousculé la ligne de base

• o3 est le nouveau modèle de langage d’OpenAI, et il a obtenu un score de 25 % sur FrontierMath
• Depuis ChatGPT, les modèles de langage publics progressent rapidement, et leur capacité à résoudre des problèmes de mathématiques est évaluée dans ce mouvement
• FrontierMath est un jeu de données privé de problèmes mathématiques créé par Epoch AI ; le résumé de l’article indique qu’il contient « des centaines » de problèmes difficiles
• Si le jeu de données était rendu public, les modèles de langage pourraient apprendre les problèmes et les réponses ; même des informations de base comme le nombre de problèmes sont donc traitées avec prudence
  • Si les problèmes et les réponses sont publiés, le modèle peut simplement régurgiter des réponses déjà vues
  • Pour cette raison, il est difficile de vérifier de l’extérieur la difficulté réelle et la représentativité d’un benchmark privé

Format et difficulté des problèmes FrontierMath

• Les problèmes FrontierMath ressemblent davantage à « trouver ce nombre » qu’à « démontrez ce théorème »
• Les problèmes doivent avoir une réponse claire, calculable et vérifiable automatiquement
• Les réponses des 5 exemples publiés sont toutes des entiers positifs
  • Parmi les réponses d’exemple figurent 9811 et 367707
  • Les trois autres réponses sont plus grandes, afin de rendre une bonne réponse par simple hasard difficile
• Les exemples publiés ne sont pas triviaux, même pour des mathématiciens de recherche
  • L’auteur dit comprendre l’énoncé des 5 problèmes
  • Le troisième problème pouvait être résolu assez vite ; pour le cinquième, il connaissait une méthode standard utilisant les Weil conjectures for curves, mais n’a pas calculé la réponse à 13 chiffres
  • Il a estimé ne pas pouvoir résoudre les premier et deuxième problèmes ; pour le quatrième, il pensait qu’un effort pourrait mener à des progrès, mais a préféré lire l’explication
• Un étudiant de premier cycle en mathématiques, même brillant, pourrait avoir du mal à en résoudre ne serait-ce qu’un seul
  • Le premier problème semble demander au moins un niveau doctorat en théorie analytique des nombres

Les avantages et les limites d’un benchmark à réponse numérique

• La raison essentielle pour laquelle FrontierMath utilise des problèmes à réponse numérique est le coût de l’évaluation
• Pour évaluer des centaines de réponses à des questions du type « démontrez ce théorème », il faut des experts humains
  • En 2024, il semble difficile de confier cette évaluation à une machine à ce niveau
• En revanche, une liste de réponses numériques peut être comparée très rapidement par un ordinateur
• Borcherds estime que les mathématiciens de recherche passent l’essentiel de leur temps à chercher non pas des nombres, mais des preuves et des idées
• Malgré cela, FrontierMath a de la valeur pour le domaine de l’IA mathématique
  • Les jeux de données difficiles sont très rares
  • Les créer est très difficile ou coûteux
  • Un texte récent de Frieder et al. examine plus en profondeur les limites des jeux de données en IA mathématique

Pourquoi les 25 % de o3 ont surpris

• L’idée dominante jusqu’ici était que l’IA en mathématiques se situait plutôt au niveau premier cycle ou pré-premier cycle
• L’IA devient déjà très forte sur les problèmes de type olympiade résolus par des lycéens très doués
• Il semble certain que, d’ici un an, l’IA sera capable de réussir des examens universitaires de mathématiques de premier cycle
  • Les examens de premier cycle incluent souvent des problèmes standard qu’un étudiant ayant compris le cours de base peut réussir
  • Une machine peut résoudre facilement ce type de problème
• En revanche, le saut qui mène au-delà du simple recyclage d’idées standard vers des idées innovantes de niveau premier cycle avancé ou début de doctorat paraît considérable
• Les réponses récentes de ChatGPT à l’examen Putnam étaient décevantes
  • Il semble que seule la question B4 ait reçu une réponse convenable de la machine
  • La plupart des autres réponses vaudraient à peine 1 ou 2 points sur 10
• Pour ces raisons, on pensait que FrontierMath resterait pratiquement imprenable pendant encore plusieurs années

Les incertitudes laissées par un jeu de données privé

• Elliot Glazer d’Epoch AI a indiqué sur Reddit que 25 % des problèmes FrontierMath étaient de style IMO/premier cycle
• Cette affirmation semble mal correspondre aux 5 problèmes publiés
  • Le problème le plus facile parmi les exemples publics admettait déjà une approche utilisant les Weil conjectures for curves
  • Ou bien il pouvait exiger une douloureuse recherche exhaustive pour factoriser un polynôme cubique de degré 10^12 sur un corps fini
• Cette information laisse planer des doutes sur la difficulté réelle du jeu de données privé et sur le caractère représentatif des 5 problèmes publiés
• Comme le jeu de données reste privé, il est difficile de vérifier ces doutes
• Si 25 % des problèmes sont de niveau premier cycle, alors le score de 25 % de o3 est peut-être moins surprenant
• La grande percée attendue serait le moment où l’IA montrera des performances significatives sur les 50 % suivants, décrits comme de niveau « qual »

« Démontrez ce théorème » reste un problème différent

• En recherche mathématique, la question importante est généralement « démontrez ce théorème »
• Même si l’on disposait de machines surhumaines pour les problèmes de recherche de nombres, leur applicabilité pourrait rester limitée dans de nombreux domaines des mathématiques de recherche
• Le plus grand succès de 2024 est considéré comme AlphaProof de DeepMind
  • AlphaProof a résolu 4 des 6 problèmes de l’IMO 2024
  • Ces problèmes étaient du type « démontrez ce théorème » ou « trouvez ce nombre et démontrez qu’il est correct »
  • Trois de ces problèmes ont été produits sous forme de démonstrations Lean entièrement formalisées
• Lean est un assistant de preuve interactif, et mathlib est une bibliothèque mathématique contenant de nombreuses techniques nécessaires à la résolution des problèmes de l’IMO, et plus encore
• Les solutions du système de DeepMind ont été vérifiées par des humains et validées comme des solutions « parfaites »
• Cela dit, même si les problèmes de l’IMO sont très difficiles, leurs solutions n’utilisent que des techniques de niveau scolaire ; on revient donc à nouveau à des problèmes de niveau lycée
• On s’attend à ce qu’en 2025, les machines atteignent un niveau médaille d’or à l’IMO

Qui corrigera les réponses de la machine ?

• On peut imaginer qu’en juillet 2025, à l’IMO, non seulement des étudiants humains participent, mais aussi des machines
• Les systèmes automatiques peuvent se diviser en deux catégories
  • Les systèmes qui soumettent des réponses dans le langage de vérificateurs de preuve informatiques comme Lean, Rocq ou Isabelle
  • Les modèles de langage qui soumettent des réponses en langage humain
• Pour les réponses soumises dans le langage d’un vérificateur de preuve, il suffit de vérifier que l’énoncé du problème a bien été traduit correctement
  • Ensuite, si la preuve compile, on sait pratiquement qu’il s’agit d’une solution « parfaite »
• Pour les modèles de langage qui soumettent des réponses en langage naturel, c’est différent
  • Même si la réponse paraît plausible, un correcteur humain doit la lire attentivement et l’évaluer
  • Rien ne garantit qu’il s’agisse d’une solution parfaite
• Les modèles de langage semblent au moins un ordre de grandeur moins précis que les experts humains en raisonnement logique
• On craint par exemple qu’une « preuve » de l’hypothèse de Riemann produite par un modèle de langage puisse mêler, au milieu de 10 pages de mathématiques correctes, des affirmations vagues ou inexactes
• Les assistants de preuve, à l’inverse, semblent au moins un ordre de grandeur plus précis
  • Quand Lean n’a pas accepté un raisonnement issu de la littérature mathématique humaine, dans les cas que l’auteur a vus, c’est l’humain qui avait tort

Objectif restant : une preuve correcte et compréhensible par l’humain

• Ce que veulent les mathématiciens, ce n’est pas seulement « démontrez ce théorème », mais une preuve exacte et une explication que les humains puissent comprendre
• Dans l’approche par modèles de langage, la justesse reste le sujet d’inquiétude principal
• Dans l’approche par assistants de preuve, c’est la compréhensibilité pour l’humain qui pose problème
• Il reste encore énormément de travail
• Les progrès sont rapides, mais personne ne sait quand la barrière du premier cycle sera franchie