Un dépôt, pas un article
OpenAI a publié le 6 octobre un catalogue de résultats mathématiques produits par ce qu’elle appelle un modèle de frontière interne, et a tout déposé dans un dépôt GitHub plutôt que de le soumettre à des revues. Le catalogue compte 722 manuscrits organisés en 372 familles de résultats, une famille regroupant un résultat principal avec ses arguments compagnons, ses conséquences ou des preuves alternatives.
L’entreprise affirme que ce travail est issu du développement du modèle et non d’un programme de recherche dédié. « Dans le cadre du développement du modèle, nous évaluons nos modèles sur des problèmes de recherche ouverts », indique le fichier de présentation du dépôt. « Nous avons élargi ces évaluations après la saturation des performances sur nos évaluations mathématiques existantes. »
Ce que les chiffres disent du calcul
OpenAI a divulgué plus de détails méthodologiques qu’à l’accoutumée. Au cours de l’évaluation, environ 4 000 problèmes ont été posés au modèle. Le résultat publié moyen a consommé l’équivalent d’environ trois heures de calcul de raisonnement ChatGPT Pro. Le regroupement des sorties en familles et en manuscrits, avec l’exigence de ce qu’OpenAI nomme un niveau de signification approprié, a donné le chiffre de 722.
Deux éléments ont été traités autrement. Les travaux sur une région sans zéro de la fonction zêta de Riemann et une preuve de la conjecture de Hodge pour les variétés abéliennes à multiplication complexe sortent de la procédure fixe, et OpenAI indique que la rédaction du résultat sur la fonction zêta — portant sur la région où la partie réelle de s dépasse 11/12 — a été relue par un humain pour la lisibilité.
Les réserves sont dans le dépôt, pas dans l’annonce
La collection réunit des résultats à des stades de vérification différents. De nombreux manuscrits sont accompagnés de formalisations en Lean, un langage qui permet à un ordinateur de vérifier une preuve, mais pas tous. OpenAI écrit sans détour que « certains des résultats non formalisés pourraient présenter des problèmes » et dit qu’elle corrigera rapidement ceux qu’elle trouvera, en ajoutant des formalisations au dépôt au fil de leur obtention.
Ce cadrage compte, car c’est l’entreprise elle-même, et non un rapporteur, qui décide de ce qui est assez significatif pour être publié. OpenAI indique avoir consulté le groupe consultatif indépendant sur les mathématiques et l’intelligence artificielle de l’Institute for Advanced Study sur les bonnes pratiques, et s’être appuyée sur ses conseils et recommandations publiques pour décider du mode de diffusion.
Dix résumés de raisonnement
Aux côtés des manuscrits, OpenAI a publié des résumés abrégés du raisonnement du modèle pour dix résultats, dont l’exposant d’irrationalité de pi, les conjectures de Mahler symétrique et générale, des bornes quasi-polynomiales pour les progressions arithmétiques, la conjecture de finitude directe de Kaplansky en caractéristique deux et le système relativiste de Vlasov-Maxwell en trois dimensions. Elle a aussi publié des instructions de citation par manuscrit et promis de conserver l’historique des versions, les corrections étant enregistrées comme de nouvelles versions.
Ce qu’il faut surveiller
Le modèle à l’origine de tout cela n’est pas disponible. OpenAI dit « travailler à diffuser de manière responsable le modèle qui a produit ces résultats » et annonce le financement d’ateliers, de conférences et de programmes spéciaux consacrés à la compréhension des grands résultats produits par l’IA, avec des détails à venir.
L’épreuve pratique est désormais la bibliothèque Lean. Les preuves formalisées peuvent être vérifiées par une machine ; les manuscrits non formalisés doivent être lus par des mathématiciens, et 722 représentent beaucoup de lecture. La vitesse de remplissage du catalogue de formalisations — et le nombre de résultats non formalisés qui survivront au contact de la discipline — en dira plus que le décompte affiché.
