- El Busy Beaver Challenge, con la participación de más de 20 personas de todo el mundo, verificó que el número Busy Beaver para máquinas de Turing de 5 reglas es BB(5)=47,176,870
- Quedó confirmado que la máquina hallada en 1989 por Marxen y Buntrock, que se detiene tras 47,176,870 pasos, es realmente la máquina de 5 reglas que se detiene y tarda más en ejecutarse
- El equipo combinó un método genealógico para reducir candidatos duplicados, programas para detectar no detención y el asistente de pruebas Coq para procesar decenas de millones de candidatos
- El resultado final se completó como una prueba en Coq de 40,000 líneas en la que mxdys integró las técnicas de la comunidad, y fue revisada por Yannick Forster, especialista en Coq de Inria
- En BB(6), una máquina de 6 reglas similar a la conjetura de Collatz, Antihydra, apareció como barrera, por lo que BB(5) incluso podría ser el último número Busy Beaver que la humanidad llegue a conocer con exactitud
Se confirma BB(5)
- El equipo de Busy Beaver Challenge verificó que el valor exacto de BB(5) es 47,176,870
- Este valor representa la cantidad máxima de pasos que puede ejecutar una máquina de Turing con 5 reglas antes de detenerse, entre todas las que sí se detienen
- Para la verificación se usó el asistente de pruebas Coq, que certifica que una prueba matemática esté construida sin errores
- Cristopher Moore, del Santa Fe Institute, evaluó que la ingeniería social y matemática de este trabajo fue impresionante
- Damien Woods, de Maynooth University, comparó la velocidad con la que se obtuvo el resultado con “territorio de Usain Bolt”
- Lo clave de BB(5) no está en aplicaciones a otras áreas de la informática, sino en que es un logro obtenido en el límite de lo no computable
El problema Busy Beaver y el problema de la detención
- El problema Busy Beaver no se refiere a lenguajes de programación generales, sino a máquinas de Turing
- Una máquina de Turing lee y escribe 0 y 1 sobre una cinta infinita, mientras su head se mueve una celda a la vez y actúa según una tabla de reglas
- Cada regla especifica la siguiente acción según si el valor leído es 0 o 1
- Cambiar o mantener el valor
- Moverse a la izquierda o a la derecha
- Indicar la siguiente regla que se consultará
- Una regla especial determina cuándo se detendrá la máquina
- El problema de decidir en general si una máquina de Turing eventualmente se detendrá o seguirá ejecutándose para siempre es el problema de la detención
- Alan Turing demostró que no existe una solución general para el problema de la detención
- La caza del Busy Beaver, en vez de resolver en general si todas las máquinas se detienen o no, consiste en clasificar cada máquina dentro de un conjunto finito con un número fijo de reglas
El Busy Beaver game de Radó
- Tibor Radó definió en un artículo de 1962 el Busy Beaver game, agrupando las máquinas de Turing por número de reglas
- En el conjunto de todas las máquinas de Turing con n reglas:
- Algunas máquinas se ejecutan para siempre
- Algunas máquinas se detienen
- Entre las que se detienen, la que más tarda en ejecutarse es el busy beaver
- Su número de pasos de ejecución es BB(n)
- Para determinar BB(n), hay que comprobar el tiempo de ejecución de todas las máquinas que se detienen y demostrar que todas las demás no se detienen
- Medir el tiempo de ejecución normalmente puede hacerse con simulación por computadora, pero demostrar la no detención se parece mucho a resolver el problema de la detención para máquinas concretas
- Shawn Ligocki, colaborador de Busy Beaver Challenge, ve este trabajo como algo que ocurre en “la frontera de lo desconocido”
De BB(1) a BB(4)
- BB(1)=1 se comprueba fácilmente
- Si la primera regla hace que se detenga al leer 0, se detiene en el primer paso
- En cualquier otro caso, sigue moviéndose sobre una cinta llena de 0
- Con solo 2 reglas ya aparecen más de 6,000 máquinas de Turing distintas; con 3 reglas, varios millones; y con 4 reglas, decenas de miles de millones
- Allen Brady integró en un programa un método genealógico que reduce duplicados agrupando máquinas con comportamiento inicial similar
- Shen Lin, junto con Radó, demostró BB(3)=21, y el resultado se publicó en 1965
- Brady descubrió en 1966 una máquina de 4 reglas que se detenía tras 107 pasos, y en 1974 demostró que ese valor era BB(4)
- BB(4) fue durante más de 40 años el último número Busy Beaver conocido por la humanidad
La caza del quinto Busy Beaver
- La competencia de Dortmund de 1984 fue la primera cacería a gran escala de BB(5)
- Existen casi 1.7 billones de máquinas de Turing de 5 reglas, y aun enumerándolas a razón de una por milisegundo tomaría más de 500 años
- La máquina más ocupada encontrada por los participantes de Dortmund se detenía tras más de 100,000 pasos
- Después, otro investigador halló una máquina que se ejecutaba por más de 2 millones de pasos
- Heiner Marxen y Jürgen Buntrock desarrollaron técnicas matemáticas para acelerar la simulación de máquinas de Turing
- En 1989, Marxen ejecutó su programa durante un fin de semana en una nueva y potente computadora de la empresa y encontró una máquina que se detenía tras 47,176,870 pasos
- Buntrock reprodujo el resultado, y ambos publicaron un artículo a comienzos de 1990
- Esa máquina sí era en realidad el quinto Busy Beaver, pero demostrar que todas las máquinas restantes no se detenían tomó más de 30 años adicionales
Skelet y las máquinas no resueltas
- A inicios de los años 2000, el informático búlgaro Georgi Ivanov Georgiev se acercó muchísimo a BB(5)
- Georgiev pasó dos años dedicando varias horas al día a mejorar un programa para identificar máquinas que no se detienen
- El programa final tenía 6,000 líneas de código denso sin comentarios, y tardaba más de una semana en ejecutarse
- Ese programa dejó unas 100 máquinas de Turing sin resolver, y Georgiev las redujo manualmente a 43
- Georgiev publicó los resultados en línea en 2003 bajo el seudónimo Skelet
- Estas 43 máquinas difíciles pasaron a llamarse máquinas Skelet, en referencia a su seudónimo
- Georgiev dijo que, tras dos años de trabajo intenso, quedó demasiado agotado como para seguir produciendo ideas nuevas
La estructura colaborativa de Busy Beaver Challenge
- Tristan Stérin inició el Busy Beaver Challenge en 2022
- El proyecto se desarrolló como colaboración en línea y creció hasta convertirse en una comunidad internacional de más de 20 personas, incluyendo muchos colaboradores sin credenciales académicas tradicionales
- Stérin consideraba que, para confirmar BB(5), hacía falta una prueba documentada y reproducible
- El programa de Georgiev era sofisticado, pero difícil de revisar para otros investigadores
- Stérin dividió el trabajo basándose en enfoques previos
- Eliminar máquinas duplicadas con el método genealógico de Brady
- Identificar las máquinas que se detienen dentro de 47,176,870 pasos
- Tratar las máquinas que corren para siempre con programas independientes que contienen distintos métodos de prueba
- Un programa de primera etapa escrito a fines de 2021 generó una lista de cerca de 120 millones de máquinas de Turing suficiente para decidir BB(5)
- Aproximadamente una cuarta parte se detenía antes que la máquina de Marxen y Buntrock, y 88 millones siguieron en revisión
- Stérin también construyó una interfaz en línea con diagramas espacio-tiempo que muestran el comportamiento de las máquinas como una cuadrícula bidimensional de 0 y 1
Lenguaje de cinta cerrada y aceleración de la colaboración
- Shawn Ligocki se unió al Busy Beaver Challenge en 2022 y revivió el método de lenguaje de cinta cerrada creado por Marxen
- Este método ofrece un marco matemático unificado para mostrar, a partir de patrones en la cinta de una máquina de Turing, que la máquina no se detiene
- Ligocki escribió una entrada de blog presentando la técnica, pero no sabía cómo escribir un programa que cubriera todos los casos
- Justin Blanchard la implementó después de sumarse al proyecto, y otros dos colaboradores aumentaron mucho la velocidad de ejecución
- En pocos meses, el método de lenguaje de cinta cerrada se volvió una de las herramientas más potentes del equipo
- La técnica también pudo resolver 10 de las 43 máquinas Skelet que había dejado Georgiev
- Ligocki cree que ese resultado no habría surgido del aporte de una sola persona
Skelet #1, Skelet #17 y Coq
- Skelet #1 era una máquina que alternaba entre fases predecibles y fases caóticas
- En marzo de 2023, Ligocki y Pavel Kropitz reforzaron una técnica de simulación acelerada de Marxen y Buntrock de hace 30 años para analizar Skelet #1
- Skelet #1 solo entraba en un ciclo repetitivo después de superar un billón por un billón de pasos, y ese ciclo repetitivo duraba más de 8 mil millones de pasos
- mei, programador autodidacta de 21 años, aprendió Coq y luego tradujo a Coq varias pruebas del Busy Beaver Challenge
- mei también llevó a Coq la prueba de no detención de Skelet #1 de Ligocki y Kropitz, reforzando así la solidez de ese resultado
- Skelet #17 era otra máquina difícil en la que Chris Xu logró un avance decisivo
- La prueba de Xu fue sobresaliente, pero incluía intuiciones matemáticas difíciles de trasladar al formato preciso que exige Coq
- El equipo no quería pruebas del tipo “ejecuta el programa durante 6 meses”, sino pruebas razonablemente reproducibles
Una prueba en Coq de 40,000 líneas
- En abril de 2024, un nuevo colaborador conocido solo por el seudónimo mxdys se unió al trabajo para completar la prueba en Coq
- Ni siquiera el equipo conoce la ubicación o antecedentes personales de mxdys
- El 10 de mayo, mxdys publicó en Discord: “The Coq proof of BB(5) is finished.”
- En cuestión de semanas, mxdys integró las técnicas y resultados de la comunidad y completó una sola prueba en Coq de 40,000 líneas
- La prueba se publicó en el repositorio Coq-BB5
- Yannick Forster, especialista en Coq de Inria, revisó la prueba y comentó que no fue algo fácil de formalizar
- Como resultado, quedó confirmado que la máquina de 47,176,870 pasos encontrada hace más de 30 años por Marxen y Buntrock es realmente el quinto Busy Beaver
- Georgiev dijo que no esperaba que este problema se resolviera en vida suya
- Allen Brady falleció a los 90 años el 21 de abril de 2024, un mes antes de que se completara la prueba
BB(6) y la siguiente frontera
- Los colaboradores del Busy Beaver Challenge comenzaron a preparar un artículo académico oficial que explique el resultado
- El artículo complementará la prueba en Coq de mxdys con una demostración legible para humanos
- Algunos miembros del equipo ya pasaron al siguiente Busy Beaver
- mxdys y Racheline encontraron en BB(6) una barrera que parece muy difícil de superar
- Esta barrera es una máquina de 6 reglas cuyo problema de detención se parece a la conjetura de Collatz
- La máquina se llama Antihydra
- La conexión entre máquinas de Turing y la conjetura de Collatz se remonta a un artículo de Pascal Michel de 1993, pero Antihydra parece ser la máquina más pequeña que no puede resolverse sin un avance conceptual en matemáticas
- Scott Aaronson cree que BB(5) podría ser el último número Busy Beaver que la humanidad llegue a conocer
- Algunos colaboradores planean seguir trabajando en variantes del problema Busy Beaver, pero no todos los participantes seguirán en la misma dirección
- Stérin dijo que Busy Beaver Challenge le confirmó la efectividad de la investigación colaborativa en línea, y quiere desarrollar herramientas de software que ayuden a proyectos colaborativos en otras áreas de las matemáticas
1 comentarios
Comentarios de Hacker News
Hay un comentario de Scott Aaronson sobre este resultado: https://scottaaronson.blog/?p=8088
Y también hay grandes hilos de principios de este año sobre los “leisure-class beavers”:
https://news.ycombinator.com/item?id=40453221
https://news.ycombinator.com/item?id=38113792
https://news.ycombinator.com/item?id=37910297
El problema del castor ocupado original tiene muchas variantes, y una de ellas es el castor ocupado funcional definido mediante cálculo lambda [1]
Como mide el tamaño del programa en bits, no la cantidad de estados, se pueden determinar más valores; hasta ahora solo se conocen 6 para máquinas de Turing, mientras que en esta variante ya se llegó hasta 37. La brecha entre el mayor valor conocido y un valor que supera el número de Graham es de apenas 13 bits de programa. Una variante estrechamente relacionada [2] puede expresarse directamente mediante complejidad de Kolmogorov, y Mikhail Andreev [3] considera que esto es importante para aplicaciones en teoría de la información
[1] https://oeis.org/A333479
[2] https://oeis.org/A361211
[3] https://arxiv.org/pdf/1703.05170
Encontré https://oeis.org/A141475, pero ahí para 5 aparece 27 billones
Recuerdo haber visto un video que explicaba esa definición
Trabajé durante varios años con un ingeniero increíblemente inteligente, hasta el punto de ser difícil de comprender, que ascendió más rápido en niveles de IC que cualquiera que haya visto en una empresa tecnológica de élite
Se fue hace unos años, y cuando le pregunté cuáles eran sus planes me dijo que iba a investigar el problema del castor ocupado. Me pregunto si el colaborador anónimo mxdys, que terminó la prueba formal de BB(5) en el artículo, será esa persona, pero probablemente nunca lo sepa
No sé cuál es la recompensa, y si se trata de una mente tan brillante, me gustaría que resolviera problemas más relacionados con mejorar el mundo
El artículo original de Tibor Radó sobre el castor ocupado, “On Non-Computable Functions”, en realidad es bastante fácil y entretenido de leer
Aquí hay una versión moderna con notas adicionales: https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
Lo llamativo aquí es que la demostración es una prueba en Coq
Me pregunto si es la primera demostración importante implementada desde el inicio en un asistente de teoremas, en vez de trasladar a un asistente una prueba ya conocida. Antes hubo demostraciones asistidas por computadora, pero el teorema de los cuatro colores o la conjetura de Kepler recién se trasladaron después a entornos de verificación formal
El problema principal era que los decisores y las pruebas manuales no estaban ordenados y resultaban algo sospechosos. En particular, Skelet #1 necesitó un programa específico para acelerar hasta el patrón final [0], y para Skelet #17 Xu tuvo que usar un razonamiento denso de 7 páginas para demostrar que no se detiene [1]. La prueba completa en Coq aporta exactamente la confianza que estos resultados necesitaban
[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
Puede que no haya entendido exactamente qué significa “entorno de verificación formal”, pero tengo entendido que el teorema de los cuatro colores fue demostrado por computadora desde el principio. El intento de demostración original de Kempe tenía fallas, pero proporcionó algunas de las herramientas básicas usadas en demostraciones posteriores, y al final parece que el teorema fue demostrado por computadora
Este castor ocupado fue descubierto en 1990, y es muy probable que todas las máquinas de tamaño 5 también se hayan enumerado poco después
Felicitaciones al equipo. Con esto, queda resuelto el problema de la detención para programas de máquinas de Turing de 5 estados y 2 símbolos con cinta en blanco como referencia
Me pregunto si alguien ha intentado aplicar la misma técnica al caso de 2 estados y 4 símbolos. En general, los símbolos son más potentes que los estados, pero con ese tamaño quizá sea manejable y podría haber resultados inesperados. Tanto 6 estados y 2 símbolos como 2 estados y 5 símbolos parecen difíciles de abordar, y quizá incluso demostrablemente difíciles. Por cierto, existe esa idea absurda pero extrañamente difundida de que los humanos pueden intuir la respuesta al problema de la detención con algo como el ojo de la mente o la mecánica cuántica en el cerebro; por supuesto, nada de eso intervino en esta demostración
Según entiendo, los decisores que se usan actualmente ya bastan para demostrar que todos los casos restantes de 2×4 no se detienen. Por lo tanto, si no hay un error grande en el diseño de los decisores, del campeón actual se obtiene Σ(2,4) = 2,050, S(2,4) = 3,932,964. Simplemente los resultados no están reunidos en un solo lugar
En 2×5 está Hydra y en 6×2 está Antihydra; ambas calculan la misma iteración, solo cambian el punto de partida y la condición de detención. La conjetura estándar, relacionada con el problema 3/2 de Mahler, es que esta iteración está uniformemente distribuida mod 2; si se demostrara esa conjetura, se obtendrían cotas superiores e inferiores para la proporción acumulada de 0 y 1, lo que probaría casi con certeza que ambas máquinas no se detienen. Por supuesto, no se conoce ningún método de demostración
Se usó un generador de demostraciones basado en una teoría lógica llamada Aleph*, y para entonces ya se sabía desde hacía 1,500 años que ZFC no podía establecer BB(18). Comparado con 2024, ningún programa anterior al uso de Aleph* podía, ni siquiera en teoría, usarse para una verificación de demostraciones por fuerza bruta destinada a resolver BB(18). Contrasta con el hecho de que hoy podemos enumerar y verificar demostraciones en ZFC y, en teoría, resolver BB(??)
La postura de que “los humanos intuyen la respuesta al problema de la detención” significa algo así. Hasta donde sé, no hay una razón teórica fuerte por la que esta historia futura sea imposible. Y como Busy Beaver no es computable, para crear el programa necesario los humanos tuvieron que desarrollar una nueva teoría. El mérito del resultado tiene que atribuirse a algo, y como el programa de entonces no existía, no puede atribuirse al cómputo
Me pregunto si, por casualidad, todos los programas no detenidos de longitud 5 resultaron ser demostrablemente no detenidos
“El hecho de que Σ(5) = 1,915 y S(5) = 2,358,064 nunca será demostrado. O, si se descubre una cota inferior mayor, se puede sustituir ese nuevo valor en esta predicción.”
La razón era que probablemente la naturaleza había sembrado entre las máquinas pendientes de 5 estados al menos un problema tan escurridizo como la conjetura de Goldbach. Dicho de otro modo, probablemente existía un patrón recursivo de no detención más allá de nuestra capacidad de reconocerlo. Por suerte esta predicción no se hizo realidad, pero fue cuestión de un estado extra
[0] Allen Brady, "The Busy Beaver Game and the Meaning of Life", en Rolf Herken (ed.), The Universal Turing Machine: A Half-Century Survey, Oxford University Press, 1988, pp. 259–277. Este capítulo también puede encontrarse en la 2.ª ed., Springer, 1995, pp. 237–254.
Si es en el sentido práctico, otras personas ya respondieron. Si es en el sentido matemático, me habría parecido bastante sorprendente que BB(5) fuera indecidible. 5 estados y 2 símbolos es demasiado pequeño para codificar comportamiento indecidible
Sin embargo, como consecuencia de los teoremas de incompletitud, necesariamente existe algún n para el cual la matemática estándar no puede demostrar el valor de BB(n). En los últimos años varias personas han investigado qué tan bajo puede llevarse ese n, y el récord actual[0] es 745. Probablemente ese récord pueda bajarse más, pero aun así hay mucha distancia entre el valor más alto que conocemos, 5, y el valor más bajo que sabemos que no se puede conocer, 745
[0] Por si te preguntas qué es “matemática estándar”, este es el récord actual tanto para ZFC como para PA. Así que, al menos para PA, debería ser posible bajarlo más. Hasta ahora parece que no se ha encontrado un método mejor para PA que para ZFC, pero ¿no debería ser posible, obviamente?
“Hace apenas cuatro días, mxdys y otra colaboradora llamada Racheline encontraron una barrera que parece difícil de superar para BB(6): una máquina de 6 reglas cuyo problema de detención se parece a la conjetura de Collatz, un problema matemático famoso por ser difícil de abordar. La conexión entre las máquinas de Turing y la conjetura de Collatz se remonta a un artículo de 1993 del matemático Pascal Michel, pero la máquina recién descubierta, llamada ‘Antihydra’, parece ser la máquina más pequeña que no puede resolverse sin un avance conceptual en matemáticas.”
Como proyecto personal, una vez escribí un programa para resolver el problema de corte de stock (https://en.wikipedia.org/wiki/Cutting_stock_problem)
El inventario incluía cortes de piezas con formas /---/, /---|, |---|, y no podía o no quería usar programas existentes porque no quería desperdiciar material en cortes de 45 grados. Me pareció interesante que la descripción de cómo Brady recortó subárboles de búsqueda donde las diferencias no importaban para optimizar la búsqueda de BB(4) se parece bastante a lo que hice para hacer rápido mi programa
Según una entrada del blog de Scott Aaronson, hay 16,679,880,978,201 máquinas de Turing de 5 estados
Me pregunto si se sabe qué porcentaje de ellas se detiene. Edición: el número de máquinas de Turing de n estados es (4n + 1)^(2n). Encontré datos para n pequeños similares al análisis que me interesaba: https://github.com/LukasKalbertodt/beaver
No la encontré en el sitio bbchallenge.org, pero todas las máquinas están clasificadas
En conjunto, la demostración es bastante corta. Son 19.000 líneas de Coq, incluyendo espacios en blanco y comentarios.
Por mi experiencia, si se compilara como un artículo tradicional, creo que quedaría mucho más corta que la versión en Coq. Claro que la longitud de una demostración no es una medida de su dificultad ni de su complejidad, pero puede servir como un criterio muy aproximado.
Cuando se habla de los límites del conocimiento humano, a menudo pensamos en teoremas que son demostrables, pero tan complejos que ningún ser humano podría entenderlos. Probablemente la demostración más compleja que tenemos sea la clasificación de los grupos simples finitos: tiene miles o decenas de miles de páginas, y es posible que haya muy pocas personas en el mundo, o ninguna, que la entienda por completo.
Como dice el artículo, BB(6) podría ser indecidible. Pero también existe la posibilidad de que haya una demostración de millones de páginas y quede fuera del alcance de la humanidad.