Com o quinto Busy Beaver, pesquisadores se aproximam dos limites da computação

• Introdução

  • Há 40 anos, cientistas da computação se reuniram em Dortmund, na Alemanha, para competir na busca pelo quinto Busy Beaver
  • Busy Beaver é um programa de computador simples cujo tempo de execução se torna extremamente longo
  • Esses programas estão ligados a famosos problemas em aberto da matemática e têm origem em um problema antigo da ciência da computação
  • Há dois anos, o estudante de pós-graduação Tristan Stérin iniciou o Busy Beaver Challenge, e mais de 20 colaboradores do mundo todo participaram
  • Hoje, a equipe confirmou o valor de BB(5) como 47.176.870

• Parar ou não parar

  • Os programas Busy Beaver são escritos como instruções para um computador teórico chamado máquina de Turing
  • A máquina de Turing realiza cálculos lendo e escrevendo 0 e 1 em uma fita infinita
  • O problema de prever se uma máquina de Turing vai parar ou rodar para sempre é chamado de problema da parada
  • O problema da parada não tem solução geral, o que torna a caça ao Busy Beaver ainda mais atraente

• A chegada do castor

  • O matemático Tibor Radó inventou o jogo do Busy Beaver em 1962
  • A máquina de Turing que roda por mais tempo em cada conjunto de regras é chamada de Busy Beaver
  • BB(n) representa o número de passos até uma máquina Busy Beaver com n regras parar

• A tropa de castores de Brady

  • Allen Brady desenvolveu técnicas de caça ao Busy Beaver nos anos 1960 e determinou o valor do quarto Busy Beaver em 1974
  • BB(4) foi identificado como a máquina que para após 107 passos

• O quinto castor

  • Na competição de Dortmund em 1984, começou a primeira grande caçada para encontrar o quinto Busy Beaver
  • Em 1989, Heiner Marxen descobriu uma máquina que para após 47.176.870 passos
  • Em 2003, Georgi Georgiev interrompeu a busca por BB(5), deixando 43 máquinas de Turing sem solução

• Chamando todos os caçadores

  • Tristan Stérin iniciou o Busy Beaver Challenge em 2022, com a participação de colaboradores do mundo todo
  • Shawn Ligocki entrou para a equipe em 2022 e fez contribuições importantes
  • Justin Blanchard desenvolveu o método de linguagem de fita fechada, uma das técnicas mais poderosas da equipe

• A aproximação do monstro

  • Skelet #1 e #17 eram máquinas particularmente difíceis, e a equipe combinou várias ideias para resolvê-las
  • Em maio de 2023, um colaborador anônimo chamado mxdys concluiu uma prova em Coq

• Onde os castores circulam

  • A equipe está escrevendo um artigo acadêmico formal, e alguns já estão tentando encontrar o próximo castor
  • BB(6) parece difícil de resolver por causa de um problema semelhante à conjectura de Collatz

Opinião do GN⁺

• Este artigo oferece um exemplo fascinante de exploração dos limites da ciência da computação
• O Busy Beaver Challenge mostra a importância da pesquisa colaborativa
• A resolução de BB(5) tem grande significado para as comunidades de ciência da computação e matemática
• Um projeto com características semelhantes é a pesquisa sobre a conjectura de Collatz
• Ao adotar novas tecnologias ou open source, colaboração e reprodutibilidade são importantes

[GN⁺]

Comentários do Hacker News

• Foi compartilhado um comentário sobre a postagem no blog de Scott Aaronson

  • Foi fornecido um link para uma thread anterior relacionada

• Existem várias variantes do problema Busy Beaver

  • Há uma variante que usa cálculo lambda
  • Há uma variante expressa em termos de complexidade de Kolmogorov

• Foi compartilhada a história de um engenheiro que largou o emprego para estudar o problema Busy Beaver

  • Perguntam se esse engenheiro é o mxdys

• Há uma menção a uma prova em Coq

  • Levanta-se a possibilidade de não ser uma prova organizada desde o início, mas a primeira prova organizada posteriormente

• Há a opinião de que o artigo original de Tibor Radó sobre o Busy Beaver é fácil de ler e divertido

  • Foi fornecido um link para uma versão moderna do artigo

• O problema da parada de programas de máquinas de Turing de 5 estados e 2 cores foi resolvido

  • Levanta-se a possibilidade de aplicar isso ao caso de 2 estados e 4 cores

• Há uma menção à ideia equivocada de que humanos conseguem resolver intuitivamente o problema da parada

• Foi compartilhada a experiência de escrever, em um projeto pessoal, um programa para resolver o problema Cutting Stock

  • Usava um método de otimização semelhante ao programa de Brady

• Há a opinião de que foi uma sorte ter sido possível provar se programas de máquinas de Turing de 5 estados param ou não

• Segundo a postagem no blog de Scott Aaronson, existem 16.679.880.978.201 máquinas de Turing de 5 estados

  • Perguntam qual porcentagem delas para

• Os valores da função Busy Beaver foram compartilhados

  • Foi provado que BB(5) = 47.176.870
  • BB(6) é no mínimo 10^10^...^10 (uma torre de expoentes com 15 níveis)