Yang–Mills. Le comité publie le code Lean d’OpenAI et précise ce qu’il a vérifié

Le groupe de chercheurs chargé d’examiner le travail d’OpenAI sur Yang–Mills a rendu publics deux dépôts. Le premier contient le dépôt du code Lean remis par OpenAI le 28 octobre au groupe. Le second contient le dépôt des vérifications du comité et le rapport daté du 10 novembre. Les deux dépôts étaient consultables le 11 novembre au matin. La publication donne accès aux énoncés et aux contrôles utilisés par le groupe.

Ce que le groupe estime établi

Le rapport d’évaluation du groupe conclut que la soumission permet de construire une théorie quantique des champs relativiste qui satisfait les axiomes de Wightman dans le cadre étudié. La construction part de la théorie de jauge sur réseau de Wilson en quatre dimensions pour tout groupe de jauge compact simple. Le texte décrit la manière dont les corrélations sont obtenues dans la limite continue.

Une façon de comprendre l’étape est de distinguer la grille de calcul et l’espace continu. Le réseau donne un objet mathématique à chaque échelle. Il faut établir que les observables pertinentes convergent lorsque la grille devient plus fine. Le rapport indique que cette construction se fait d’abord à volume physique fixé. Le passage au volume infini utilise ensuite des sous-suites dont le groupe décrit la convergence.

Deux questions restent ouvertes

La convergence d’une sous-suite ne montre pas que toutes les façons de faire grandir le volume conduisent à la même limite. Le rapport précise que l’unicité n’a pas été démontrée. Il distingue aussi ce point de l’écart de masse. Cette seconde question revient à établir une séparation positive entre l’état du vide et les excitations de plus basse énergie dans la théorie visée.

Le comité indique que la soumission ne revendique pas de preuve d’un écart de masse. La construction formelle vérifiée couvre donc un résultat d’existence dans le cadre décrit. Le problème du millénaire formulé par Jaffe et Witten comprend des exigences qui vont au-delà de ce résultat.

Ce que Lean permet de contrôler

Le groupe rapporte une reconstruction du projet et un audit des axiomes. Il a également vérifié certaines conséquences avec des énoncés formulés indépendamment dans Lean. La lecture humaine des définitions complète ces contrôles. Le noyau du logiciel peut examiner la dérivation d’un énoncé. Les chercheurs doivent encore comprendre si l’énoncé et ses hypothèses décrivent exactement la théorie visée.

Le groupe précise avoir utilisé Astra d’OpenAI pour l’aider à analyser le code. Il indique aussi qu’il ne revendique pas encore une compréhension complète de la preuve. Son examen porte sur la soumission Lean. Le rapport ne prend pas pour base le manuscrit informel séparé. Le rôle du modèle dans l’analyse et le jugement final des chercheurs restent deux éléments distincts.

Comme dans la vérification formelle de certaines propriétés de Signal, l’ouverture des artefacts permet à d’autres équipes d’examiner ce qui a été vérifié et de reproduire les contrôles documentés. Le résultat est désormais inspectable jusque dans les définitions et les preuves. L’avancement concerne une construction précise et rend visibles les questions que la communauté peut encore étudier.