1 points par GN⁺ 2024-07-03 | 1 commentaires | Partager sur WhatsApp
  • Introduction

    • Il y a 40 ans, à Dortmund en Allemagne, des informaticiens se sont réunis pour rivaliser afin de trouver le cinquième Busy Beaver
    • Le Busy Beaver est un programme informatique simple dont le temps d’exécution devient extrêmement long
    • Ces programmes sont liés à de célèbres problèmes mathématiques non résolus et trouvent leur origine dans un vieux problème de l’informatique théorique
    • Il y a deux ans, le doctorant Tristan Stérin a lancé le Busy Beaver Challenge, auquel plus de 20 contributeurs du monde entier ont participé
    • Aujourd’hui, l’équipe a confirmé que la valeur de BB(5) est 47,176,870
  • S’arrêtera-t-elle ou non ?

    • Les programmes Busy Beaver sont écrits sous forme d’instructions pour un ordinateur théorique appelé machine de Turing
    • Une machine de Turing effectue des calculs en lisant et en écrivant des 0 et des 1 sur une bande infinie
    • Le problème consistant à prédire si une machine de Turing va s’arrêter ou tourner pour toujours s’appelle le problème de l’arrêt
    • Le problème de l’arrêt n’a pas de solution générale, ce qui rend la chasse au Busy Beaver encore plus fascinante
  • L’apparition du beaver

    • Le mathématicien Tibor Radó a inventé le jeu du Busy Beaver en 1962
    • Dans chaque groupe de règles, la machine de Turing qui s’exécute le plus longtemps est appelée le Busy Beaver
    • BB(n) désigne le nombre d’étapes qu’effectue une machine Busy Beaver à n règles avant de s’arrêter
  • Le troupeau de beavers de Brady

    • Allen Brady a développé dans les années 1960 des techniques de chasse au Busy Beaver, puis a déterminé en 1974 la valeur du quatrième Busy Beaver
    • BB(4) a été confirmé comme étant une machine qui s’arrête après 107 étapes
  • Le cinquième beaver

    • Lors du concours de Dortmund en 1984, la première grande chasse visant à trouver le cinquième Busy Beaver a commencé
    • En 1989, Heiner Marxen a découvert une machine qui s’arrête après 47,176,870 étapes
    • En 2003, Georgi Georgiev a interrompu la chasse à BB(5), laissant 43 machines de Turing non résolues
  • Appel à tous les chasseurs

    • Tristan Stérin a lancé le Busy Beaver Challenge en 2022, avec la participation de contributeurs du monde entier
    • Shawn Ligocki a rejoint l’équipe en 2022 et a apporté des contributions importantes
    • Justin Blanchard a développé la méthode du langage à bande fermée, l’une des techniques les plus puissantes de l’équipe
  • Approche du monstre

    • Skelet #1 et #17 étaient des machines particulièrement difficiles, et l’équipe a combiné diverses idées pour les résoudre
    • En mai 2023, un contributeur anonyme nommé mxdys a achevé une preuve Coq
  • Là où errent les beavers

    • L’équipe est en train de rédiger un article académique officiel, et certains travaillent déjà à trouver le prochain beaver
    • BB(6) semble difficile à résoudre en raison d’un problème analogue à la conjecture de Collatz

L’avis de GN⁺

  • Cet article offre un exemple fascinant d’exploration des limites de l’informatique théorique
  • Le Busy Beaver Challenge montre l’importance de la recherche collaborative
  • La résolution de BB(5) a une grande portée pour les communautés de l’informatique et des mathématiques
  • Parmi les projets aux caractéristiques similaires, on peut citer les recherches sur la conjecture de Collatz
  • Lorsqu’on adopte de nouvelles technologies ou de l’open source, la collaboration et la reproductibilité sont essentielles

1 commentaires

 
GN⁺ 2024-07-03
Commentaires sur Hacker News
  • Des commentaires sur le billet de blog de Scott Aaronson ont été partagés

    • Un lien vers un fil précédent connexe est fourni
  • Il existe diverses variantes du problème du Busy Beaver

    • Il existe une variante utilisant le lambda-calcul
    • Il existe une variante exprimée en complexité de Kolmogorov
  • L’histoire d’un ingénieur qui a quitté son emploi pour étudier le problème du Busy Beaver est partagée

    • On se demande si cet ingénieur est mxdys
  • Une mention d’une preuve Coq apparaît

    • Il est suggéré qu’il pourrait ne pas s’agir d’une preuve formalisée depuis le début, mais de la première preuve à avoir été formalisée
  • Un avis indique que l’article original de Tibor Radó sur le Busy Beaver est facile à lire et intéressant

    • Un lien vers une version moderne de l’article est fourni
  • Le problème de l’arrêt pour les programmes de machines de Turing à 5 états et 2 couleurs a été résolu

    • La possibilité de l’appliquer au cas à 2 états et 4 couleurs est évoquée
  • Il est fait mention de l’idée erronée selon laquelle les humains peuvent résoudre intuitivement le problème de l’arrêt

  • Une expérience d’écriture d’un programme pour résoudre le problème de Cutting Stock dans un projet personnel est partagée

    • Des méthodes d’optimisation similaires au programme de Brady ont été utilisées
  • Un avis estime qu’avoir pu prouver l’arrêt ou non de programmes de machines de Turing à 5 états relevait de la chance

  • Selon le billet de blog de Scott Aaronson, il existe 16,679,880,978,201 machines de Turing à 5 états

    • On se demande quel pourcentage d’entre elles s’arrête
  • Les valeurs de la fonction Busy Beaver sont partagées

    • Il est prouvé que BB(5) vaut 47,176,870
    • BB(6) est au moins égal à 10^10^...^10 (une tour d’exponentielles de 15 niveaux)