OpenAI et Anthropic revendiquent une percée : les humains vérifient encore
OpenAI et Anthropic affirment que leurs IA ont réfuté une hypothèse de 1999 sur 3-SAT. Un logiciel a contrôlé les preuves ; les humains relisent encore.
Le 26 octobre, OpenAI affirme que l’un de ses modèles internes a fait tomber une hypothèse posée en 1999 par deux chercheurs. Le lendemain, Anthropic publie sa propre réfutation, signée « Claude ». Reste une question simple : qui vérifie, quand ce sont les laboratoires eux-mêmes qui annoncent, et que la preuve d’Anthropic n’avait été relue par aucun humain à sa publication ?
Ce qui est revendiqué, en clair
En jeu : savoir si une barrière que les informaticiens croyaient solide existe vraiment. Si elle cède, des centaines de travaux perdent une partie de leur fondement.
Le problème s’appelle 3-SAT. On donne une liste de contraintes logiques portant sur des variables qui valent « vrai » ou « faux ». Il faut dire si une combinaison les satisfait toutes. Chaque variable ajoutée double le nombre de combinaisons à essayer. La méthode la plus bête, la « force brute », les teste toutes ; elle devient impraticable autour de cent variables, rappelle ActuIA.
En 1999, Russell Impagliazzo et Ramamohan Paturi, de l’université de Californie à San Diego, ont posé qu’aucun algorithme ne pouvait échapper à cette explosion, sauf par un facteur constant. C’est l’hypothèse du temps exponentiel, ou ETH. Les chercheurs s’en servent comme d’un étalon : pour montrer qu’un problème de planification ou de graphes ne se résoudra jamais vite, ils le ramènent à 3-SAT et invoquent l’ETH. Selon l’article d’Anthropic, cité par ActuIA, plus de 800 articles en dépendent, directement ou via une hypothèse apparentée.
En clair : les deux laboratoires disent avoir trouvé une méthode un peu plus rapide que « tout essayer », alors que l’ETH affirmait que c’était impossible.
Une chronologie serrée, deux preuves jumelles
En jeu : deux annonces quasi simultanées, venues de rivaux, sur un même résultat. Les deux laboratoires datent leur découverte du 16 octobre.
OpenAI a annoncé le 26 octobre qu’un de ses modèles internes avait réfuté l’ETH. Moins de six heures plus tard, selon ActuIA, Anthropic a publié un article de 49 pages, « A 2^o(n) Time Algorithm for 3-SAT », signé « Claude ». Chez Anthropic, l’algorithme central a été trouvé par un modèle de recherche interne, avec 14 millions de tokens produits (un token, c’est à peu près un demi-mot) et sans intervention humaine dans la découverte elle-même. C’est ce qu’a indiqué sur X le mathématicien d’Anthropic Levent Alpöge, selon OfficeChai, média cité par ActuIA.
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 ».
Un détail donne l’échelle. Pour que l’algorithme d’Anthropic batte la force brute sur une formule à cinq fois plus de contraintes que de variables, il faut dix puissance dix mille variables, soit un 1 suivi de 10 000 zéros. Il 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 le résultat jumeau.
Lean : un logiciel contrôle la preuve, pas son sens
En jeu : que veut dire « prouvé » quand personne n’a eu le temps de relire ? Les deux laboratoires ont joint une preuve formalisée dans Lean, un langage où chaque étape du raisonnement est contrôlée par un programme. Un peu comme un correcteur d’orthographe impitoyable, mais pour la logique.
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 et relu par d’autres instances des mêmes modèles. 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 bien des axiomes de départ. Elle ne garantit pas que l’énoncé traduit en Lean dit ce que les auteurs prétendent. Une erreur de traduction, et la machine valide parfaitement… autre chose. C’est ce que des humains doivent maintenant établir.
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. Selon The Next Web, cité par ActuIA, ils ont obtenu d’OpenAI la publication des données brutes et le financement d’une conférence. Le théoricien 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. Ryan Williams juge certaines parties routinières, mais deux ou trois éléments très inhabituels.
Ce que le résultat ne change pas, pour l’instant
En jeu : faut-il s’inquiéter pour la sécurité informatique ? Pour l’instant, la réponse rassure. Ryan Williams a demandé à Dan Roberts, responsable scientifique d’OpenAI, si des systèmes de chiffrement étaient touchés. Selon lui, OpenAI a vérifié et s’est dite « raisonnablement confiante » qu’aucun n’est cassé, rapporte TechCrunch, cité par ActuIA. RSA, très répandu, 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 astuces que l’ETH n’a jamais concernées. L’article d’Anthropic le dit lui-même : le résultat ne dit rien de la résolution des formules en pratique. Enfin, la question « P contre NP » reste ouverte, car un temps à peine sous-exponentiel est encore loin d’un temps rapide au sens strict.
En clair : sur le papier, c’est un séisme pour la théorie. Dans les machines, rien ne change demain matin.
Qui valide quand les laboratoires annoncent eux-mêmes ?
En jeu : la confiance. Ces annonces viennent des entreprises qui vendent les modèles, publiées sur leurs propres canaux, avant la relecture complète. Ce n’est pas une preuve de mauvaise foi, mais c’est un rapport de force à garder en tête.
OpenAI revendiquait aussi, le 26 octobre, une preuve de la conjecture de lissage local de Christopher Sogge, qui réglerait la conjecture de Kakeya. Elle annonçait de même une preuve de l’existence de la théorie de Yang-Mills pure en quatre dimensions. Cette dernière 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 », c’est-à-dire une inondation qui submerge ceux qui doivent répondre. Il a pourtant accepté d’organiser l’examen.
Le point de vigilance tient en une phrase d’ActuIA : la découverte se compte désormais en tokens, la vérification se compte toujours en mois de travail de chercheurs, et ce sont eux qui manquent. À observer dans les semaines qui viennent : le verdict de l’examen ouvert, la formulation exacte de l’énoncé Lean, et la question de savoir si des mathématiciens indépendants retrouvent seuls ces résultats.
