-
Présentation d'o3 et de FrontierMath
- o3 est un nouveau modèle de langage d’OpenAI qui a obtenu un score de 25 % sur FrontierMath, un jeu de données secret.
- FrontierMath est un jeu de données confidentiel composé de problèmes mathématiques difficiles publiés par Epoch AI.
- Les questions sont de type « Trouve ce nombre ! » et exigent une réponse précise vérifiable automatiquement.
-
Difficulté du jeu de données FrontierMath
- Les problèmes de FrontierMath sont aussi peu conventionnels pour les chercheurs en mathématiques, et certains nécessitent un niveau de connaissances équivalent à un doctorat.
- Les tâches du jeu de données privilégient la recherche de nombres plutôt que les preuves mathématiques.
- Comme les chercheurs passent surtout leur temps à trouver des preuves ou des idées, FrontierMath constitue un jeu de données important pour la recherche en mathématiques avec l’IA.
-
Capacités mathématiques de l’IA
- Aujourd’hui, l’IA résout bien les problèmes de mathématiques de niveau lycée et devrait bientôt passer les examens universitaires.
- En revanche, générer des idées innovantes au-delà du niveau licence avancée reste encore un défi.
- Le score de 25 % d’o3 est impressionnant, même si certains avancent que certains problèmes sont d’un niveau d’étudiant de premier cycle.
-
Rôle de l’IA en recherche mathématique
- En recherche mathématique, l’objectif central est de résoudre des problèmes du type « Prouve ce théorème ! ».
- AlphaProof de DeepMind a résolu 4 problèmes de l’Olympiade internationale de mathématiques 2024, dont certains ont été entièrement vérifiés avec une preuve Lean.
- Pour que l’IA joue un rôle plus important en recherche mathématique, elle doit pouvoir expliquer les preuves d’une manière compréhensible par les humains.
-
Perspectives
- Pour que l’IA ait un rôle plus important en recherche mathématique, elle doit être capable d’expliquer les preuves de façon intelligible pour les humains.
- Les progrès de l’IA sont rapides, mais la route reste longue.
- On ne sait pas encore quand l’IA franchira la barrière du niveau universitaire.
1 commentaires
Commentaires Hacker News
Dans le fil Reddit, sur trois niveaux de difficulté, 25 % sont en T1 (les plus faciles) et 50 % en T2. Parmi les cinq problèmes publics que l’auteur a vus, deux étaient en T1 et deux en T2. Glazer a décrit T1 comme des “problèmes de niveau IMO/licence”, mais l’auteur ne considère pas cela comme de vrais problèmes de licence. Le LLM réalise déjà des choses qui ont surpris l’auteur.
En essayant d’utiliser ChatGPT pour comprendre l’algèbre linéaire, il a constaté qu’il commet souvent des erreurs vraiment basiques en mathématiques réelles, par exemple en indexant au-delà de la dimension d’un vecteur, en essayant une décomposition de matrice sur un scalaire, ou en multipliant des matrices de dimensions incompatibles.
O1 repère mieux les erreurs que 4o, mais continue de faire beaucoup d’erreurs idiotes. Sans l’aide de quelqu’un qui a un minimum de connaissances, il est difficile d’obtenir des résultats cohérents.
Dans la conférence d’Akshay Venkatesh, il a été discuté de l’avenir du “métier de mathématicien” si les preuves théoriques automatisées devenaient plus répandues. On a évoqué la manière dont les avancées du raisonnement automatique pourraient modifier la façon de conceptualiser et de pratiquer les mathématiques de recherche.
En tant que parent d’un fils de 18 ans qui veut étudier les mathématiques, il s’inquiète que l’automatisation puisse éliminer cet emploi. Mais il doute que les LLM puissent remplacer totalement les humains. Puisque les LLM n’ont ni un temps infini ni des ressources illimitées pour tout résoudre, il pense qu’il y aura encore une place pour l’humain.
Il n’exclut pas qu’on puisse constituer un jeu de problèmes que les LLM résoudraient presque tous, mais il ne pense pas que ces modèles deviendront un résolveur universel capable de remplacer le raisonnement humain. Tant que l’IA ne développera pas une rationalité sociale indépendante au sens humain, le raisonnement n’en sera pas possible.
Il donne des exemples d’erreurs fondamentales commises par ChatGPT. Par exemple, il a expliqué une étape erronée en dérivant la formule d’efficacité du protocole Stop-and-Wait ARQ. Dans un autre cas, lorsqu’on lui a demandé un syllogisme d’entraînement, il a donné un syllogisme incohérent.
Il soulève la possibilité que le dataset FrontierMath soit compromis. Si OpenAI connaissait les questions, il pense qu’elle pourrait dépasser 80 % au test FrontierMath dans la version suivante.
Il se heurte au même type de problème qu’en recherche quantique : il faut effectuer des calculs impossibles sur un ordinateur classique pour démontrer les progrès. Quand ChatGPT a obtenu 25 %, la question s’est posée de savoir à quel point ces 25 % étaient proches des questions du jeu d’entraînement.
Il s’inquiète de la possibilité qu’un modèle de langage fournisse une “preuve” de l’hypothèse de Riemann. Les mathématiciens pourraient vouloir vérifier de telles preuves, mais cela pourrait prendre beaucoup de temps.
Une machine ne participera pas à l’IMO 2025. À l’IMO, il n’existe pas de notion de “correcteur” ; le score est fixé par une négociation entre le chef de chaque équipe nationale et les jurés. Personne ne restera des centaines de personnes de plus pour noter du travail produit par une IA.