OpenAI publie 372 preuves mathématiques générées par l’IA sur GitHub, en invitant le monde académique à suivre le rythme

OpenAI publie 372 preuves mathématiques générées par l’IA sur GitHub, en invitant le monde académique à suivre le rythme

Points clés

• OpenAI a publié 372 résultats mathématiques générés par un modèle d’IA interne.
• Les résultats visent à résoudre ou avancer des problèmes ouverts, y compris les améliorations des algorithmes informatiques et les progrès concernant l'hypothèse de Riemann.
• La plupart des résultats proviennent d’un seul prompt à un seul agent, et chaque fois, il faut en moyenne environ trois heures de calcul par ChatGPT Pro.

OpenAI a publié une grande collection de résultats mathématiques produits par un modèle d’IA interne. Les preuves sont déposées sur GitHub plutôt que dans des revues académiques, et la vérification formelle vise à rendre la révision plus pratique.

OpenAI a publié 372 nouveaux résultats mathématiques générés par un modèle interne de frontière. Chaque résultat est censé résoudre un problème ou faire des progrès significatifs vers celui-ci. La collection comprend des améliorations de principaux algorithmes informatiques et des avancées liées à l’théorème de Riemann.

L’entreprise héberge les résultats dans un répertoire GitHub, comprenant des journaux de révision et des références. Selon OpenAI, le même modèle a déjà produit une solution à un problème de Navier-Stokes qui a été soumise à revue formelle pendant des semaines.

Pratiquement tous les résultats provenaient d’un seul prompt à un seul agent AI, selon OpenAI, bien que certains aient nécessité plusieurs essais. Cela contraste fort avec la solution de Navier-Stokes, qui a nécessité un groupe de 10 000 agents et des millions de dollars de calcul. En moyenne, chaque résultat a nécessité environ trois heures de calcul avec ChatGPT Pro Thinking.

La vérification formelle pourrait faciliter le gouffre de revue

Beaucoup de preuves sont accompagnées de formalisations en Lean, un langage de programmation conçu pour permettre le contrôle automatique des preuves mathématiques. De plus grandes formalisations sont prévues. La raison est pratique : le volume énorme des résultats générés par l’IA pourrait facilement surcharger la capacité de la communauté mathématique à effectuer une vérification manuelle.

OpenAI a également publié des détails sur sa méthodologie, incluant des résumés du processus de raisonnement, des statistiques sur le nombre de problèmes que le modèle a tenté de résoudre, ainsi que des estimations des coûts de calcul.

Les revues traditionnelles ne sont pas conçues pour ce rythme

OpenAI a publié ses résultats sur GitHub plutôt que dans des revues peer‑reviewées. C’est une démarche symbolique, car cela indique que le processus traditionnel de la recherche scientifique est trop lent pour ce volume de connaissances potentielles nouvelles.

OpenAI a consulté le Groupe consultatif sur les mathématiques et l’intelligence artificielle de l’Institut pour les études avancées et a suivi de manière générale leurs recommandations publiques, car l’entreprise ne publie aucun prompt et ne partage que des coûts de calcul moyens plutôt que des chiffres par problème. Le groupe consultatif comprend entre autres le lauréat de la médaille Fields, Timothy Gowers, ainsi que d’autres mathématiciens renommés.

L’entreprise a également annoncé des plans pour financer des ateliers et des conférences visant à comprendre les résultats produits par l’IA. OpenAI a reconnu qu’elle souhaite améliorer la qualité de ses citations et de ses présentations, et déclare travailler sur une publication responsable du modèle afin de « donner directement des compétences avancées aux scientifiques ».

OpenAI a fixé une limite importante pour le groupe de conseil en amont : les mathématiciens peuvent donner des conseils sur la manière dont les résultats sont communiqués, mais pas sur si et à quelle vitesse ils sont produits.

Le monde des mathématiques est divisé quant à la signification réelle des preuves produites en grand nombre

Les formalisations formelles peuvent vérifier la cohérence logique, mais elles ne peuvent pas juger si un résultat est mathématiquement pertinent ou original. OpenAI espère que ses résultats pousseront les limites du savoir humain. L’accord de la communauté mathématique reste une question ouverte. Jusqu’à présent, les réactions vont de l’excitation à la frustration.

Dans une récente lettre ouverte intitulée « Une grave désalignement de l’IA en mathématiques », 25 lauréats de la médaille Fields ont averti que les objectifs de l’industrie de l’IA et ceux des mathématiques sont profondément dissemblables. La résolution de problèmes, écrivaient-ils, n’est qu’un outil et un intermédiaire pour l’objectif réel de la compréhension conceptuelle et de l’insight. La production en masse de affirmations vraies pourrait détruire un terreau fertile plutôt que de donner vie à de nouvelles idées, arguaient-ils. L’effet se propagerait ensuite dans d’autres domaines.

Gowers a averti que, dans une à deux décennies, la littérature mathématique pourrait croître de manière énorme, sans qu’une communauté humaine puisse vraiment la comprendre. Le lauréat de la médaille Fields, Terence Tao, a ajouté que la formation des jeunes mathématiciens devrait mettre l’accent sur le aspect humain et limiter strictement l’utilisation d’outils d’IA, afin que l’apprentissage et la compréhension authentiques survivent.

Nouvelles sur l’IA sans hype – sélectionnées par des humains

Abonnez-vous à THE DECODER pour une lecture sans publicités, un bulletin informatif sur l’IA hebdomadaire, notre rapport exclusif « AI Radar » six fois par an, un accès complet à l’archive, et un accès à notre section de commentaires.