OpenAI et Anthropic disent avoir réfuté l'ETH, mais personne n'a encore validé la preuve

Deux laboratoires rivaux affirment, à quelques heures d’intervalle, que leurs systèmes d’IA ont trouvé un algorithme capable de résoudre 3-SAT en temps sous-exponentiel. Si ces résultats résistent à l’examen, une hypothèse utilisée depuis des décennies pour mesurer la difficulté de nombreux problèmes informatiques devra être réévaluée. Pour l’instant, il s’agit encore de revendications de recherche, pas d’un consensus établi.

L’ETH, une frontière théorique au cœur de l’informatique

L’Exponential Time Hypothesis (ETH) est une conjecture de complexité informatique. Elle affirme, sous une formulation courante, qu’il n’existe pas d’algorithme résolvant 3-SAT en temps \(2^{o(n)}\), où \(n\) représente notamment le nombre de variables de l’instance.

Le problème 3-SAT consiste à déterminer si une formule logique composée de clauses contenant trois variables — ou leur négation — peut être rendue vraie par une attribution appropriée de valeurs. Il s’agit d’un problème NP-complet, c’est-à-dire qu’il appartient à une vaste classe de problèmes dont la résolution rapide permettrait de résoudre rapidement tous les problèmes de la classe NP.

Dans la pratique, 3-SAT peut déjà être traité sur des instances limitées grâce à des solveurs très optimisés. L’ETH ne prétend pas que toute instance est impossible à résoudre. Elle pose une limite plus précise : à mesure que la taille des entrées augmente, aucun algorithme ne devrait éviter une croissance essentiellement exponentielle du temps de calcul.

Cette hypothèse sert de fondation à de nombreux résultats dits conditionnels. Lorsqu’un chercheur démontre qu’un problème ne peut pas être résolu sous un certain seuil de complexité « à moins que l’ETH soit fausse », il s’appuie sur cette frontière pour comparer la difficulté d’algorithmes et de problèmes très différents.

OpenAI affirme avoir obtenu un algorithme sous-exponentiel

Le 26 octobre, OpenAI a publié un résultat affirmant qu’un algorithme résout 3-SAT en temps sous-exponentiel. Une telle conclusion contredirait directement l’ETH, à condition que l’algorithme et sa preuve soient corrects dans le modèle de calcul considéré.

L’élément mis en avant par OpenAI concerne la formalisation du résultat avec Lean, un assistant de preuve qui permet de faire vérifier des énoncés mathématiques par un noyau logiciel. L’entreprise indique également avoir transmis ses documents à un groupe d’experts conduit par Russell Impagliazzo, Ramamohan Paturi et Ryan Williams.

Le choix de ces examinateurs n’est pas anodin. Tous trois sont des figures reconnues de la théorie de la complexité et sont directement associés aux travaux ayant contribué à établir le rôle de l’ETH dans l’analyse des algorithmes. Leur examen doit permettre de vérifier non seulement les étapes algébriques ou combinatoires, mais aussi la traduction exacte du résultat en termes de complexité.

La formalisation dans Lean constitue un signal important, mais elle ne clôt pas le débat à elle seule. Il faut encore déterminer si le théorème formalisé correspond bien à la question posée, si les hypothèses sont correctement encadrées et si le coût de l’algorithme est évalué sur toutes les instances concernées. Une preuve assistée par ordinateur peut sécuriser une chaîne logique ; elle ne dispense pas d’en examiner la portée mathématique.

Anthropic publie à son tour un résultat attribué à Claude

Quelques heures plus tard, Anthropic a mis en ligne une prépublication attribuée à un modèle de recherche Claude. Le document avance lui aussi un algorithme sous-exponentiel pour 3-SAT.

Cette seconde annonce renforce l’intérêt de la séquence, mais ne constitue pas une validation indépendante au sens scientifique. Les deux laboratoires n’ont pas présenté deux réplications évaluées par des équipes extérieures. Ils ont publié deux revendications rapprochées dans le temps, dont les détails techniques doivent encore être comparés.

Anthropic prend soin de préciser la nature asymptotique de son résultat. En clair, l’algorithme pourrait présenter une croissance théorique plus favorable que \(2^n\) lorsque la taille des instances tend vers l’infini, sans être utilisable sur des problèmes de taille réaliste.

La différence est essentielle. Un algorithme en \(2^{\sqrt n}\), par exemple, est sous-exponentiel au sens usuel, mais peut rester extrêmement lent pour les valeurs de \(n\) rencontrées dans des applications concrètes. Les constantes cachées, les étapes de prétraitement, la mémoire nécessaire et la structure exacte de l’algorithme peuvent rendre un tel résultat inutilisable pendant très longtemps.

Autrement dit, même une réfutation correcte de l’ETH ne transformerait pas automatiquement les solveurs de satisfaction logique en outils pratiques. Elle modifierait d’abord une frontière théorique.

Le point décisif : une annonce n’est pas encore une réfutation

L’enjeu porte moins sur la capacité des modèles à produire une idée originale que sur la vérification de cette idée. Plusieurs questions devront recevoir une réponse précise.

Le résultat couvre-t-il toutes les instances de 3-SAT, ou seulement une famille particulière ? Le temps annoncé est-il mesuré dans un modèle de calcul standard ? L’algorithme est-il déterministe, ou repose-t-il sur une procédure probabiliste dont le taux d’erreur doit être contrôlé ? Les paramètres dissimulés dans la notation asymptotique restent-ils indépendants de la taille du problème ? Enfin, les preuves formalisées décrivent-elles exactement l’algorithme présenté dans les articles ?

Ces vérifications sont particulièrement importantes lorsque la découverte est produite ou assistée par un modèle d’IA. Un système peut explorer rapidement un espace d’idées, proposer des transformations mathématiques ou générer une preuve apparemment cohérente. La difficulté consiste ensuite à établir qu’aucune condition implicite, aucun cas limite et aucune confusion entre une borne théorique et une procédure effective ne subsistent.

Le groupe d’experts mentionné par OpenAI représente donc le prochain filtre crédible. La publication de fichiers Lean et de documents techniques facilite l’audit, mais la reconnaissance par la communauté dépendra d’une lecture indépendante, d’éventuelles corrections et, idéalement, d’une reproduction par d’autres chercheurs.

Si l’ETH tombe, les conséquences seront d’abord théoriques

Une preuve valide aurait des effets considérables sur la théorie de la complexité. De nombreux résultats qui reposent sur l’ETH comme hypothèse devraient être reformulés. Certaines bornes inférieures conditionnelles — celles qui affirment qu’un problème ne peut pas être résolu sous un certain coût — deviendraient caduques ou exigeraient une nouvelle justification.

Le résultat ne démontrerait toutefois pas que P = NP. Un algorithme sous-exponentiel reste potentiellement bien plus lent qu’un algorithme polynomial. Il ne suffirait pas non plus à rendre tous les problèmes NP-complets praticables, ni à invalider directement les mécanismes cryptographiques utilisés dans les systèmes actuels. Les conséquences dépendraient de la forme exacte de l’algorithme et des problèmes auxquels il pourrait être réduit.

Le prochain jalon est donc concret : l’examen indépendant des preuves d’OpenAI et d’Anthropic, puis leur confrontation avec les définitions standard de l’ETH. Tant que Russell Impagliazzo, Ramamohan Paturi, Ryan Williams et d’autres spécialistes n’auront pas confirmé les résultats, l’ETH reste une hypothèse — et les deux annonces, des pistes spectaculaires mais non établies.