OpenAI revendique une réfutation d’ETH : ce que Lean vérifie vraiment

Pour comprendre la revendication, imaginons un ensemble de contraintes portant sur des variables qui peuvent prendre la valeur « vrai » ou « faux ». Dans le problème nommé 3-SAT, chaque contrainte concerne au plus trois variables. La question est de savoir s’il existe une combinaison qui satisfait toutes les contraintes à la fois. ETH pose une limite dans les cas les plus difficiles : aucun algorithme général ne pourrait éviter un temps de calcul exponentiel lorsque le problème grandit.^[2]

OpenAI revendique davantage qu’une méthode pour trouver si une solution existe : son algorithme compterait toutes les combinaisons satisfaisantes en temps sous-exponentiel, franchissant ainsi la limite posée par ETH. Le lien entre compter et décider est simple : un nombre de solutions nul signifie qu’aucune combinaison ne convient ; un nombre supérieur à zéro signifie qu’il en existe au moins une. Un comptage suffisamment rapide permettrait donc aussi de répondre rapidement à la question de départ.^[2]

C’est ici que deux contrôles différents deviennent indispensables. Lean vérifie mécaniquement qu’une proposition découle des définitions et des hypothèses inscrites dans son langage. Les chercheurs doivent, eux, vérifier que ces définitions représentent fidèlement le problème visé. Une chaîne logique correcte ne suffit pas si son point de départ ou sa conclusion ne correspond pas exactement à la question mathématique annoncée.^[2]

Dans ce dossier, OpenAI reconnaît en outre que la borne de temps de calcul vérifiée dans Lean est plus faible que celle mise en avant dans son article, tout en restant sous-exponentielle. Il faut donc séparer deux questions : la borne formalisée suffit-elle à réfuter ETH, et la borne plus ambitieuse du manuscrit est-elle également démontrée ? La seule mention « vérifié dans Lean » ne donne pas une réponse identique aux deux.^[2]

L’article d’OpenAI est daté du 17 octobre et révisé le 25 octobre. Russell Impagliazzo et Ramamohan Paturi, qui ont contribué à formuler ETH, participent à l’examen indépendant, avec Ryan Williams à la tête du groupe. Leur participation ne vaut pas approbation du résultat, et l’évaluation par les pairs n’est pas achevée. Comme dans le cas de BootLoops, vérifier les calculs de l’IA ne suffit pas à faire de la science : le contrôle technique et l’interprétation scientifique remplissent des fonctions différentes.^[2][3]

Si la réfutation était confirmée, elle changerait surtout la manière de justifier certaines limites du calcul. De nombreux travaux établissent une conclusion conditionnelle : si ETH est vraie, alors tel problème ne possède pas d’algorithme rapide. Ces démonstrations ne deviendraient pas logiquement fausses. En revanche, leur hypothèse de départ ne permettrait plus de conclure que la rapidité recherchée est impossible. Cela rouvrirait des pistes sans fournir, à soi seul, les algorithmes capables de les exploiter.^[2]

Il ne s’agirait donc ni d’une résolution de P contre NP, la question de savoir si tout problème dont on vérifie facilement une réponse se résout aussi facilement, ni d’une promesse de logiciels immédiatement plus rapides. OpenAI reconnaît que transformer ces gains théoriques en accélérations pratiques demanderait encore d’importantes recherches. Le résultat à surveiller est d’abord la validation d’une nouvelle limite théorique, pas un changement déjà acquis dans la vitesse de nos ordinateurs.^[1][2]