L'hypothèse du temps exponentiel réfutée par un modèle d'OpenAI ?

Le 26 octobre, OpenAI a publié dans le dépôt openai/math l’article « The Exponential Time Hypothesis is False ». D’après ce texte, un modèle interne d’OpenAI non dévoilé a réfuté l’hypothèse du temps exponentiel (ETH), l’une des hypothèses de base de la théorie de la complexité. Un groupe indépendant d’informaticiens, dont deux coauteurs de l’hypothèse elle-même, examine l’article ainsi que sa formalisation en Lean.

Qu’est-ce que l’hypothèse du temps exponentiel ?

L’ETH (Exponential Time Hypothesis) suppose que le problème 3-SAT, c’est-à-dire savoir si une formule logique dont les clauses comptent trois variables peut être satisfaite, ne peut pas être tranché plus vite qu’en temps 2^Ω(n) pour n variables. Plus simplement : à chaque variable supplémentaire, le temps croît de façon exponentielle, et aucun algorithme astucieux n’y changera rien.

L’hypothèse a été formulée par Russell Impagliazzo et Ramamohan Paturi (avec Francis Zane). Des centaines de travaux s’appuient sur l’ETH pour démontrer qu’un problème de graphes, de bases de données ou de biologie computationnelle « ne peut pas » être résolu plus vite (comme le rappelle The Next Web).

Qu’a démontré exactement le modèle d’OpenAI ?

L’article donne un algorithme déterministe qui compte exactement toutes les affectations satisfaisant une formule k-CNF pour tout k ≥ 2 fixé. Il fonctionne en espace polynomial et en temps (n + m)^O(1) · 2^(n/(log n)^(1/2+o(1))), donc sous-exponentiel. Le cas de 3-SAT suffit pour réfuter l’ETH.

Fait intéressant, l’algorithme ne se contente pas de répondre « oui » ou « non » : il compte les solutions. L’article en tire d’autres conséquences :

1. des algorithmes sous-exponentiels pour compter les colorations de graphes, les ensembles indépendants et les couplages parfaits,
2. des approximations aussi précises que l’on veut pour Max-k-SAT en temps sous-exponentiel,
3. une nouvelle borne inférieure sur la taille des circuits logiques pour la classe E^NP.

Selon The Next Web, le modèle a trouvé la preuve le 16 octobre, et le lendemain elle était déjà vérifiée en Lean (un langage formel permettant à un ordinateur de vérifier des démonstrations). Dans l’historique des modifications du dépôt, OpenAI indique que l’article a été mis en ligne avec sa formalisation en Lean.

Qui vérifie la preuve ?

Le groupe chargé d’examiner et d’expliquer la preuve est dirigé par Russell Impagliazzo, Ramamohan Paturi (UC San Diego) et Ryan Williams (MIT). D’après l’historique du dépôt, c’est justement à la demande de ce groupe que les documents ont été publiés immédiatement, pour que tout le monde puisse les vérifier. Williams a écrit sur X qu’un modèle interne d’OpenAI avait produit une « claimed refutation of ETH », c’est-à-dire une réfutation revendiquée de l’ETH.

Les chercheurs n’ont signé aucun NDA et ne sont pas payés pour ce travail (selon The Next Web). Ils ont demandé à OpenAI de rendre publiques toutes les données brutes et de financer une conférence sur les conséquences du résultat, et l’entreprise a accepté. Dans une lettre ouverte, ils précisent toutefois que leur participation ne vaut pas confirmation du résultat (« should not be taken as certification of the claim »), en ajoutant que si la preuve est correcte, « it will change an important part of theoretical computer science ».

Est-ce une nouveauté dans le monde de l’IA ?

Ce n’est pas la première publication de ce genre chez OpenAI. Comme on le sait, le 6 octobre l’entreprise a déposé dans le même dépôt plus de 700 articles mathématiques générés par le modèle. Le README du dépôt indique que le modèle a reçu environ 4 000 problèmes ouverts, et que chaque résultat a demandé en moyenne trois heures de « réflexion » au niveau de ChatGPT Pro.

Ce qui est nouveau, c’est que le 26 octobre OpenAI a annoncé trois résultats d’un coup et a choisi une voie différente pour chacun (comme le décrit Unite.AI) :

1. ETH : l’article et la preuve en Lean sont publics, et un groupe ouvert autour d’Impagliazzo, Paturi et Williams les vérifie.
2. La conjecture de Sogge sur le « local smoothing » en toutes dimensions, dont découlent selon OpenAI la conjecture de Kakeya et la conjecture de restriction de Stein : également publiée avec une preuve en Lean.
3. L’existence de la théorie de Yang-Mills et de la QCD en quatre dimensions (l’un des problèmes du millénaire de l’Institut Clay) : pas encore de documents. Un groupe dirigé par le prix Nobel David Gross a décidé de rédiger lui-même le résultat.

OpenAI déclare par ailleurs ne pas vouloir le mérite scientifique des découvertes de ses modèles. La reconnaissance doit revenir aux personnes qui les comprendront et les décriront. L’entreprise a aussi versé 5 millions d’USD à la Fondation Simons pour des ateliers et des conférences sur les résultats générés par l’IA.

À quoi faire attention ?

D’abord, à l’état de la vérification. Une formalisation en Lean est un signal fort, mais il faut toujours vérifier que le théorème énoncé en Lean dit vraiment la même chose que le texte de l’article. OpenAI écrit elle-même dans le README que certains résultats non formalisés peuvent contenir des erreurs, et le 7 octobre elle a retiré trois articles à cause d’une erreur de signe dans l’une des preuves. Prenons donc ce résultat avec du recul tant que le groupe n’a pas terminé son travail.

Ensuite, à ce que le résultat ne signifie pas. Les auteurs écrivent clairement qu’il n’en découle pas que tous les problèmes NP ont des algorithmes sous-exponentiels. Ce n’est donc pas une résolution du problème P vs NP, et le temps d’exécution croît toujours plus vite que n’importe quel polynôme.

Enfin, au rythme. Un résultat sur lequel les théoriciens travaillaient depuis plus de 20 ans aurait été trouvé par le modèle lors d’une évaluation interne. S’il se confirme, ce sera sans doute l’exemple le plus fort à ce jour d’une IA qui fait des découvertes autonomes en informatique théorique. Au passage, cela ramène le sujet des preuves formelles, dont j’ai parlé à propos de la vérification formelle avec Claude.

FAQ

Qu’est-ce que l’hypothèse du temps exponentiel ?

C’est l’hypothèse de la théorie de la complexité selon laquelle 3-SAT ne peut pas être résolu en moins de 2^Ω(n) pour n variables. Elle a été formulée par Impagliazzo et Paturi avec Francis Zane.

OpenAI a-t-elle résolu le problème P vs NP ?

Non. L’algorithme est sous-exponentiel mais pas polynomial, et les auteurs soulignent que le résultat ne s’étend pas à tous les problèmes NP.

La réfutation de l’ETH est-elle déjà confirmée ?

Pas encore. Il existe une formalisation en Lean, mais le groupe indépendant d’Impagliazzo, Paturi et Williams commence seulement à l’examiner et précise que sa participation ne vaut pas confirmation.

Quel modèle d’OpenAI a fait cela ?

Un modèle interne non dévoilé. Dans le README du dépôt, OpenAI ne donne pas son nom.