Le défi du « castor », une conjecture mathématique vieille de plus de 30 ans, résolu par une équipe constituée en partie d’« amateurs »

Ces derniers temps, recenser les exploits en informatique se réduisait à narrer les derniers progrès de l’intelligence artificielle. Le 2 juillet, l’annonce de la démonstration d’une conjecture vieille de plus de trente ans est venue bouleverser cette litanie. En plus, l’exploit, raconté par le média américain Quanta Magazine, n’est issu ni du monde académique ni de l’industrie. Il a été accompli par une équipe internationale constituée d’une vingtaine de personnes, collaborant à distance, en partie « amateurs », et réunie par le jeune Français Tristan Stérin.

Cofondateur de l’entreprise de logiciels PRGM, il a lancé, en mars 2022, le défi de résoudre un problème qui en a épuisé plus d’un : savoir quel programme informatique, parmi une famille de plus de 16 000 milliards, s’arrête pour donner sa réponse, éliminant de fait les programmes « inutiles » qui continuent ad vitam aeternam. Et surtout trouver la perle rare, celui qui stoppe après le plus grand nombre d’étapes. Le problème a été baptisé « compétition du castor affairé » par le mathématicien hongrois Tibor Rado, en 1962, en hommage aux vertus de l’animal.

« C’est comme la chasse au Pokémon ! » plaisante Tristan Stérin. Quel intérêt ? Ce « jeu », qui illustre comment la complexité jaillit de la simplicité, touche à de profondes questions en mathématiques et en informatique.

Le ruban de Turing Pour saisir l’enjeu, des rappels s’imposent. En 1936, le Britannique Alan Turing démontre que tout programme, depuis le simple « afficher “bonjour” » aux plus complexes, comme les énormes ChatGPT et consorts, peut se représenter « simplement » par une machine qui porte son nom : un ruban infini, marqué de 0 ou de 1 lorsqu’il passe sous une tête de lecture/écriture. La tête ne peut que changer les symboles 0 ou 1, faire avancer ou reculer le ruban d’une case et changer d’état. Cet « état », qui contient ces trois instructions (écrire 0 ou 1, avancer/reculer, changer d’état), est le logiciel de la machine. Il peut en avoir un, deux ou plus… Une machine à un état peut générer 25 programmes différents. De une à deux, 6 561, et de une à cinq, plus de 16 000 milliards.

Avec ce concept, Turing montre qu’il est impossible de trouver un programme qui dise si un autre programme va s’arrêter ou non. Le problème du castor affairé (« busy beaver » en anglais ou BB pour les intimes) présente une autre impossibilité : calculer le plus grand programme « utile », celui qui fait bouger le plus le ruban avant de s’arrêter et de donner la réponse. Tibor Rado a démontré que cette fonction n’était pas calculable : il est impossible de trouver toutes ces valeurs par une suite d’opérations.

Tibor Rado observe que, pour une machine à deux états, la fonction BB vaut six − un programme, dont le ruban a bougé de plus de six cases, est en fait un programme qui ne s’arrête jamais − et que BB (3), pour une machine à trois états, vaut 21. Dans les années 1970, Allen Brady montre que BB (4) vaut 107. En 1989, dans la quête de BB (5), Heiner Marxen et Jürgen Buntrock trouvent un « Pokemon » qui s’épuise au bout de 47 176 870 étapes. Et l’équipe de Tristan Stérin vient seulement de démontrer qu’il n’y a pas plus fort comme castor.

« Quand on demandait à George Mallory [un alpiniste britannique] pourquoi il voulait escalader l’Everest, il répondait parce que la montagne est là. C’est pareil ici. Ces nombres BB existent. A nous de les trouver », raconte Pascal Michel, enseignant émérite de l’université Paris Cité, spécialiste du sujet mais non membre de l’équipe. « BB (5) est un défi au savoir humain », complète Tristan Stérin.

Sortes de « Pokemons » inarrêtables L’aventure n’a pas été simple. Impossible de faire tourner 16 000 milliards de programmes pour voir lesquels s’arrêtent. Les « trappeurs » ont donc mis au point des « filets », appelés « décideurs », des programmes pour identifier des comportements de « Pokémons » inarrêtables. Il y a ceux qui bégaient et se répètent. Ceux qui comptent sans fin ânonnant sans faiblir des chiffres… Une demi-douzaine de « décideurs » ont permis de réduire le nombre de suspects. Mais il est resté au moins deux programmes très retors. L’un se met en boucle toutes les 8 468 569 863 opérations, mais seulement à partir d’un nombre gigantesque d’étapes (plus d’un million de milliards de milliards). Trompeur.

En avril, le travail était bien avancé, lorsque, sur le forum de discussion du groupe, un contributeur anonyme informe qu’il a traduit tout le travail réalisé jusqu’alors dans un langage informatique particulier, Coq. Et qu’il a même été plus loin, en achevant la démonstration rigoureuse avec ce langage. « L’apothéose finale ! » souligne Tristan Stérin. Coq est en effet l’un des outils phares pour démontrer qu’un programme n’a pas de bogues. Il est utilisé pour certifier la sécurité de logiciels critique. Après une vérification auprès de spécialistes de cette méthode, l’annonce que BB (5) est bien égal à 47 176 870 est faite. « Si la démonstration n’avait pas utilisé d’outils d’assistants de preuve, comme Coq, la communauté n’aurait pas eu confiance aussi vite dans le résultat, estime Yannick Forster, chercheur à l’Institut national de recherche en sciences et technologies du numérique et l’un des “vérificateurs”. En retour, ce travail donne une grande visibilité à Coq. » « J’ai été étonné par l’efficacité de cette recherche “massivement” parallèle. Les contributions étaient de grande qualité. Chaque mois il y en avait de nouvelles. Sans les autres, chacun n’aurait pas pu avancer », apprécie Tristan Stérin.

Et BB (6) ? Pas sûr que ce nouvel Everest soit accessible. Parmi les près de 60 millions de milliards de programmes à étudier, il y a des « monstres », baptisé cryptides. Prouver que ces castors ne s’arrêteront jamais de courir serait aussi dur que démontrer des conjectures mathématiques qui résistent, comme celle dite « de Collatz », une série d’entiers qui retombent toujours sur « 1 », quel que soit le nombre de départs. « Plutôt que m’attaquer à ce problème, je préfère me concentrer sur l’article scientifique qui expliquera à tous notre démonstration, et fournir des outils de travail collaboratif », prévoit Tristan Stérin, en castor avisé