Analyse de O1 par Terence Tao

Présentation de mathstodon.xyz

• mathstodon.xyz fait partie du réseau social décentralisé basé sur Mastodon et constitue une instance destinée aux utilisateurs liés aux mathématiques.
• Prend en charge le rendu LaTeX dans l’interface web.
• Administrateur : Christian Lawson-Perfect (@christianp)
• Statistiques du serveur : 3K utilisateurs actifs

Expériences de Terence Tao avec GPT-o1

• GPT-o1 : nouvelle version de GPT d’OpenAI, qui effectue une phase initiale de raisonnement avant l’exécution du LLM.
• Expérience 1 : face à une question mathématique ambiguë, il a correctement identifié le théorème de Cramer et fourni une réponse satisfaisante.
  • Dans la version précédente, le concept connexe était mentionné, mais les détails étaient erronés.
• Expérience 2 : sur un problème complexe d’analyse, il a abouti à la bonne solution grâce à de nombreux indices et guidages, mais n’a pas su générer seul l’idée conceptuelle principale et a commis quelques erreurs.
  • Il s’agit d’un progrès par rapport au modèle précédent, mais cela reste insuffisant.
  • Avec quelques améliorations supplémentaires, il pourrait devenir utile pour des travaux de niveau recherche.
• Expérience 3 : pour formaliser un résultat dans Lean, il a bien compris le problème et correctement effectué la décomposition initiale, mais le manque d’informations récentes sur Lean a entraîné plusieurs erreurs dans le code.
  • Il pourrait être très utile dans un IDE intégrant un modèle spécialisé pour Lean et Mathlib.

Discussion complémentaire

• Progrès des outils d’IA : attente de l’émergence d’un écosystème d’outils d’IA capable de traiter divers travaux de recherche.
  • Aujourd’hui, les grands LLM généralistes attirent l’attention, mais on s’attend aussi à ce que des modèles open source légers, adaptés à des applications spécifiques, jouent un rôle important.
• Comparaison entre l’IA et les doctorants : discussion sur la capacité des outils d’IA à apporter une contribution de niveau doctorant.
  • Pour l’instant, ils demandent plus d’efforts qu’un doctorant, mais il est possible que ce ratio tombe à 1 ou moins dans les prochaines années.

# Résumé de GN⁺

• Terence Tao a testé le nouveau modèle GPT-o1 d’OpenAI pour évaluer ses capacités de résolution de problèmes mathématiques.
• GPT-o1 est meilleur que les versions précédentes, mais présente encore plusieurs limites.
• Avec quelques améliorations supplémentaires, il pourrait devenir utile pour des travaux de niveau recherche.
• Il anticipe l’émergence d’un écosystème où divers outils d’IA pourront soutenir les travaux de recherche.
• Aujourd’hui, les grands LLM généralistes attirent l’attention, mais on s’attend aussi à ce que des modèles open source légers, adaptés à des applications spécifiques, jouent un rôle important.

[GN⁺]

Discussion sur Hacker News

• On s’attend à ce que GPT devienne plus utile pour les mathématiques de niveau recherche s’il est affiné pour Lean (assistant de preuve) comme il l’a été pour Python

  • Dans les domaines liés à la recherche opérationnelle (OR), ChatGPT 4o a suffisamment assimilé la littérature OR pour proposer des formulations utiles de programmation linéaire en nombres entiers mixtes (MIP)
  • Lorsqu’on lui présente un problème logique, il génère des formules mathématiques utiles qui ne nécessitent que de légères modifications
  • Il signale les formulations faibles dont la logique peut échouer, ce qui aide à éviter les problèmes
  • GPT résout des problèmes qui, autrefois, auraient demandé de se creuser la tête tout un week-end, ce qui fait gagner beaucoup de temps
  • Pour quelqu’un qui comprend l’optimisation MIP et sait découper un problème en petits morceaux, l’abonnement mensuel à 20 $ de ChatGPT vaut largement son prix
  • Beaucoup de gens utilisent mal les LLM ou en attendent trop, puis s’en montrent mécontents
  • Ceux qui connaissent les points forts des LLM et savent vérifier leurs erreurs en tirent une grande aide dans leur travail

• Imaginez revenir en 2019 et lire que l’expérience d’interagir avec Alexa est « comparable au fait de conseiller un étudiant de master moyen, mais pas totalement incompétent »

  • En cinq ans, l’écart est devenu énorme

• Le modèle o1 est très impressionnant

  • Il a permis d’obtenir d’importants gains de vitesse dans un projet d’optimisation de code Rust, avec vérification de la correction
  • Il a imaginé et implémenté une nouvelle mesure de dépendance statistique fondée sur la divergence de Jensen-Shannon
  • Il a implémenté rapidement une information mutuelle normalisée, pour laquelle il était difficile de trouver une implémentation rapide lorsqu’on manipule de grands vecteurs (par ex. plus de 15 000 dimensions)
  • Il n’a pas fourni un code Rust parfait du premier coup, mais a corrigé tous les bugs en une seule tentative
  • GPT-4o a eu besoin de plusieurs essais pour corriger des erreurs de type Rust
  • Claude 3.5 Sonnet est très incompétent en Rust
  • Il apporte une grande aide sur des tâches très difficiles
  • Il comprend l’objectif et le concrétise en combinant optimisation des performances, code relativement peu bogué, résolution créative de problèmes et vaste savoir mathématique et algorithmique

• Les expériences avec le modèle O1 sont très variables

  • Il se montre confus même face à des questions simples

• Ce qui est nouveau, c’est que les LLM ressemblent, sur des sujets variés, à « conseiller un étudiant de master moyen, mais pas totalement incompétent »

  • Ils sont très utiles pour traiter de petites tâches dans des domaines où l’on a de l’expérience
  • Lorsqu’on découpe un problème en petits morceaux, ils font un travail solide
  • Une compréhension conceptuelle est nécessaire, et le savoir-faire en prompting est important
  • On peut utiliser les LLM pour comprendre des sujets complexes, puis valider les concepts avec la vérification d’un expert

• Les humains aussi peuvent tirer profit d’un raisonnement de type « chaîne de pensée »

  • Si tous les étudiants qui apprennent les mathématiques devaient mémoriser les définitions et informations pertinentes, leurs capacités s’en trouveraient grandement améliorées
  • L’IA peut mieux raisonner car elle n’a pas de barrières émotionnelles

• Accord avec l’avis de Terence Tao

  • Les LLM peuvent améliorer leurs performances par appariement de motifs, mais cela pourrait ne pas suffire à produire une véritable généralisation
  • Sur des problèmes nouveaux ou complexes, des hallucinations et des raisonnements erronés peuvent encore survenir

• Il est enthousiasmant de se remettre à étudier les mathématiques comme loisir indépendant

  • Les LLM apportent une aide précieuse pour résoudre des questions complexes d’analyse
  • Leur capacité à repérer rapidement des liens conceptuels est impressionnante
  • À la question de savoir si l’on pouvait faire de l’analyse complexe sur une variété non orientée en assouplissant certaines définitions, le LLM a immédiatement compris que les équations de Cauchy-Riemann ne sont pas cohérentes globalement
  • Sans LLM, il n’aurait pas été possible de répondre à cette question

• L’avis de Terence Tao est surprenant

• Daniel Litt a été impressionné par o1-preview, mais n’a pas encore eu de chance pour résoudre des problèmes mathématiques intéressants

  • Il est plus fiable sur des tâches simples et peut faire gagner du temps sur des tâches non mathématiques