- Le Busy Beaver Challenge, auquel ont participé plus de 20 personnes dans le monde, a vérifié que le nombre Busy Beaver des machines de Turing à 5 règles est BB(5)=47 176 870
- Il est confirmé que la machine découverte en 1989 par Marxen et Buntrock, qui s’arrête après 47 176 870 étapes, est bien la machine à 5 règles qui s’arrête et s’exécute le plus longtemps
- L’équipe a traité des dizaines de millions de candidates en combinant une méthode par arbres de filiation pour réduire les doublons, des programmes de détection de non-arrêt et l’assistant de preuve Coq
- Le résultat final a été achevé sous la forme d’une preuve Coq de 40 000 lignes, dans laquelle mxdys a intégré les techniques de la communauté, et a été examiné par Yannick Forster, expert Coq à l’Inria
- Pour BB(6), une machine à 6 règles ressemblant à la conjecture de Collatz, Antihydra, apparaît comme un obstacle, au point que BB(5) pourrait être le dernier nombre Busy Beaver que l’humanité connaîtra exactement
BB(5) est confirmé
- L’équipe du Busy Beaver Challenge a vérifié la valeur exacte de BB(5), soit 47 176 870
- Cette valeur correspond au nombre maximal d’étapes qu’une machine de Turing à 5 règles qui finit par s’arrêter peut exécuter
- La vérification a utilisé le Coq proof assistant, qui certifie qu’une preuve mathématique a été construite sans erreur
- Cristopher Moore, du Santa Fe Institute, a jugé impressionnante l’ingénierie sociale et mathématique de ce travail
- Damien Woods, de la Maynooth University, a comparé la vitesse à laquelle le résultat a été obtenu au “Usain Bolt territory”
- L’intérêt principal de la valeur précise de BB(5) tient moins à ses applications dans d’autres domaines de l’informatique qu’à la prouesse réalisée à la frontière de l’incomputabilité
Le problème du Busy Beaver et le problème de l’arrêt
- Le problème du Busy Beaver ne porte pas sur un langage de programmation généraliste, mais sur les machines de Turing
- Une machine de Turing lit et écrit des 0 et des 1 sur un ruban infini, tandis que sa tête se déplace case par case en suivant une table de règles
- Chaque règle indique l’action suivante selon que la valeur actuellement lue est 0 ou 1
- Modifier la valeur ou la conserver
- Se déplacer vers la gauche ou vers la droite
- Désigner la prochaine règle à consulter
- Une règle spéciale définit quand la machine doit s’arrêter
- Déterminer en général si une machine de Turing finira par s’arrêter ou s’exécutera indéfiniment est le problème de l’arrêt
- Alan Turing a démontré qu’il n’existe pas de solution générale au problème de l’arrêt
- La chasse au Busy Beaver ne consiste pas à résoudre en général l’arrêt de toutes les machines, mais à classer chaque machine dans un ensemble fini où le nombre de règles est fixé
Le Busy Beaver game de Radó
- Dans un article de 1962, Tibor Radó a regroupé les machines de Turing par nombre de règles et défini le Busy Beaver game
- Dans l’ensemble de toutes les machines de Turing comportant n règles :
- Certaines machines s’exécutent indéfiniment
- Certaines machines s’arrêtent
- Parmi celles qui s’arrêtent, celle qui s’exécute le plus longtemps est le busy beaver
- Son nombre d’étapes d’exécution est BB(n)
- Pour établir BB(n), il faut vérifier le temps d’exécution de toutes les machines qui s’arrêtent et prouver que toutes les autres ne s’arrêtent pas
- La mesure du temps d’exécution peut généralement se faire par simulation informatique, mais prouver le non-arrêt revient presque à résoudre le problème de l’arrêt pour une machine donnée
- Shawn Ligocki, contributeur du Busy Beaver Challenge, voit ce travail comme une exploration de la “frontière de l’inconnu”
De BB(1) à BB(4)
- BB(1)=1 se vérifie facilement
- Si la première règle prévoit l’arrêt lorsqu’elle lit 0, la machine s’arrête à la première étape
- Sinon, elle continue de se déplacer le long du ruban rempli de 0
- Avec seulement 2 règles, on obtient déjà plus de 6 000 machines de Turing différentes ; avec 3 règles, des millions, et avec 4 règles, des milliards
- Allen Brady a intégré dans un programme informatique une méthode par arbres de filiation qui regroupe les machines ayant les mêmes premiers comportements afin de réduire les doublons
- Shen Lin a démontré avec Radó que BB(3)=21, un résultat publié en 1965
- Brady a découvert en 1966 une machine à 4 règles qui s’arrête après 107 étapes, puis a prouvé en 1974 qu’il s’agissait de BB(4)
- BB(4) est ensuite resté pendant plus de 40 ans le dernier nombre Busy Beaver connu de l’humanité
La chasse au cinquième Busy Beaver
- Le concours de Dortmund de 1984 a été la première grande chasse à BB(5)
- Les machines de Turing à 5 règles sont près de 17 billions, et les énumérer à raison d’une par milliseconde prendrait plus de 500 ans
- La machine la plus occupée trouvée par les participants de Dortmund s’arrêtait après plus de 100 000 étapes d’exécution
- Par la suite, un chercheur a trouvé une machine s’exécutant pendant plus de 2 millions d’étapes
- Heiner Marxen et Jürgen Buntrock ont développé des techniques mathématiques pour accélérer la simulation des machines de Turing
- En 1989, Marxen a fait tourner son programme pendant un week-end sur un nouvel ordinateur puissant de son entreprise et a découvert une machine qui s’arrête après 47 176 870 étapes
- Buntrock a reproduit le résultat, et les deux chercheurs ont publié un article début 1990
- Cette machine était bien le cinquième Busy Beaver, mais il a fallu plus de 30 ans supplémentaires pour prouver que toutes les machines restantes ne s’arrêtaient pas
Skelet et les machines non résolues
- Au début des années 2000, l’informaticien bulgare Georgi Ivanov Georgiev s’est approché de très près de BB(5)
- Pendant deux ans, Georgiev a consacré plusieurs heures par jour à améliorer un programme identifiant les machines qui ne s’arrêtent pas
- Le programme final comptait 6 000 lignes de code dense sans commentaires et mettait plus d’une semaine à s’exécuter
- Il laissait environ 100 machines de Turing non résolues, que Georgiev a ramenées à 43 par une analyse manuelle
- En 2003, Georgiev a publié ses résultats en ligne sous le pseudonyme Skelet, sur ce site
- Ces 43 machines difficiles ont fini par être appelées Skelet machines, d’après son pseudonyme
- Georgiev a déclaré qu’après deux années de travail intensif, il était trop épuisé pour trouver de nouvelles idées
La structure collaborative du Busy Beaver Challenge
- Tristan Stérin a lancé le Busy Beaver Challenge en 2022
- Le projet s’est déroulé sous forme de collaboration en ligne et est devenu une communauté internationale de plus de 20 personnes, avec de nombreux contributeurs sans qualifications académiques traditionnelles
- Stérin estimait qu’établir BB(5) nécessitait une preuve documentée et reproductible
- Le programme de Georgiev était très sophistiqué, mais difficile à examiner pour d’autres chercheurs
- Stérin a divisé le travail en s’appuyant sur les approches existantes
- Éliminer les machines redondantes grâce à la méthode par arbres de filiation de Brady
- Identifier les machines qui s’arrêtent en moins de 47 176 870 étapes
- Traiter les machines qui s’exécutent indéfiniment avec des programmes indépendants contenant chacun une méthode de preuve
- Le programme de première étape, écrit fin 2021, a généré une liste d’environ 120 millions de machines de Turing, suffisante pour déterminer BB(5)
- Environ un quart d’entre elles s’arrêtaient avant la machine de Marxen et Buntrock, et 88 millions restaient à examiner
- Stérin a aussi construit une interface en ligne de diagrammes espace-temps, qui affiche le comportement des machines sous forme de grille bidimensionnelle de 0 et de 1
Langages de ruban fermés et accélération de la collaboration
- Shawn Ligocki a rejoint le Busy Beaver Challenge en 2022 et a remis en usage la méthode des langages de ruban fermés créée par Marxen
- Cette méthode fournit un cadre mathématique unifié qui utilise les motifs du ruban d’une machine de Turing pour montrer qu’elle ne s’arrête pas
- Ligocki a écrit un billet de blog présentant la technique, mais ne savait pas comment écrire un programme couvrant tous les cas
- Justin Blanchard l’a implémentée après avoir rejoint le projet, et deux autres contributeurs en ont fortement accéléré l’exécution
- En quelques mois, la méthode des langages de ruban fermés est devenue l’un des outils les plus puissants de l’équipe
- Elle a même permis de traiter 10 des 43 Skelet machines laissées par Georgiev
- Ligocki estime que ce résultat n’aurait pas pu venir de la contribution d’une seule personne
Skelet #1, Skelet #17 et Coq
- Skelet #1 était une machine alternant des phases prévisibles et des phases chaotiques
- En mars 2023, Ligocki et Pavel Kropitz ont analysé Skelet #1 en renforçant les techniques de simulation accélérée vieilles de 30 ans de Marxen et Buntrock
- Skelet #1 n’est entré dans un cycle répétitif qu’après avoir dépassé 1 billion × 1 billion d’étapes, et ce cycle répétitif durait plus de 8 milliards d’étapes
- mei, programmeur autodidacte de 21 ans, a appris Coq puis a traduit en Coq plusieurs preuves du Busy Beaver Challenge
- mei a également transposé en Coq la preuve de non-arrêt de Skelet #1 produite par Ligocki et Kropitz, renforçant ainsi ce résultat
- Skelet #17 était une autre machine difficile sur laquelle Chris Xu a réalisé une percée
- La preuve de Xu était remarquable, mais elle contenait une intuition mathématique difficile à convertir dans la forme précise exigée par Coq
- L’équipe voulait une preuve raisonnablement reproductible, et non une preuve du type “faites tourner le programme pendant six mois”
Une preuve Coq de 40 000 lignes
- En avril 2024, un nouveau contributeur connu seulement sous le pseudonyme mxdys a rejoint l’effort pour achever la preuve Coq
- L’équipe ne connaît ni la localisation ni le parcours personnel de mxdys
- Le 10 mai, mxdys a publié sur Discord : “The Coq proof of BB(5) is finished.”
- En quelques semaines, mxdys a intégré les techniques et les résultats de la communauté dans une unique preuve Coq de 40 000 lignes
- La preuve est disponible dans le dépôt Coq-BB5
- Yannick Forster, expert Coq à l’Inria, a examiné cette preuve et estimé qu’il ne s’agissait pas d’une tâche facile à formaliser
- Le résultat confirme que la machine à 47 176 870 étapes trouvée par Marxen et Buntrock plus de 30 ans auparavant est bien le cinquième Busy Beaver
- Georgiev a indiqué qu’il ne s’attendait pas à voir ce problème résolu de son vivant
- Allen Brady est mort le 21 avril 2024 à l’âge de 90 ans, un mois avant l’achèvement de la preuve
BB(6) et la prochaine frontière
- Les contributeurs du Busy Beaver Challenge ont commencé à préparer un article académique officiel expliquant le résultat
- L’article devrait compléter la preuve Coq de mxdys par une preuve lisible par des humains
- Certains membres de l’équipe sont passés au Busy Beaver suivant
- mxdys et Racheline ont découvert dans BB(6) un obstacle qui semble difficile à surmonter
- Cet obstacle est une machine à 6 règles dont le problème de l’arrêt ressemble à la conjecture de Collatz
- Cette machine est appelée Antihydra
- Le lien entre machines de Turing et conjecture de Collatz remonte à un article de Pascal Michel de 1993, mais Antihydra semble être la plus petite machine impossible à résoudre sans percée conceptuelle en mathématiques
- Scott Aaronson estime que BB(5) pourrait être le dernier nombre Busy Beaver que l’humanité connaîtra
- Certains contributeurs prévoient de continuer à travailler sur des variantes du problème du Busy Beaver, mais tous les participants ne resteront pas dans la même direction
- Stérin a été convaincu par le Busy Beaver Challenge de l’efficacité de la recherche collaborative en ligne et souhaite développer des outils logiciels pour aider des projets collaboratifs dans d’autres domaines des mathématiques
1 commentaires
Avis sur Hacker News
Scott Aaronson a écrit un commentaire à propos de ce résultat : https://scottaaronson.blog/?p=8088
Et il y a aussi eu de gros fils de discussion plus tôt cette année au sujet des « leisure-class beavers » :
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
À l’origine, le problème du castor affairé a beaucoup de variantes, dont l’une est le castor affairé fonctionnel défini avec le lambda-calcul [1]
Comme on mesure la taille du programme en bits plutôt que le nombre d’états, on peut déterminer davantage de valeurs : jusqu’ici, on n’en a que 6 pour les machines de Turing, tandis qu’ici on est allé jusqu’à 37. L’écart entre la plus grande valeur connue et une valeur dépassant le nombre de Graham n’est lui aussi que de 13 bits de programme. Une variante étroitement liée [2] peut s’exprimer directement en termes de complexité de Kolmogorov, et Mikhail Andreev [3] considère que c’est important pour les applications en théorie de l’information
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
J’ai trouvé https://oeis.org/A141475, mais celle-ci donne 27 000 milliards pour 5
Je me souviens avoir vu une vidéo qui expliquait cette définition
J’ai travaillé pendant quelques années avec un ingénieur incroyablement, presque incompréhensiblement intelligent, qui a gravi les échelons d’IC plus vite que quiconque que j’aie vu dans une grande entreprise tech
Il est parti il y a quelques années et, quand je lui ai demandé quels étaient ses projets, il m’a dit qu’il allait travailler sur le problème du castor affairé. Je me demande si le contributeur anonyme mxdys, qui a finalisé la preuve formelle de BB(5) dans l’article, est cette personne, mais je ne le saurai probablement jamais
Je ne vois pas quelle est la récompense, et avec une intelligence aussi brillante, j’aimerais qu’il s’attaque à des problèmes plus directement liés à l’amélioration du monde
L’article original de Tibor Radó sur le castor affairé, « On Non-Computable Functions », est en fait assez facile et agréable à lire
Une version moderne avec des notes supplémentaires se trouve ici : https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
Ce qui frappe ici, c’est que la preuve est une preuve Coq
Je me demande si ce n’est pas la première preuve importante implémentée dès le départ dans un assistant de preuve, plutôt qu’une preuve déjà connue ensuite portée dans un assistant de théorèmes. Il y avait déjà eu des preuves assistées par ordinateur auparavant, mais le théorème des quatre couleurs ou la conjecture de Kepler n’ont été transférés dans un environnement de vérification formelle que plus tard
Le principal problème était que les décideurs et les preuves manuelles n’étaient pas bien organisés et suscitaient quelques doutes. En particulier, Skelet #1 nécessitait un programme dédié pour accélérer jusqu’au motif final [0], et pour Skelet #17, Xu a dû utiliser un raisonnement dense de 7 pages afin de prouver la non-terminaison [1]. La preuve Coq complète apporte le niveau de confiance indispensable à ces résultats
[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...
https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v
https://en.m.wikipedia.org/wiki/Four_color_theorem
Je n’ai peut-être pas compris exactement ce que signifie « environnement de vérification formelle », mais il me semble que le théorème des quatre couleurs a été démontré par ordinateur dès le départ. La tentative de preuve originale de Kempe comportait une faille, mais elle a fourni certains des outils de base utilisés dans les preuves ultérieures, et le théorème a finalement été démontré par ordinateur
Ce castor affairé a été découvert en 1990, et il est probable que toutes les machines de taille 5 aient été énumérées peu après
Félicitations à l’équipe. On peut donc dire que le problème de l’arrêt pour les programmes de machines de Turing à 5 états et 2 symboles sur ruban vierge est désormais résolu
Je me demande si quelqu’un a essayé d’appliquer la même technique au cas 2 états et 4 symboles. En général, les symboles sont plus puissants que les états, mais à ce niveau-là cela devrait peut-être rester traitable, avec possiblement des résultats inattendus. Les cas 6 états et 2 symboles, comme 2 états et 5 symboles, semblent tous deux difficiles à traiter, et peut-être même prouvablement difficiles. Au passage, il existe cette idée absurde mais étrangement répandue selon laquelle les humains pourraient intuiter la réponse au problème de l’arrêt grâce à l’œil de l’esprit ou à une quelconque mécanique quantique dans le cerveau ; évidemment, rien de tel n’est intervenu dans cette preuve
À ma connaissance, les décideurs actuellement utilisés suffisent déjà à prouver que tous les cas restants en 2×4 ne s’arrêtent pas. Donc, s’il n’y a pas de grosse erreur dans la conception des décideurs, le champion actuel donne Σ(2,4) = 2 050, S(2,4) = 3 932 964. Les résultats n’ont simplement pas encore été rassemblés au même endroit
En 2×5 il y a Hydra, et en 6×2 il y a Antihydra ; les deux calculent la même itération, seuls le point de départ et la condition d’arrêt diffèrent. La conjecture standard, en lien avec le problème des 3/2 de Mahler, est que cette itération est uniformément distribuée modulo 2 ; si on la prouvait, on obtiendrait des bornes supérieure et inférieure sur la proportion cumulée de 0 et de 1, ce qui permettrait presque certainement de prouver la non-terminaison des deux machines. Bien sûr, on ne connaît aucune méthode de preuve
Elle aurait utilisé un générateur de preuves fondé sur une théorie logique appelée Aleph*, et à cette époque on savait déjà depuis 1 500 ans que ZFC ne pouvait pas établir BB(18). Par rapport à 2024, aucun programme antérieur à l’utilisation d’Aleph* n’aurait pu, même en théorie, servir à une vérification brute de preuves pour résoudre BB(18). C’est à comparer au fait qu’aujourd’hui nous pouvons, en théorie, résoudre BB(??) en énumérant et en vérifiant des preuves ZFC
La position selon laquelle « les humains intuitent la réponse au problème de l’arrêt » signifie cela. À ma connaissance, il n’y a pas de raison théorique forte pour qu’une telle histoire future soit impossible. Et comme le castor affairé est non calculable, il a bien fallu que des humains développent de nouvelles théories pour créer les programmes nécessaires. Le mérite du résultat doit bien revenir à quelque chose, et puisque le programme n’existait pas à l’époque, on ne peut pas l’attribuer au calcul
Je me demande si tous les programmes non terminants de longueur 5 se sont trouvés, par hasard, être prouvablement non terminants
« Le fait que Σ(5) = 1 915 et S(5) = 2 358 064 ne sera jamais prouvé. Ou, si une borne inférieure plus grande est découverte, on peut remplacer cette valeur dans cette prédiction. »
La raison était qu’il paraissait probable que la nature ait placé, parmi les machines à 5 états en suspens, au moins un problème aussi insaisissable que la conjecture de Goldbach. Autrement dit, il pouvait très bien exister des motifs récursifs de non-terminaison dépassant nos capacités de reconnaissance. Heureusement, cette prédiction ne s’est pas réalisée, mais il s’en est fallu d’un état supplémentaire
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", in Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. This chapter can also be found in the 2nd ed., Springer, 1995, pp. 237–254.
Au sens pratique, d’autres ont déjà répondu. Au sens mathématique, il aurait été assez surprenant que BB(5) soit indécidable. Les machines à 5 états et 2 symboles sont trop petites pour encoder un comportement indécidable
Cela dit, comme conséquence des théorèmes d’incomplétude, il existe nécessairement un certain n pour lequel les mathématiques standard ne peuvent pas prouver la valeur de BB(n). Ces dernières années, plusieurs personnes ont cherché à trouver un tel n et à voir jusqu’où on pouvait l’abaisser ; le record actuel[0] est 745. Ce record peut probablement être encore abaissé, mais il reste un grand écart entre la plus grande valeur que nous connaissons, 5, et la plus petite dont nous savons qu’elle est inconnaissable, 745
[0] Si vous vous demandez ce que sont les « mathématiques standard », il s’agit du record actuel aussi bien pour ZFC que pour PA. Donc au moins pour PA, il devrait être possible de faire mieux. Jusqu’ici, il semble qu’on n’ait pas trouvé de meilleure méthode pour PA que pour ZFC, mais cela devrait forcément être possible, non ?
« Il y a seulement quatre jours, mxdys et une autre contributrice, Racheline, ont découvert pour BB(6) une barrière qui semble difficile à franchir. Il s’agit d’une machine à 6 règles dont le problème de l’arrêt ressemble à la conjecture de Collatz, un problème mathématique notoirement difficile. Le lien entre les machines de Turing et la conjecture de Collatz remonte à un article de 1993 du mathématicien Pascal Michel, mais la machine nouvellement découverte, baptisée “Antihydra”, semble être la plus petite machine impossible à résoudre sans percée conceptuelle en mathématiques. »
Pour un projet personnel, j’ai écrit un programme qui résout le problème de découpe de stock (https://en.wikipedia.org/wiki/Cutting_stock_problem)
Le stock incluait la découpe de pièces de formes /---/, /---| et |---|, et comme je ne voulais pas gaspiller de matière lors des coupes à 45 degrés, je ne pouvais pas, ou ne voulais pas, utiliser les programmes existants. J’ai trouvé intéressant que la description de la manière dont Brady a élagué les sous-arbres de recherche où les différences n’avaient pas d’importance pour optimiser la recherche de BB(4) ressemble beaucoup à ce que j’ai fait pour rendre mon programme rapide
D’après un billet de blog de Scott Aaronson, il existe 16 679 880 978 201 machines de Turing à 5 états
Je me demande si l’on sait quel pourcentage d’entre elles s’arrêtent. Modification : le nombre de machines de Turing à n états est (4n + 1)^(2n). J’ai trouvé des données pour de petits n qui ressemblent à l’analyse que je cherchais : https://github.com/LukasKalbertodt/beaver
Je ne l’ai pas trouvée sur le site bbchallenge.org, mais toutes les machines ont été classées
Dans l’ensemble, la preuve est plutôt courte. Elle fait 19 000 lignes de Coq, espaces et commentaires compris.
D’après mon expérience, si on la compilait sous forme d’article traditionnel, elle serait probablement beaucoup plus courte que la version Coq. Bien sûr, la longueur d’une preuve n’est pas une mesure de sa difficulté ni de sa complexité, mais elle peut servir d’indicateur très grossier.
Quand on parle des limites de la connaissance humaine, on pense souvent à des théorèmes démontrables mais trop complexes pour qu’un humain puisse les comprendre. La preuve la plus complexe dont nous disposions est sans doute la classification des groupes simples finis : elle s’étend sur des milliers, voire des dizaines de milliers de pages, et il est possible que presque personne sur Terre, voire personne, ne la comprenne entièrement.
Comme le dit l’article, BB(6) pourrait être indécidable. Mais il pourrait aussi exister une preuve de plusieurs millions de pages, hors de portée de l’humanité.