Les modèles d’OpenAI et d’Anthropic réfutent l’hypothèse du temps exponentiel, établie de longue date

OpenAI et Anthropic ont tous deux publié des résultats générés par IA qui affirment réfuter l’hypothèse du temps exponentiel, une conjecture établie de longue date en théorie de la complexité computationnelle.

Le 26 octobre, OpenAI a annoncé que ses modèles avaient produit une preuve de la fausseté de l’hypothèse du temps exponentiel. Cette hypothèse, proposée au début des années 2000, affirme que 3-SAT ne peut pas être résolu en temps sous-exponentiel — ce qui signifie que certains casse-têtes logiques courants ne peuvent pas être résolus beaucoup plus rapidement qu’en testant toutes les réponses possibles par force brute.

L’hypothèse ayant été largement acceptée et utilisée dans des centaines d’articles pour établir des résultats conditionnels de difficulté computationnelle dans un large éventail de domaines, sa réfutation invaliderait une part importante de ces résultats et obligerait les chercheurs à réévaluer la difficulté computationnelle de problèmes dans des domaines tels que les algorithmes, la théorie des graphes et la biologie computationnelle.

L’entreprise d’IA a déclaré que ses modèles avaient généré la réfutation en langage naturel le 16 octobre, puis l’avaient formalisée le lendemain dans l’assistant de preuve mathématique Lean. Les deux éléments sont disponibles dans un dépôt GitHub public.

Selon OpenAI, le travail est examiné par un groupe externe dirigé par Russell Impagliazzo et Ramamohan Paturi, de l’UC San Diego — deux des auteurs à l’origine de l’hypothèse — ainsi que par Ryan Williams, du MIT.

Sur X, Williams a déclaré que les chercheurs cherchent encore à déterminer les implications pratiques de cette découverte.

« Au rythme actuel des progrès, il est plausible que nous assistions à une avancée importante dans la résolution pratique de SAT au cours des 12 prochains mois. Ou peut-être que nous ne verrons rien de tel. Je n’en sais vraiment rien », a déclaré Williams.

Par ailleurs, Anthropic a publié un article et une formalisation dans Lean 4 affirmant qu’un algorithme déterministe résout 3-SAT d’une manière qui réfuterait l’hypothèse du temps exponentiel. L’entreprise a déclaré qu’un modèle de recherche interne Claude avait découvert l’algorithme central le 16 octobre — le jour même où les modèles d’OpenAI avaient fait cette découverte — en utilisant 14 millions de jetons générés, sans intervention humaine.

« Le résultat est purement asymptotique et ne dit rien sur la résolution pratique de formules », a précisé Anthropic.

Entre-temps, OpenAI a également dévoilé deux autres résultats générés par IA : une preuve de la conjecture du lissage local dans toutes les dimensions en analyse harmonique, ainsi qu’une preuve d’existence mathématiquement rigoureuse pour certaines théories quantiques des champs, notamment la chromodynamique quantique et la théorie de Yang-Mills pure.