- Le problème d’Erdős n°728 a récemment été résolu presque de manière autonome par des outils d’IA, marquant une nouvelle étape dans l’automatisation de la recherche en mathématiques
- Le problème était à l’origine une question sur la factorisation en nombres premiers des coefficients binomiaux posée en 1975 par Erdős, Graham, Ruzsa, Strauss, et il est longtemps resté difficile à traiter clairement en raison de conditions ambiguës
- ChatGPT a généré une preuve sous des contraintes ajustées, puis Aristotle l’a formalisée en preuve formelle Lean en corrigeant automatiquement les erreurs
- Plusieurs participants l’ont ensuite réécrite en langage naturel avec ChatGPT et ont amélioré de manière itérative une version renforçant les liens avec la littérature et la structure narrative
- Terence Tao estime que ce processus montre le potentiel de la capacité de l’IA à rédiger et corriger rapidement des preuves pour transformer la manière même d’écrire des articles de recherche
Le problème d’Erdős n°728 résolu par l’IA
- L’application récente d’outils d’IA a apporté de nouveaux progrès dans la résolution de problèmes d’Erdős, et le problème n°728 a été résolu presque de manière autonome par l’IA
- Après une première tentative, une version corrigée intégrant les retours a permis d’aboutir
- Le résultat n’a pas été reproduit à l’identique dans la littérature existante ; seuls des résultats proches par des méthodes similaires y figurent
- Ce cas montre que, ces derniers mois, les capacités de l’IA en résolution de problèmes mathématiques se sont réellement améliorées
- Par le passé, l’IA avait déjà été créditée de la résolution de problèmes d’Erdős, mais la plupart de ces résultats se sont ensuite révélés déjà présents dans la littérature
- Dans ce cas précis, l’énoncé original d’Erdős avait été présenté sous une forme incorrecte, et ce n’est que récemment qu’il a été reconstruit sous la forme voulue
- Cela expliquerait le manque de travaux antérieurs sur le sujet dans la littérature
Histoire du problème et premières approches
- En 1975, Erdős, Graham, Ruzsa, Strauss ont étudié la factorisation en nombres premiers du coefficient binomial (2n choose n) et ont posé plusieurs problèmes connexes
- L’un d’eux demandait s’il existe une infinité de a, b, n satisfaisant la condition a!b! | n!(a+b−n)! et a+b > n + C log n
- Cependant, plusieurs éléments, dont la taille de C (petite ou grande), étaient formulés de manière ambiguë
- Il y a quelques mois, l’équipe AlphaProof a trouvé une solution simple au problème, mais celle-ci ne correspondait pas à l’esprit du problème visé, ce qui a conduit à ajouter la contrainte a,b ≤ (1−ε)n
- Même après une recherche bibliographique assistée par IA, très peu de travaux pertinents ont été trouvés
Collaboration entre ChatGPT et Aristotle
- Le 4 janvier, ChatGPT a généré une preuve pour le cas de petit C sous les contraintes ajustées
- Cette preuve a ensuite été formalisée en preuve formelle Lean par Aristotle
- En réexaminant le texte original, il a toutefois été confirmé que l’article initial traitait déjà le cas du petit C
- Un autre participant a converti la preuve Lean en langage naturel avec ChatGPT, puis a produit une version améliorée au fil d’échanges supplémentaires
- Cette version comblait certaines lacunes de la démonstration, mais conservait encore une tournure maladroite typique de l’IA et un manque de références à la littérature
- Malgré cela, elle a atteint un niveau suffisamment lisible pour comprendre l’idée centrale
Réécriture à grande échelle et résultat amélioré
- Grâce à des prompts supplémentaires, ChatGPT a généré une preuve étendue jusqu’au cas de grand C
- Il subsistait quelques erreurs, mais Aristotle les a corrigées automatiquement et a achevé une preuve vérifiée par Lean
- Un troisième participant a compressé la preuve Lean, puis un autre, au terme d’une longue conversation avec ChatGPT, a
- réécrit le tout sous la forme d’un article abouti, avec des liens à la littérature et une structure narrative renforcés
- Le résultat a été jugé moins marqué par l’aspect typique d’un texte généré par IA, et d’une qualité proche de celle d’un article de recherche
- Tao indique avoir relu ce texte sur le forum consacré aux problèmes d’Erdős
Comment l’IA transforme la rédaction des articles de recherche
- Tao estime que, dans l’article final, les parties essentielles doivent encore être rédigées par des humains, mais
- l’association de l’IA et de Lean a, selon lui, considérablement accéléré la rédaction et la correction des preuves
- Jusqu’ici, rendre un article agréable à lire demandait beaucoup de temps, et
- les révisions à la suite des retours des relecteurs se limitaient souvent à des modifications locales
- Désormais, la combinaison de la génération et de la révision de texte par l’IA avec la vérification offerte par les outils de preuve formelle permet
- de produire rapidement de nouvelles versions d’un article avec différents niveaux de précision et de narration
- Au-delà d’un unique « article officiel », l’existence de nombreuses versions auxiliaires générées par l’IA
- ouvre la possibilité d’apporter des points de vue variés et une valeur supplémentaire
Réactions de la communauté
- Certains utilisateurs ont décrit la valeur ajoutée des documents générés par l’IA comme la capacité à voir les choses sous un autre angle
- D’autres mathématiciens ont souligné la nécessité de mesurer l’originalité des résultats produits par l’IA ou d’évaluer leur similarité avec la littérature existante
- Par exemple, une proposition consiste à mesurer quantitativement cette similarité en comparant la longueur des preuves formelles Lean
- Un autre commentaire avance que l’IA peut réécrire un article de manière globale, comme dans un refactoring de code, ce qui
- pousserait les chercheurs à se concentrer davantage sur la conception de la structure générale des documents
- Certains se sont montrés sceptiques quant à la possibilité que l’IA remplace le rôle des mathématiciens, mais
- d’autres y voient une nouvelle opportunité de collaboration et d’élargissement de la réflexion
Aucun commentaire pour le moment.