722 manuscrits mathématiques d’IA, des preuves à examiner

Un corpus de 722 manuscrits mathématiques produits par un modèle interne d’OpenAI est accessible, avec des preuves formalisées et des vérifications inégales.

Des centaines de travaux mathématiques produits par un modèle encore inaccessible au public sont désormais consultables dans le dépôt de recherche d’OpenAI. Le catalogue rassemble 722 manuscrits, organisés en 372 familles : chacune peut réunir un résultat principal, des développements complémentaires, des conséquences ou plusieurs démonstrations. Ce décompte ne correspond donc pas à autant de problèmes distincts résolus. Selon l’entreprise, ces recherches prolongent ses évaluations habituelles, devenues insuffisantes pour mesurer les capacités mathématiques de ses modèles.

Le niveau de vérification varie selon les travaux. Une partie s’accompagne de preuves formalisées en Lean, un langage dans lequel les démonstrations sont écrites pour être contrôlées par ordinateur. D’autres restent sans formalisation, et le laboratoire reconnaît que certains de ces résultats pourraient comporter des erreurs. Le dépôt doit s’enrichir de nouvelles preuves formelles et conserver les versions antérieures des manuscrits lors des corrections.

Environ 4 000 problèmes ont été soumis au modèle pendant l’évaluation. Les productions ont ensuite été sélectionnées selon leur importance et regroupées pour constituer le corpus. Le calcul mobilisé par résultat représente, en moyenne, l’équivalent d’environ trois heures de réflexion dans ChatGPT Pro : une estimation des ressources utilisées par ce modèle interne. Pour documenter le processus, dix résumés de raisonnement sont accessibles, portant entre autres sur l’exposant d’irrationalité de π et les conjectures de Mahler. Le protocole comporte quelques exceptions ; un texte sur la fonction zêta de Riemann a aussi été retravaillé par un humain pour en améliorer la lisibilité.

La publication s’appuie, selon l’entreprise, sur les recommandations du groupe indépendant Mathematics and Artificial Intelligence de l’Institute for Advanced Study. Dans ses préconisations publiques, celui-ci demande des textes compréhensibles, des références précises et un soutien financier à leur étude. Il appelle aussi explicitement les laboratoires à cesser de tester des problèmes mathématiques avancés sur des modèles propriétaires inaccessibles à la communauté scientifique. De son côté, le laboratoire prévoit de financer des ateliers, conférences et programmes consacrés à la compréhension de ces résultats. D’après son billet de recherche, il prépare également l’accès au modèle utilisé, sans calendrier précisé.