Pendant près de trois décennies, une hypothèse appelée l’hypothèse du temps exponentiel est restée discrètement au fondement de l’informatique théorique. Il ne s’agissait ni d’une loi, ni d’un théorème, mais d’une supposition si largement acceptée que des pans entiers de recherche ont été construits par-dessus. OpenAI affirme aujourd’hui que ses modèles d’IA ont produit un algorithme qui la réfute. Si cette découverte se confirme, les conséquences dépassent largement le cadre d’un simple article de recherche.
Ce que disait réellement l’hypothèse du temps exponentiel
L’hypothèse du temps exponentiel, proposée il y a environ 30 ans, répond à une question faussement simple: à quelle vitesse un ordinateur peut-il résoudre certains puzzles logiques? L’approche la plus directe est la force brute, qui consiste à tester toutes les combinaisons possibles de vrai ou de faux pour chaque variable du puzzle. L’ETH ne prétendait pas que c’était la seule méthode. Elle reconnaissait l’existence de raccourcis. Ce qu’elle proposait était une limite minimale: peu importe la finesse du raccourci, le travail de calcul requis doit toujours croître de manière exponentielle à mesure que le puzzle grandit.
Cela semble technique, mais l’implication pratique est importante. L’ETH constituait essentiellement une limite de vitesse pour une catégorie de problèmes. Elle indiquait aux chercheurs ce qui était, en principe, réalisable et ce qui ne l’était pas. Des branches entières d’algoritmes et de théorie de la complexité ont été développées en prenant cette limite pour acquise.
OpenAI affirme que ses modèles ont conçu un algorithme qui dépasse cette limite de vitesse supposée. L’affirmation est que l’ETH est fausse.
L’effet domino: ce qui se brise lorsqu’une fondation bouge
C’est ce que la plupart des articles sur cette annonce omettent. L’histoire ne se résume pas à une hypothèse erronée. Elle concerne ce qui a été construit par-dessus.
Fedor Fomin, de l’Université de Bergen, décrit la réaction des chercheurs comme un choc total. Il fait remarquer qu’un manuel qu’il a écrit sur le sujet deviendrait obsolète si la découverte est confirmée. Ce n’ét pas une exagération. De nombreuses conclusions en informatique ont été tirées en supposant que l’ETH était vraie. Si cette supposition tombe, ces conclusions ne tiennent plus. Comme le dit Fomin, le résultat nécessiterait une révision complète de plusieurs domaines liés aux algorithmes et à la complexité.
Leslie Goldberg, de l’Université d’Oxford, qualifie l’avancée, de manière conditionnelle, d’énorme percée. La condition a son importance: la découverte doit encore être vérifiée et, surtout, comprise. Stefan Szeider, de la TU Wien, a examiné ce qu’OpenAI a publié et s’attend à ce que cela résiste à l’examen, tout en notant que les chercheurs doivent encore confirmer que l’énoncé formellement prouvé signifie bien ce que ses auteurs prétendent. Cette distinction, entre une preuve techniquement valide et une preuve qui signifie ce que vous pensez qu’elle signifie, n’est pas anodine.
L’ETH est également liée à l’un des problèmes ouverts les plus célèbres en mathématiques: P versus NP. Il s’agit de savoir si les problèmes dont les réponses sont faciles à vérifier sont également faciles à résoudre. Le fait que l’ETH soit vraie aurait impliqué que la réponse est non. Mais Goldberg est explicite: réfuter l’ETH ne signifie pas que la réponse est oui. La question P versus NP reste ouverte.
OpenAI a utilisé Lean, un outil logiciel qui vérifie formellement les mathématiques des preuves, pour valider le résultat concernant l’ETH. L’entreprise a également mandaté un groupe d’examen indépendant comprenant Russell Impagliazzo et Ramamohan Paturi, tous deux de l’Université de Californie à San Diego, qui figuraient parmi les chercheurs ayant initialement proposé l’ETH. Leur lettre ouverte décrit cette découverte comme quelque chose susceptible de modifier un pan important de l’informatique théorique.
Des mathématiques faites par communiqué de presse, et pourquoi cette formule compte
Le résultat sur l’ETH n’était pas la seule annonce. OpenAI affirme également que son IA a prouvé une conjecture de 1991 sur le comportement des ondes, avec des implications sur la manière dont les ondes se propagent et sur la finesse d’une forme tout en contenant des segments de droite pointant dans toutes les directions. En physique théorique, l’entreprise affirme avoir prouvé que les théories quantiques des champs, y compris la chromodynamique quantique qui décrit la force forte maintenant les quarks ensemble, sont mathématiquement cohérentes et pas seulement utiles sur le plan expérimental. Des travaux touchant à l’existence de la théorie pure de Yang Mills, qui fait partie d’un problème mathématique à un million de dollars, n’ont pas été rendus publics pendant qu’un groupe dirigé par le prix Nobel David Gross les examine.
L’ampleur de ces annonces a suscité un certain malaise dans les milieux académiques. Magnus Wahlström, de Royal Holloway, à l’Université de Londres, décrit ce phénomène comme des mathématiques faites par communiqué de presse, soulevant l’inquiétude que des modèles d’IA propriétaires puissent soudainement bouleverser des mois de travail de chercheurs sans passer par le processus habituel d’évaluation par les pairs et de vérification graduelle.
Clément Canonne, de l’Université de Sydney, établit une distinction tranchée qu’il est utile de garder en tête: prouver quelque chose et comprendre pourquoi c’est vrai ne sont pas la même chose. Le réseau de découvertes qui reposait sur l’ETH s’est effondré. La raison de cet effondrement reste inconnue.
En bref
Une hypothèse qui a façonné l’informatique théorique pendant 30 ans a peut-être été réfutée par un modèle d’IA. Si cela est confirmé, les implications sont structurelles: les conclusions fondées sur l’ETH dans le domaine des algorithmes et de la théorie de la complexité devraient être revues. La découverte fait l’objet d’un examen indépendant, notamment de la part des chercheurs qui avaient initialement proposé l’hypothèse. Ce qui rend ce moment véritablement inhabituel n’est pas seulement le résultat en soi, mais le fossé qu’il révèle: les systèmes d’IA peuvent désormais produire des preuves que les humains ne peuvent pas encore expliquer pleinement. Ce fossé entre la preuve et la compréhension est là où le véritable travail commence.
D’après un reportage de New Scientist.