L'ESSENTIEL EN 30 SECONDES

  • Selon des bénévoles, les preuves Lean des deux laboratoires passent des vérificateurs indépendants. Un contributeur indique que l'étape qui les relie à un modèle standard de machine de Turing a été formalisée le 6 novembre.
  • Russell Impagliazzo, Ramamohan Paturi et Ryan Williams, qui coordonnent l'examen, précisent que leur participation ne vaut pas certification. Aucun verdict n'a été publié.
  • Restent ouvertes deux questions : les définitions formelles correspondent-elles à l'hypothèse classique, et la borne plus fine de l'article d'OpenAI tient-elle ? Cette borne n'a pas été entièrement formalisée.

Le 26 octobre, OpenAI a affirmé qu'un de ses modèles internes avait réfuté l'hypothèse du temps exponentiel (ETH). Formulée par Russell Impagliazzo et Ramamohan Paturi, cette conjecture postule que le problème 3-SAT ne peut pas être résolu en temps sous-exponentiel. Le manuscrit de 67 pages d'OpenAI décrit un algorithme qui décide les instances de k-SAT et en compte les solutions en temps sous-exponentiel. Il s'accompagne d'une preuve vérifiée par l'assistant de preuve Lean. Anthropic a publié sa propre réfutation le même jour.

Ce qui a été vérifié

L'examen se déroule surtout en public, sur un blog de discussion animé par Impagliazzo et Paturi (Université de Californie à San Diego) et par Ryan Williams (MIT). Sur le fil consacré à Lean, des contributeurs ont relancé les deux formalisations. Le 31 octobre, l'un d'eux notait que seul le noyau par défaut de Lean avait accepté la preuve d'OpenAI, alors que celle d'Anthropic passait aussi le vérificateur indépendant nanoda. Le 5 novembre, un autre a reproduit les deux suites sous macOS. Le 6 novembre, un troisième participant, aidé d'agents Claude, a dit avoir porté la preuve d'OpenAI vers une autre bibliothèque Lean, où quatre vérificateurs l'ont acceptée. Selon lui, le passage du modèle de machine de Mathlib à une machine de Turing multiruban standard est désormais formalisé pour les deux résultats, ce que ShiftDelete a également rapporté le 7 novembre. Il s'agit de comptes rendus de bénévoles, qui n'ont pas fait l'objet d'une relecture formelle.

Ce que disent les experts

D'après le résumé qu'en donne AI Weekly, un article du New York Times du 6 novembre cite Impagliazzo, qui parle d'une nouvelle « very shocking » (très surprenante). Les examinateurs disent n'avoir signé aucun accord de confidentialité et ne pas être rémunérés. À la demande de Williams, OpenAI a accepté de publier ses données brutes et de financer une conférence. Selon ShiftDelete, Impagliazzo a confié à Science ne pas en être totalement certain. Les trois organisateurs rappellent que leur implication ne doit pas être prise pour une certification.

Ce qui reste en suspens

Une vérification Lean montre seulement qu'un énoncé formel découle de ses définitions. Reste à juger, humainement, si ces définitions traduisent bien la version classique de l'ETH. La preuve Lean d'OpenAI établit une borne plus faible que celle de l'article. La borne plus fine doit donc encore être contrôlée. Même si la réfutation se confirme, Lance Fortnow souligne qu'elle porte sur k-SAT et non sur l'ensemble des problèmes NP. Des estimations extérieures citées par le Times suggèrent que le gain n'apparaîtrait que pour des tailles de problème astronomiques.