Dix puissance dix mille. C'est le nombre de variables qu'il faut à une formule logique comptant cinq fois plus de contraintes que de variables pour que l'algorithme publié le 27 octobre par Anthropic batte la méthode la plus bête, celle qui essaie toutes les combinaisons. La force brute devient déjà impraticable autour de cent variables. L'algorithme ne servira donc à rien en pratique. S'il est correct, il « changera une part importante de l'informatique théorique », écrivent pourtant les trois chercheurs chargés d'examiner un résultat jumeau.

Car il ne vient pas seul. Le 26 octobre, OpenAI annonçait qu'un de ses modèles internes avait réfuté l'hypothèse du temps exponentiel, une conjecture formulée en 1999 sur laquelle reposent des centaines de résultats. Moins de six heures plus tard, Anthropic publiait sa propre réfutation, un article de 49 pages intitulé « A 2^o(n) Time Algorithm for 3-SAT » et signé « Claude ». Les deux laboratoires datent leur découverte du même jour, le 16 octobre. Chez Anthropic, l'algorithme central a été trouvé par un modèle Claude de recherche interne, avec 14 millions de tokens produits et sans intervention humaine dans la découverte elle-même, a indiqué sur X le mathématicien d'Anthropic Levent Alpöge, selon OfficeChai.

Une conjecture dont dépendent plus de 800 articles

Le problème 3-SAT consiste à décider si l'on peut attribuer vrai ou faux à des variables de façon à satisfaire une liste de contraintes logiques. Chaque variable ajoutée double le nombre de combinaisons à essayer. En 1999, Russell Impagliazzo et Ramamohan Paturi, de l'université de Californie à San Diego, ont posé qu'aucun algorithme ne pouvait échapper à cette croissance exponentielle autrement que par une constante. C'est l'hypothèse du temps exponentiel, ou ETH.

Les chercheurs s'en servent comme d'un étalon. Quand ils veulent montrer qu'un problème de planification, de graphes ou de vérification ne se résoudra jamais vite, ils le ramènent à 3-SAT et invoquent l'ETH. Plus de 800 articles en dépendent, ETH ou une hypothèse apparentée, selon l'article d'Anthropic. Si la réfutation tient, leurs bornes inférieures perdent leur fondement, et des problèmes classiques comme la clique ou la couverture par sommets admettent en théorie des algorithmes plus rapides que prévu.

Deux preuves, une même borne, aucune relecture humaine achevée

Les deux algorithmes aboutissent à des bornes très proches, de l'ordre de 2 puissance n divisé par la racine du logarithme de n, à des facteurs secondaires près. C'est à peine moins qu'exponentiel. Mais l'ETH interdisait justement ce « à peine ».

Les deux laboratoires ont accompagné leur texte d'une preuve formalisée dans Lean, un langage où chaque étape est contrôlée par un programme. OpenAI dit avoir achevé la sienne le 17 octobre. Anthropic a fait vérifier la sienne par le noyau de Lean et par un second vérificateur indépendant, nanoda, selon son dépôt GitHub. Son annexe précise que ce développement a été écrit par des modèles d'IA, relu par d'autres instances des mêmes modèles, et qu'au moment de la rédaction aucune personne n'était connue pour l'avoir vérifié.

Une preuve formelle garantit que le théorème énoncé découle des axiomes. Elle ne garantit pas que l'énoncé formalisé dit bien ce que les auteurs prétendent. C'est ce que doivent maintenant établir des humains. OpenAI a demandé à Russell Impagliazzo et Ramamohan Paturi eux-mêmes, avec Ryan Williams, du MIT, d'organiser un examen ouvert. Dans leur lettre à la communauté, les trois chercheurs préviennent que leur participation ne vaut pas certification. Ils ont obtenu d'OpenAI la publication des données brutes et le financement d'une conférence, selon The Next Web. Le théoricien de la complexité Lance Fortnow, qui dit ne pas avoir vérifié la preuve lui-même, estime le 28 octobre sur son blog qu'on peut désormais considérer l'hypothèse comme morte.

Ni les clés de chiffrement ni les solveurs ne bougent

La question qu'un responsable de la sécurité se pose en premier a, pour l'instant, une réponse rassurante. Ryan Williams a demandé à Dan Roberts, responsable scientifique d'OpenAI, si des systèmes cryptographiques étaient touchés : selon lui, OpenAI a vérifié et s'est dite « raisonnablement confiante » qu'aucun n'était cassé, a rapporté TechCrunch. RSA repose sur la factorisation des entiers, qui n'est pas connue pour être aussi difficile que 3-SAT. Ryan Williams estime toutefois que des raffinements de l'algorithme pourraient un jour concerner des systèmes dimensionnés sur des tailles de clés précises.

Les solveurs SAT industriels, qui vérifient des puces ou planifient des chaînes logistiques, ne gagnent rien non plus : ils traitent des millions de variables avec des heuristiques que l'ETH n'a jamais concernées. L'article d'Anthropic l'écrit lui-même, le résultat ne dit rien de la résolution des formules en pratique. P contre NP reste ouvert. Un temps à peine sous-exponentiel est encore loin d'un temps polynomial.

Le goulot passe de la découverte à la vérification

Ce 26 octobre, OpenAI revendiquait aussi une preuve de la conjecture de lissage local de Christopher Sogge dans toutes les dimensions, qui réglerait la conjecture de Kakeya, et une preuve de l'existence de la théorie de Yang-Mills pure en quatre dimensions, qui ne règle qu'une partie de l'un des sept problèmes du millénaire de l'Institut Clay. Pour la physique, le groupe dirigé par le prix Nobel David Gross a choisi de ne pas publier pour l'instant le matériel produit par l'IA.

Début octobre, OpenAI avait déjà diffusé d'un coup 722 articles de mathématiques produits par ses modèles. Ryan Williams avait qualifié cette salve d'« attaque DDoS contre les mathématiciens ». Il a pourtant accepté d'organiser l'examen. Il juge certaines parties de la preuve routinières, mais deux ou trois éléments très inhabituels.

La découverte, désormais, se compte en tokens. La vérification se compte toujours en mois de travail de chercheurs, et ce sont eux qui manquent.

Citations traduites de l'anglais par ActuIA.

Nos articles remonteront en priorité dans « À la une » de Google.