Pesquisadores chegam ao limite da computação com o quinto Busy Beaver
(quantamagazine.org)- O Busy Beaver Challenge, com a participação de mais de 20 pessoas no mundo todo, verificou que o número Busy Beaver para máquinas de Turing com 5 regras é BB(5)=47.176.870
- Foi confirmado que a máquina encontrada em 1989 por Marxen e Buntrock, que para após 47.176.870 passos, é de fato a máquina que para com 5 regras que roda por mais tempo
- A equipe combinou a abordagem de genealogia para reduzir candidatos duplicados, programas para detectar não-parada e o assistente de provas Coq para processar dezenas de milhões de candidatos
- O resultado final foi consolidado por mxdys em uma prova em Coq com 40.000 linhas que integra as técnicas da comunidade, e revisado pelo especialista em Coq da Inria, Yannick Forster
- Em BB(6), a máquina de 6 regras Antihydra, com um comportamento parecido com a conjectura de Collatz, surgiu como barreira, levantando a possibilidade de que BB(5) seja o último número Busy Beaver que a humanidade conhecerá exatamente
BB(5) foi confirmado
- A equipe do Busy Beaver Challenge verificou que o valor exato de BB(5) é 47.176.870
- Esse valor representa o número máximo de passos que uma máquina de Turing com 5 regras e que para pode executar
- A verificação usou o Coq proof assistant, que certifica se uma prova matemática foi construída sem erros
- Cristopher Moore, do Santa Fe Institute, avaliou como impressionante a engenharia social e matemática desse trabalho
- Damien Woods, da Maynooth University, comparou a velocidade com que o resultado saiu a “território de Usain Bolt”
- O ponto central de BB(5) não está em aplicações a outras áreas da ciência da computação, mas no fato de ser um resultado obtido na fronteira da incomputabilidade
O problema do Busy Beaver e o problema da parada
- O problema do Busy Beaver trata de máquinas de Turing, não de linguagens de programação gerais
- Máquinas de Turing leem e escrevem 0s e 1s sobre uma fita infinita, enquanto o cabeçote se move uma casa por vez seguindo uma tabela de regras
- Cada regra define a próxima ação conforme o valor lido no momento, 0 ou 1
- altera ou mantém o valor
- move para a esquerda ou para a direita
- define qual regra consultar em seguida
- uma regra especial define quando a máquina deve parar
- O problema de determinar, em geral, se uma máquina de Turing vai eventualmente parar ou rodar para sempre é o problema da parada
- Alan Turing provou que não existe solução geral para o problema da parada
- A busca pelo Busy Beaver, em vez de resolver de forma geral se todas as máquinas param, consiste em classificar cada máquina dentro de um conjunto finito com número fixo de regras
O Busy Beaver game de Radó
- Tibor Radó definiu em um artigo de 1962 o Busy Beaver game, agrupando máquinas de Turing pelo número de regras
- No conjunto de todas as máquinas de Turing com n regras:
- algumas máquinas rodam para sempre
- algumas máquinas param
- entre as que param, a que roda por mais tempo é a busy beaver
- o número de passos dessa execução é BB(n)
- Para determinar BB(n), é preciso verificar o tempo de execução de todas as máquinas que param e provar que todas as demais não param
- Medir o tempo de execução normalmente é possível por simulação em computador, mas provar a não-parada se aproxima de resolver o problema da parada para máquinas específicas
- O colaborador do Busy Beaver Challenge Shawn Ligocki descreve esse trabalho como algo feito na “fronteira do desconhecido”
De BB(1) a BB(4)
- BB(1)=1 é fácil de verificar
- se a primeira regra mandar parar ao ler 0, a máquina para no primeiro passo
- caso contrário, ela continua se movendo sobre a fita preenchida com 0s
- Com apenas 2 regras, já existem mais de 6.000 máquinas de Turing diferentes; com 3 regras, milhões; com 4, bilhões
- Allen Brady integrou a um programa de computador a abordagem de genealogia, que reduz duplicações ao agrupar máquinas com o mesmo comportamento inicial
- Shen Lin, junto com Radó, provou BB(3)=21, e o resultado foi publicado em 1965
- Em 1966, Brady encontrou uma máquina de 4 regras que para após 107 passos, e em 1974 provou que ela é BB(4)
- BB(4) foi, por mais de 40 anos, o último número Busy Beaver conhecido pela humanidade
A caça ao quinto Busy Beaver
- A competição de Dortmund, em 1984, foi a primeira grande busca por BB(5)
- Existem quase 1,7 trilhão de máquinas de Turing com 5 regras, e mesmo listando uma por milissegundo seriam necessários mais de 500 anos
- A máquina mais “ocupada” encontrada pelos participantes de Dortmund parava depois de mais de 100.000 passos
- Depois disso, outro pesquisador encontrou uma máquina que rodava por mais de 2 milhões de passos
- Heiner Marxen e Jürgen Buntrock desenvolveram técnicas matemáticas para acelerar a simulação de máquinas de Turing
- Em 1989, Marxen rodou o programa durante um fim de semana em um novo computador potente da empresa e encontrou uma máquina que parava após 47.176.870 passos
- Buntrock reproduziu o resultado, e os dois publicaram um artigo no começo de 1990
- Essa máquina era de fato o quinto Busy Beaver, mas ainda seriam necessários mais de 30 anos para provar que todas as máquinas restantes não param
Skelet e as máquinas não resolvidas
- No começo dos anos 2000, o cientista da computação búlgaro Georgi Ivanov Georgiev chegou muito perto de BB(5)
- Georgiev passou dois anos aprimorando um programa para identificar máquinas que não param, dedicando várias horas por dia a isso
- O programa final tinha 6.000 linhas de código denso, sem comentários, e levava mais de uma semana para rodar
- Esse programa deixou cerca de 100 máquinas de Turing sem solução, e Georgiev reduziu esse número manualmente para 43
- Em 2003, Georgiev publicou os resultados online sob o pseudônimo Skelet
- Essas 43 máquinas difíceis passaram a ser chamadas de máquinas Skelet, em referência ao seu pseudônimo
- Georgiev disse que, após dois anos de trabalho intenso, estava exausto demais para continuar tendo novas ideias
A estrutura colaborativa do Busy Beaver Challenge
- Tristan Stérin iniciou o Busy Beaver Challenge em 2022
- O projeto foi conduzido de forma colaborativa online e cresceu até virar uma comunidade internacional com mais de 20 pessoas, incluindo muitos colaboradores sem credenciais acadêmicas tradicionais
- Stérin considerava que, para fechar BB(5), era necessária uma prova documentada e reproduzível
- O programa de Georgiev era avançado, mas difícil para outros pesquisadores revisarem
- Stérin dividiu o trabalho com base em abordagens existentes
- remover máquinas duplicadas com a abordagem de genealogia de Brady
- identificar máquinas que param antes de 47.176.870 passos
- tratar as máquinas que rodam para sempre com programas independentes, cada um contendo seu próprio método de prova
- O programa da primeira etapa, escrito no fim de 2021, gerou uma lista de cerca de 120 milhões de máquinas de Turing suficiente para decidir BB(5)
- Cerca de um quarto delas parava antes da máquina de Marxen e Buntrock, e 88 milhões continuaram na lista de análise
- Stérin também criou uma interface online com diagramas espaço-tempo que mostram o comportamento das máquinas como grades bidimensionais de 0s e 1s
Linguagem de fitas fechadas e aceleração da colaboração
- Shawn Ligocki entrou no Busy Beaver Challenge em 2022 e reviveu o método da linguagem de fitas fechadas criado por Marxen
- Esse método fornece uma estrutura matemática unificada para mostrar que uma máquina de Turing não para com base em padrões observados na fita
- Ligocki escreveu um post de blog apresentando a técnica, mas não sabia como implementar um programa que cobrisse todos os casos
- Depois que Justin Blanchard entrou no projeto, ele implementou a técnica, e outros dois colaboradores aumentaram bastante a velocidade de execução
- Em poucos meses, o método da linguagem de fitas fechadas se tornou uma das ferramentas mais poderosas da equipe
- A técnica também conseguiu resolver 10 das 43 máquinas Skelet deixadas por Georgiev
- Ligocki avalia que esse resultado não teria surgido a partir da contribuição de uma só pessoa
Skelet #1, Skelet #17 e Coq
- Skelet #1 era uma máquina que alternava entre fases previsíveis e fases caóticas
- Em março de 2023, Ligocki e Pavel Kropitz analisaram a Skelet #1 reforçando a técnica de simulação acelerada criada por Marxen e Buntrock 30 anos antes
- A Skelet #1 só entrou em um ciclo repetitivo depois de ultrapassar 1 trilhão × 1 trilhão de passos, e esse ciclo tinha mais de 8 bilhões de passos
- mei, um programador autodidata de 21 anos, aprendeu Coq e depois traduziu para Coq várias provas do Busy Beaver Challenge
- mei também levou para Coq a prova de não-parada da Skelet #1 feita por Ligocki e Kropitz, tornando esse resultado mais sólido
- Skelet #17 era outra máquina difícil em que Chris Xu conseguiu um avanço decisivo
- A prova de Xu era excelente, mas incluía intuições matemáticas difíceis de converter para o formato preciso exigido pelo Coq
- A equipe queria provas razoavelmente reproduzíveis, e não algo do tipo “rode o programa por 6 meses”
A prova em Coq com 40.000 linhas
- Em abril de 2024, um novo colaborador conhecido apenas pelo pseudônimo mxdys juntou-se ao esforço para concluir a prova em Coq
- Nem a localização nem o histórico pessoal de mxdys são conhecidos pela equipe
- Em 10 de maio, mxdys publicou no Discord: “The Coq proof of BB(5) is finished.”
- Em poucas semanas, mxdys integrou as técnicas e resultados da comunidade em uma única prova em Coq com 40.000 linhas
- A prova foi publicada no repositório Coq-BB5
- Yannick Forster, especialista em Coq da Inria, revisou a prova e avaliou que não foi algo fácil de formalizar
- Com isso, ficou confirmado que a máquina de 47.176.870 passos, encontrada por Marxen e Buntrock há mais de 30 anos, é de fato o quinto Busy Beaver
- Georgiev disse que não esperava ver esse problema resolvido durante sua vida
- Allen Brady morreu aos 90 anos em 21 de abril de 2024, um mês antes da conclusão da prova
BB(6) e a próxima fronteira
- Os colaboradores do Busy Beaver Challenge começaram a preparar um artigo acadêmico formal explicando o resultado
- O artigo deve complementar a prova em Coq de mxdys com uma demonstração legível por humanos
- Parte da equipe já passou ao próximo Busy Beaver
- mxdys e Racheline encontraram em BB(6) uma barreira que parece muito difícil de superar
- Essa barreira é uma máquina de 6 regras cujo problema de parada se parece com a conjectura de Collatz
- Essa máquina é chamada de Antihydra
- A conexão entre máquinas de Turing e a conjectura de Collatz remonta a um artigo de Pascal Michel, de 1993, mas a Antihydra parece ser a menor máquina que não pode ser resolvida sem um avanço conceitual na matemática
- Scott Aaronson considera possível que BB(5) seja o último número Busy Beaver que a humanidade venha a conhecer
- Alguns colaboradores planejam continuar trabalhando em variantes do problema do Busy Beaver, mas nem todos os participantes seguirão na mesma direção
- Stérin disse que o Busy Beaver Challenge o convenceu da eficácia da pesquisa colaborativa online, e ele quer desenvolver ferramentas de software para ajudar projetos colaborativos em outras áreas da matemática
1 comentários
Comentários do Hacker News
Há um comentário de Scott Aaronson sobre esse resultado: https://scottaaronson.blog/?p=8088
E também há grandes threads do início deste ano sobre os “leisure-class beavers”:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
O problema do castor ocupado original tem muitas variantes, e uma delas é o castor ocupado funcional definido por cálculo lambda [1]
Como ela mede o tamanho do programa em bits, e não o número de estados, é possível determinar mais valores; até agora, há apenas 6 para máquinas de Turing, enquanto nessa variante já se chegou a 37. O intervalo entre o maior valor conhecido e um valor que supera o Graham's Number também é de apenas 13 bits de programa. Uma variante intimamente relacionada [2] pode ser expressa diretamente pela complexidade de Kolmogorov, e Mikhail Andreev considera isso importante para aplicações em teoria da informação [3]
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
Encontrei https://oeis.org/A141475, mas ali aparece 27 trilhões para 5
Lembro de ter visto um vídeo explicando essa definição
Trabalhei por alguns anos com um engenheiro incrivelmente inteligente, a ponto de ser difícil de compreender, que subiu nos níveis de IC mais rápido do que qualquer pessoa que vi em uma empresa de tecnologia de elite
Ele saiu há alguns anos e, quando perguntei sobre seus planos, disse que iria pesquisar o problema do castor ocupado. Fico me perguntando se o colaborador anônimo mxdys, que finalizou a prova formal de BB(5) no artigo, é essa pessoa, mas provavelmente nunca vou saber
Não sei qual é a recompensa, e, com uma inteligência tão excepcional, eu gostaria que resolvesse problemas mais diretamente relacionados a melhorar o mundo
O artigo original de Tibor Radó sobre o castor ocupado, “On Non-Computable Functions”, é de fato uma leitura bem fácil e divertida
Há uma versão moderna com anotações adicionais aqui: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
O que chama atenção aqui é que a prova é uma prova em Coq
Fico me perguntando se é a primeira prova importante implementada desde o início em um assistente de teoremas, em vez de uma prova já conhecida ser portada para um. Já houve provas assistidas por computador antes, mas o teorema das quatro cores e a conjectura de Kepler só foram posteriormente levados para um ambiente de verificação formal
O principal problema era que os decisores e as provas manuais não estavam organizados e eram um tanto suspeitos. Em especial, o Skelet #1 exigiu um programa dedicado para acelerar até o padrão final [0], e, para o Skelet #17, Xu teve de usar uma argumentação densa de 7 páginas para provar a não parada [1]. A prova completa em Coq fornece a confiança de que esses resultados precisavam
[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
Talvez eu não tenha entendido exatamente o que significa “ambiente de verificação formal”, mas entendo que o teorema das quatro cores foi provado por computador desde o início. A tentativa original de prova de Kempe tinha falhas, mas forneceu algumas das ferramentas básicas usadas em provas posteriores, e, no fim, o teorema parece ter sido provado por computador
Esse castor ocupado foi descoberto em 1990, e é bem possível que todas as máquinas de tamanho 5 tenham sido enumeradas logo depois
Parabéns à equipe. Agora, o problema da parada para programas de máquina de Turing de 5 estados e 2 símbolos com fita em branco está essencialmente resolvido
Fico curioso se alguém já tentou aplicar as mesmas técnicas ao caso de 2 estados e 4 símbolos. Em geral, símbolos são mais poderosos que estados, mas isso talvez seja tratável, e poderia haver resultados inesperados. Tanto 6 estados e 2 símbolos quanto 2 estados e 5 símbolos parecem difíceis de lidar, e talvez sejam demonstravelmente difíceis. Além disso, existe a ideia absurda, mas estranhamente difundida, de que humanos conseguem intuir a solução do problema da parada por meio do olho da mente ou de alguma mecânica quântica no cérebro; obviamente nada disso teve qualquer papel nesta prova
Pelo que sei, os decisores usados atualmente já são suficientes para provar que todos os casos restantes de 2×4 não param. Portanto, se não houver um erro grande no desenho dos decisores, o campeão atual dá Σ(2,4) = 2.050, S(2,4) = 3.932.964. O resultado apenas ainda não foi organizado em um só lugar
Em 2×5 há a Hydra, e em 6×2 há a Antihydra; as duas calculam a mesma iteração, diferindo apenas no ponto de partida e na condição de parada. A conjectura padrão, relacionada ao problema 3/2 de Mahler, é que essa iteração é uniformemente distribuída módulo 2; provar essa conjectura daria limites superior e inferior para a razão acumulada de 0s e 1s, permitindo provar quase com certeza que as duas máquinas não param. Claro, não há nenhum método de prova conhecido
Foi usado um gerador de provas baseado em uma teoria lógica chamada Aleph*, e naquela época já se sabia havia 1.500 anos que ZFC não conseguia estabelecer BB(18). Em comparação com 2024, nenhum programa anterior ao uso do Aleph* poderia, nem mesmo em teoria, ser usado para uma verificação de provas por força bruta a fim de resolver BB(18). Isso contrasta com o fato de que hoje podemos, em teoria, resolver BB(??) enumerando e verificando provas em ZFC
A posição de que “humanos intuem a solução do problema da parada” quer dizer algo assim. Até onde sei, não há uma razão teórica forte para essa história futura ser impossível. E, como o Busy Beaver é incomputável, humanos precisariam desenvolver novas teorias para criar o programa necessário. O mérito do resultado precisa ser atribuído a alguma coisa e, como o programa não existia na época, não pode ser atribuído à computação
Fico curioso se todos os programas de comprimento 5 que não param por acaso eram todos prováveis como não parantes
“O fato de que Σ(5) = 1.915 e S(5) = 2.358.064 jamais será provado. Ou, se um limite inferior maior for encontrado, substitua-se esse novo valor nesta previsão.”
O motivo era que havia uma boa chance de a natureza ter escondido, entre as máquinas de 5 estados pendentes, pelo menos um problema tão esquivo quanto a conjectura de Goldbach. Em outras palavras, havia uma boa chance de existir um padrão recursivo de não parada além da nossa capacidade de reconhecer. Felizmente essa previsão não se concretizou, mas foi por apenas um estado extra
[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. Este capítulo também pode ser encontrado na 2ª ed., Springer, 1995, pp. 237–254.
No sentido prático, outras pessoas já responderam. No sentido matemático, eu teria achado bem surpreendente se BB(5) fosse indecidível. 5 estados e 2 símbolos é pequeno demais para codificar comportamento indecidível
Dito isso, como consequência dos teoremas da incompletude, necessariamente existe algum n para o qual a matemática padrão não consegue provar o valor de BB(n). Nos últimos anos, várias pessoas pesquisaram como encontrar tal n e até onde seria possível reduzi-lo; o recorde atual[0] é 745. Esse recorde provavelmente pode ser reduzido ainda mais, mas ainda assim há uma grande distância entre 5, o maior valor que conhecemos, e 745, o menor valor que sabemos não ser conhecível
[0] Caso você esteja se perguntando o que é “matemática padrão”, este é o recorde atual tanto para ZFC quanto para PA. Então parece que, pelo menos para PA, deveria ser possível reduzir mais. Até agora, parece que não encontraram um método melhor em PA do que em ZFC, mas isso certamente deveria ser possível, não?
“Há apenas quatro dias, mxdys e outro colaborador chamado Racheline descobriram uma barreira aparentemente difícil de superar para BB(6): uma máquina de 6 regras cujo problema da parada se parece com a conjectura de Collatz, um problema matemático famoso por sua dificuldade. A ligação entre máquinas de Turing e a conjectura de Collatz remonta a um artigo de 1993 do matemático Pascal Michel, mas a máquina recém-descoberta, chamada ‘Antihydra’, parece ser a menor máquina que não pode ser resolvida sem um avanço conceitual na matemática.”
Em um projeto pessoal, já escrevi um programa para resolver o problema de corte de estoque (https://en.wikipedia.org/wiki/Cutting_stock_problem)
O estoque incluía cortes de peças nos formatos /---/, /---|, |---|, e eu não podia, ou não queria, usar programas existentes porque não queria desperdiçar material em cortes de 45 graus. Achei interessante a descrição de que Brady, para otimizar a busca por BB(4), podava subárvores de busca em que as diferenças não importavam; isso era bem parecido com o que fiz para deixar meu programa rápido
Segundo um post no blog de Scott Aaronson, há 16.679.880.978.201 máquinas de Turing de 5 estados
Fico curioso se sabemos qual porcentagem delas para. Edit: o número de máquinas de Turing de n estados é (4n + 1)^(2n). Encontrei dados para n pequeno parecidos com a análise que eu queria: https://github.com/LukasKalbertodt/beaver
Não encontrei no site bbchallenge.org, mas todas as máquinas foram classificadas
Em resumo, a prova é bem curta. São 19.000 linhas em Coq, incluindo espaços em branco e comentários
Pela minha experiência, se fosse compilada como um artigo tradicional, provavelmente ficaria muito mais curta do que a versão em Coq. Claro que o tamanho de uma prova não é uma medida de dificuldade ou complexidade, mas pode servir como uma régua bem grosseira
Quando se fala dos limites do conhecimento humano, muitas vezes pensamos em teoremas que são demonstráveis, mas tão complexos que nenhum ser humano consegue entendê-los. Talvez a prova mais complexa que temos seja a classificação dos grupos simples finitos, que chega a milhares, talvez dezenas de milhares de páginas, e é possível que haja pouquíssimas pessoas — ou nenhuma — no planeta que a compreenda por completo
Como diz o artigo, BB(6) pode ser indecidível. Mas também pode ser que exista uma prova com milhões de páginas, fora do alcance da humanidade