Le 6 octobre, OpenAI a mis en ligne sur GitHub 719 articles mathématiques produits par un modèle interne non publié. Cette publication est intervenue une semaine après que son propre organe consultatif a appelé les laboratoires d'IA à cesser de tester des problèmes mathématiques avancés sur des modèles propriétaires. Cette séquence à une semaine d'intervalle illustre la tension qui traverse désormais la recherche mathématique pilotée par l'IA : les laboratoires utilisent des problèmes ouverts pour mesurer les progrès des modèles, tandis qu'une partie de la communauté mathématique réclame la transparence et une évaluation par les pairs conventionnelle avant que les résultats générés par l'IA ne circulent.

Plus de 600 réponses à une enquête ont façonné les recommandations du comité de l'IAS du 29 septembre

L'Advisory Group on Mathematics and Artificial Intelligence, basé à l'Institute for Advanced Study de Princeton, dans le New Jersey, a publié ses recommandations le 29 septembre, en s'appuyant sur plus de 600 réponses à une enquête. « Nous tenons à dire clairement d'emblée : nous ne cautionnons pas cette pratique, et nous demandons qu'ils cessent de tester des problèmes mathématiques avancés sur des modèles propriétaires », a écrit le groupe dans ses recommandations.

Le même document met en garde contre le risque que des modèles internes détenus privéement créent un système à deux vitesses, dans lequel une poignée de laboratoires devancerait le reste de la communauté.

Selon son dépôt, OpenAI teste ses modèles sur des problèmes de recherche ouverts dans le cadre du développement de ses modèles, et a étendu ces tests après la saturation de ses benchmarks mathématiques existants — le point auquel les modèles obtiennent des scores au niveau ou proche du sommet des tests actuels. L'entreprise a déclaré avoir consulté le groupe consultatif et s'être appuyée sur ses recommandations pour cette publication. Dans une déclaration diffusée le 6 octobre, le groupe a indiqué que son rôle consultatif ne constitue pas « une caution du processus par lequel OpenAI les a obtenus », et a laissé à l'ensemble de la communauté mathématique le soin de se prononcer sur la conformité.

Le code Lean de Navier-Stokes démontre des énoncés plus faibles que l'article écrit

OpenAI a organisé les 719 articles en 372 familles mathématiques, chacune construite autour d'un résultat principal et de ses preuves associées. Le modèle propriétaire s'est vu soumettre environ 4 000 problèmes, et chaque résultat a nécessité en moyenne environ trois heures de calcul de réflexion sur ChatGPT Pro.

Le groupe consultatif a demandé aux laboratoires d'IA de publier, pour chaque résultat, le nom du modèle, les invites utilisées, un résumé de la chaîne de raisonnement, le temps écoulé et le coût de calcul. OpenAI a publié 10 résumés de raisonnement, et environ 42 % de ses résultats principaux comportent des formalisations Lean. La mesure dans laquelle la publication correspond à cette liste d'exigences par résultat fait partie questions que le groupe a laissées à la communauté mathématique.

Lean est un langage de programmation qui permet à un ordinateur de vérifier une preuve. Si le code compile, cela ne signifie pas que le code et l'argument écrit sont identiques ; cela établit seulement que l'énoncé formel est vrai. La conversion d'arguments écrits en code vérifiable par machine de cette manière est ce que les chercheurs appellent l'autoformalisation.

Cet écart a été examiné dans un article publié le 6 octobre par Alexander Bastounis, Fabian Circelli et Anders C. Hansen. Ils constatent que l'article écrit d'OpenAI sur Navier-Stokes affirme plus que ce que son code Lean démontre, l'une des estimations modifiant l'ordre des dérivées d'entrée. Les auteurs ont également détecté des erreurs de traduction similaires dans la preuve d'Euler d'OpenAI, écrivant que la preuve écrite d'OpenAI et les autres preuves Lean autoformalisées « ne devraient pas, à première vue, être considérées comme fiables sans le même processus d'évaluation par les pairs et le même examen rigoureux que celui auquel les autres preuves sont soumises ».

OpenAI avait annoncé le résultat sur Navier-Stokes le 8 septembre. Ces équations font l'objet de l'un des Problèmes du prix du millénaire du Clay Mathematics Institute, chacun doté d'un prix d'un million de dollars. Le mathématicien de l'Université de New York Tristan Buckmaster a ensuite contesté la description faite par l'entreprise de la contribution humaine minimale impliquée dans ce travail, comme l'a rapporté Cryptopolitan. L'entreprise s'est engagée à financer des ateliers, des conférences et des programmes spéciaux liés aux grands résultats de l'IA. Le 6 octobre, le mathématicien Terence Tao a écrit que les personnes qui utilisent des invites auprès des systèmes d'IA résolvent souvent des problèmes avant de perdre tout intérêt pour le domaine, ajoutant que beaucoup ne peuvent pas répondre aux questions ni donner des conférences sur les travaux obtenus ; sa publication ne citait pas OpenAI.

L'entreprise a déclaré que ses conseillers n'ont aucun pouvoir sur le rythme de ses recherches, comme l'a rapporté Cryptopolitan en septembre. Alors que le verdict de conformité se trouve désormais entre les mains de la communauté mathématique, les points à surveiller sont de savoir si l'évaluation par les pairs confirme ou conteste les traductions de l'écrit vers Lean, et si les prochaines publications détailleront les divulgations — nom du modèle, invites, chaînes de raisonnement résumées, durées et coûts de calcul — que le groupe a demandées pour chaque résultat.