OpenAI a publié sur GitHub une collection de 722 études mathématiques produites par un modèle d’intelligence artificielle interne que l’entreprise n’a pas encore rendu accessible au public. La collection couvre 372 familles de résultats, parmi lesquels des tentatives visant à traiter des problèmes ouverts dont la résolution se fait attendre depuis longtemps, selon l’évaluation du groupe indépendant Advisory Group on Mathematics and Artificial Intelligence (AGMAI).
La publication de ces travaux ne signifie toutefois pas qu’ils sont reconnus comme des avancées mathématiques définitives. OpenAI précise que les résultats se trouvent à différents stades de vérification et que certaines études informelles peuvent contenir des erreurs, tandis que l’ensemble doit encore être examiné par la communauté mathématique et confirmé par les canaux universitaires habituels.
D’environ 4 000 problèmes à 722 études
Au cours du processus d’évaluation, le modèle a été testé sur environ 4 000 problèmes mathématiques. Après avoir filtré les résultats selon leur niveau d’importance, OpenAI a sélectionné la collection publiée, composée de 372 familles et de 722 études. L’entreprise affirme que la production d’un résultat a nécessité en moyenne une capacité de calcul équivalant à environ trois heures de la capacité de raisonnement disponible pour les utilisateurs de ChatGPT Pro.
Afin de faciliter l’examen, OpenAI a publié des données supplémentaires sur 10 problèmes, comprenant de brefs résumés du processus de raisonnement, des estimations de la capacité de calcul utilisée et le nombre de problèmes qui ont été tentés. Les exemples couvrent différents domaines, notamment une mesure de l’irrationalité du nombre π, les conjectures de Mahler, la conjecture de Kaplansky sur la finitude directe et le système tridimensionnel relativiste de Vlasov-Maxwell.
La vérification avec Lean n’est pas exhaustive
Une partie importante des preuves publiées a été examinée à l’aide de Lean, un système de vérification mathématique qui permet à l’ordinateur de tester la cohérence logique d’une preuve. Cependant, toutes les études de la collection ne disposent pas encore d’une vérification formelle avec Lean.
OpenAI prévoit de mettre à jour le dépôt GitHub au fur et à mesure de l’achèvement des processus de vérification formelle. L’entreprise indique que la plupart des résultats ont été produits selon une procédure standardisée, avec certaines exceptions : l’une des études portant sur une région dépourvue de zéros de la fonction zêta de Riemann a été obtenue d’une manière différente, et son texte a été édité par un humain afin d’en améliorer la lisibilité.
Pourquoi cette nouvelle est-elle importante ?
La valeur principale de la collection ne réside pas seulement dans le nombre d’études, mais aussi dans la mise à l’épreuve d’une nouvelle méthode de production de résultats mathématiques susceptibles d’être examinés. La mise à disposition des fichiers, des données sur le coût de calcul, des résumés du raisonnement et de la vérification automatisée partielle fournit aux chercheurs les éléments nécessaires pour déterminer si le modèle produit des découvertes susceptibles d’être réexaminées ou simplement des textes qui semblent convaincants.
En revanche, des limites évidentes subsistent : la vérification est incomplète, l’examen humain et universitaire n’est pas terminé et les résultats du modèle ne constituent pas encore un système accessible aux chercheurs ni un produit public. L’AGMAI invite les entreprises d’intelligence artificielle à publier les résultats mathématiques par les canaux universitaires, à divulguer les modèles, le coût et les méthodes utilisés, et à ne pas transformer les découvertes en simple outil marketing.
OpenAI a également annoncé qu’elle financerait des ateliers, des conférences et des programmes spécifiques afin de comprendre les résultats importants produits par l’intelligence artificielle, parallèlement à ses travaux visant à rendre le modèle interne accessible de manière responsable. La collection actuelle constitue donc une étape expérimentale dans la manière de documenter les résultats scientifiques générés automatiquement, et non un jugement définitif sur les capacités mathématiques du modèle.