Hier, OpenAI a publié 722 manuscrits de mathématiques par IA en une seule fois, et à l'instant, elle en a retiré 3.
La raison est simple : un signe plus-moins a été écrit incorrectement.
À l'instant, OpenAI a publié son premier journal de mises à jour dans le dépôt openai/math. Le journal montre qu'OpenAI a retiré 3 manuscrits, révisé 14 et mis à jour les citations de 13 autres. Le nombre total de manuscrits dans le dépôt est passé de 722 à 719.
Un signe plus-moins fait tomber trois articles
Les trois articles retirés sont tous liés à la conjecture de Hodge, l'un des problèmes du prix du millénaire :
Algebraicity of Weil classes on split abelian eightfolds
Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
The rational Hodge conjecture for products of K3 surfaces
Le problème réside dans le premier article. Dans la note de retrait, OpenAI a écrit que dans un argument clé, l'article enregistrait le signe d'une certaine opération géométrique comme +1, alors que selon la convention de l'article lui-même, il devrait être -1.
https://github.com/openai/math/blob/main/history.md
Un plus contre un moins fait toute la différence. Un compte qui aurait dû s'annuler et finalement être nul est devenu un nombre non nul. Un théorème classique sur lequel l'article s'appuie a pour précondition précisément que ce compte doit être nul. La précondition échouant, toute la construction ultérieure perd son support.
Les deux autres articles ont tous deux emprunté cette construction, ils ont donc également été retirés.
Cependant, dans les trois notes de retrait, OpenAI a souligné la même phrase : ce qui est retiré est la preuve, ce qui ne signifie pas que ces propositions mathématiques elles-mêmes sont fausses. Les manuscrits originaux n'ont pas non plus été supprimés et peuvent encore être consultés via des liens archivés.
Ces trois articles appartiennent tous à la famille de résultats n° 032 du dépôt, c'est-à-dire les résultats précédemment les plus suivis liés à la conjecture de Hodge.
Après le retrait, le nom de cette famille a également changé : de « Hodge and Kuga–Satake results for all projective K3 surfaces » à « the rational Hodge conjecture for CM abelian varieties ».
En d'autres termes, la partie des conclusions concernant les surfaces K3 a été retirée de la liste. La conclusion centrale de cette famille, à savoir prouver la conjecture de Hodge rationnelle pour toutes les variétés abéliennes CM complexes, est toujours conservée, et la nouvelle version de cet article n'a mis à jour que les citations.
Il convient de mentionner que l'article contenant l'erreur est daté du 18 septembre, ce qui en fait l'un des premiers lots de manuscrits du dépôt. De sa date à sa publication publique, il s'est écoulé près de trois semaines, et il a été retiré dans les un ou deux jours suivant sa publication. Quant à savoir qui a découvert l'erreur, OpenAI ne l'a pas dit.
14 autres articles ont été révisés
Outre les retraits, OpenAI a également révisé 14 manuscrits, notamment en corrigeant des preuves, en rectifiant des énoncés de conclusions et en clarifiant des conditions préalables et des dépendances.
Ces 14 articles concernent les hauteurs de Lipschitz et le modèle d'Ashkin–Teller en physique statistique (4 articles), le programme de modèle minimal de Kähler et l'abondance en géométrie complexe (6 articles), la géométrie symplectique (2 articles), le calcul général pour les fluides de Navier-Stokes (1 article), et un article sur la formule BSD duquel des citations obsolètes ont été supprimées.
Une révision est assez représentative. La famille de résultats n° 342 prétendait prouver la conjecture de « compatibilité d'image directe modérée » proposée par Simon Donaldson. La conclusion principale n'a pas changé, et il existe une formalisation Lean. Mais une conclusion incidente plus forte de l'article s'est avérée exagérée : la version révisée la restreint à un cas spécifique et ajoute également un exemple montrant qu'elle ne tient pas en général.
Taux de formalisation : 42 %
La mise à jour a également ajouté 6 formalisations Lean et 5 résultats auxiliaires supplémentaires. Selon la comptabilité d'OpenAI, les résultats principaux de 300 manuscrits ont maintenant été formalisés, ce qui représente environ 42 % de l'ensemble des 719.
Parmi les formalisations nouvellement ajoutées, plusieurs ont un poids considérable, comme la 103e famille de résultats en informatique théorique qui prétend prouver que le calcul en espace logarithmique peut être entièrement dérandomisé (L = RL = BPL).
Il convient de noter que les « environ soixante pour cent » que nous avons rapportés précédemment étaient comptés par famille de résultats, ce qui signifie que dès qu'un article d'une famille est accompagné d'une formalisation, il est compté ; les 42 % annoncés par OpenAI sont comptés par résultat principal individuel, ce qui reflète mieux la proportion réelle qui a été vérifiée ligne par ligne par un ordinateur.
Là où des erreurs se produisent, il n'y a pas de supervision Lean
Une comparaison avec le répertoire du dépôt révèle un schéma : le contenu qui a été retiré et substantiellement révisé cette fois-ci se situe presque entièrement dans les parties sans formalisation Lean.
Cela confirme également le rappel antérieur de la communauté mathématique : les résultats qui n'ont pas été soumis à une formalisation et à une évaluation par les pairs ne peuvent actuellement être considérés que comme des « affirmations ».
Heureusement, cet erratum a été traité de manière assez appropriée : les erreurs ont été clairement énoncées, la chaîne de dépendances a été expliquée, et l'ancienne version a été conservée pour référence, conformément au principe de « modification avec une trace » recommandé par le groupe consultatif sur les mathématiques et l'intelligence artificielle de l'Institute for Advanced Study.
Cependant, à peine deux jours après la publication de plus de 700 manuscrits, le premier erratum est arrivé. Il ne sera très probablement pas le dernier.
Cet article provient du compte public WeChat « Machine Heart » (ID : almosthuman2014), éditeur : Panda
