💻 computer science

Determination of the fifth Busy Beaver value

이 논문은 1962 년 이후 40 년 만에 새로운 비시 베버 값이 결정되었으며, 1 억 8 천만 개 이상의 튜링 머신을 Coq 증명 보조기를 통해 분석하여 5 상태 비시 베버 값 $S(5)$ 가 47,176,870 임을 최초로 공식적으로 증명했습니다.

원저자: The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Sha

게시일 2026-03-24

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Naściszewski, savask, Tristan Stérin, Chris Xu, Jason Yuen, Théo Zimmermann

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

"바쁜 비버" 게임의 5 단계 미스터리를 해결하다: 40 년 만의 대업

이 논문은 수학계에서 가장 난해한 퍼즐 중 하나인 '바쁜 비버 (Busy Beaver)' 게임의 5 단계 문제를 40 년 만에 해결한 놀라운 성과를 담고 있습니다. 이 복잡한 내용을 일상적인 언어와 비유로 쉽게 풀어보겠습니다.

1. 바쁜 비버 게임이란 무엇인가요?

상상해 보세요. 거대한 종이 (테이프) 가 있고, 그 위를 오가는 작은 로봇 (컴퓨터) 이 있습니다. 이 로봇은 **5 개의 상태 (A, B, C, D, E)**만 가질 수 있고, 종이에 '0'과 '1'만 쓸 수 있습니다.

게임 규칙: 로봇은 처음에 모든 종이 칸이 '0'으로 채워진 상태에서 시작합니다. 로봇은 정해진 규칙에 따라 종이에 '1'을 쓰거나 지우며 이동합니다.
목표: 로봇이 멈추기 (정지) 전까지 종이에 '1'을 가장 많이 남긴 로봇이 이깁니다.
S(n) 의 의미: 여기서 'S(n)'은 n 개의 상태를 가진 로봇이 멈추기 전까지 얼마나 많은 걸음 (단계) 을 뗄 수 있는지를 의미합니다.

핵심 문제: "5 개의 상태를 가진 로봇 중, 멈추기 전까지 가장 오랫동안 움직일 수 있는 로봇은 정확히 몇 걸음을 걸을까?"

과거에는 1, 2, 3, 4 단계까지는 답을 알았지만, 5 단계는 1989 년 이후 30 년 넘게 답을 모르고 있었습니다. 1989 년에 한 로봇이 47,176,870 걸음을 걸은 기록이 있었지만, "이게 정말 최장 기록일까? 아니면 더 오래 걸을 로봇이 숨어있을까?"를 증명하지 못했던 것입니다.

2. 이 논문이 한 일: "전체 목록을 다 찾아냈다!"

이 연구팀은 18 억 1,385 만 7,899 개의 가능한 5 단계 로봇을 모두 조사했습니다. (이건 마치 우주에 있는 모든 모래알을 세는 것과 비슷합니다!)

그들은 각 로봇이 멈추는지, 아니면 영원히 돌아다니는지 (무한 루프) 를 판별해야 했습니다.

멈추는 로봇: 몇 걸음 만에 멈추는지 세어 기록했습니다.
멈추지 않는 로봇: "이 로봇은 영원히 멈추지 않는다"는 것을 수학적으로 증명해야 했습니다.

결과: 1989 년의 기록인 47,176,870 걸음이 정말로 최장 기록임을 증명했습니다. 즉, 5 단계 로봇이 멈추기 전까지 걸을 수 있는 최대 걸음수는 정확히 47,176,870입니다.

3. 어떻게 해결했나요? "수학의 마법사 (Coq)"와 "대규모 협업"

이 문제는 사람이 손으로 계산할 수 없을 정도로 복잡했습니다. 그래서 두 가지 강력한 무기를 사용했습니다.

A. "수학의 마법사" (Coq 증명 보조 도구)

사람이 실수할 수 있으므로, 컴퓨터가 수학적 증명을 직접 검증하는 **'Coq'**라는 도구를 사용했습니다.

비유: 수백만 페이지의 복잡한 수학 논문을 사람이 읽으면 실수할 수 있지만, Coq 는 "이 논리 단계가 100% 맞습니다"라고 딱 잘라 말해줍니다.
이 논문은 Coq 가 직접 18 억 개의 로봇을 시뮬레이션하고, 멈추지 않는 로봇들에 대해 "이건 영원히 멈추지 않아"라고 증명하는 코드를 실행했습니다. 이는 수학 역사상 가장 계산량이 많은 공식 증명 중 하나입니다.

B. "온라인 마을의 협업" (bbchallenge.org)

이 작업은 한 두 명의 천재가 혼자 한 것이 아닙니다. 전 세계 수백 명의 아마추어와 전문가가 온라인 커뮤니티 (디스코드, 위키 등) 에서 함께 참여했습니다.

비유: 마치 전 세계의 개발자들이 모여 거대한 오픈소스 소프트웨어를 만드는 것처럼, 각자 다른 아이디어 (로봇이 멈추는지 판단하는 '해결사' 알고리즘) 를 만들어 공유하고 다듬었습니다.
이 과정에서 발견된 13 개의 아주 특별한 로봇 (Sporadic Machines) 은 일반적인 방법으로 해결되지 않아, 각자 개별적인 수학적 증명 (마치 미스터리 소설의 결말을 풀듯이) 이 필요했습니다.

4. 발견된 흥미로운 로봇들 (야생의 알고리즘)

연구팀은 로봇들을 관찰하며 마치 동물을 분류하듯 '동물원 (Zoology)'을 만들었습니다.

순환 로봇 (Cyclers): 같은 패턴을 반복하며 빙글빙글 도는 로봇.
이동 로봇 (Translated Cyclers): 패턴을 반복하되, 종이 위를 한 방향으로 미끄러지듯 이동하는 로봇.
카운터 로봇 (Counters): 종이에 숫자를 세는 로봇.
프랙탈 로봇 (Fractals): 종이에 눈송이나 나뭇가지처럼 복잡한 무늬를 그리는 로봇.
특이한 로봇들: 50 조 년이 넘는 시간을 보낸 후 갑자기 패턴이 반복되기 시작하는 로봇이나, 피보나치 수열을 두 개 동시에 계산하는 로봇 등 인간이 설계하지 않은 기발한 알고리즘들이 발견되었습니다.

5. 왜 이 일이 중요한가요?

40 년 만의 돌파구: 1983 년 이후 40 년 넘게 해결되지 않았던 난제를 풀었습니다.
수학의 한계 확인: 이 연구는 "5 단계 로봇은 우리가 풀 수 있지만, 6 단계 로봇은 골드바흐의 추측 (수학의 난제) 을 푸는 것과 비슷하게 어렵거나, 아예 수학적으로 증명할 수 없는 영역일 수 있다"는 것을 보여줍니다.
협업의 승리: 수학과 컴퓨터 과학이 어떻게 대중과 함께 발전할 수 있는지 보여주는 완벽한 사례입니다.

요약

이 논문은 **"5 단계 바쁜 비버 게임의 우승자는 47,176,870 걸음을 걸은 로봇이며, 이는 전 세계 수백 명의 사람들이 온라인에서 협력하고, 최첨단 컴퓨터 증명 도구 (Coq) 를 이용해 18 억 개의 경우의 수를 모두 확인함으로써 증명되었다"**는 이야기입니다.

이는 단순히 숫자를 맞춘 것이 아니라, 인간과 기계, 그리고 전 세계 커뮤니티가 함께 복잡한 미스터리를 해결할 수 있다는 희망을 보여주는 역사적인 사건입니다.

1. 문제 정의 (The Problem)

비지 베버 함수 $S(n)$ : $n$ 개의 상태를 가진 2 심볼 튜링 기계가 빈 테이프 (모든 0) 에서 시작하여 정지할 때까지 수행할 수 있는 최대 단계 수를 의미합니다.
비계산성: $S(n)$ 은 비계산 함수 (uncomputable function) 로 알려져 있어, 모든 $n$ 에 대한 값을 계산하는 알고리즘은 존재하지 않습니다.
역사적 배경: $S(1)$ 부터 $S(4)$ 까지는 이미 알려져 있었으나, $S(5)$ 의 정확한 값은 1989 년 Heiner Marxen 과 Jürgen Buntrock 이 47,176,870 단계를 기록하는 기계를 발견한 이후로, 그것이 최댓값인지 여부가 30 년 이상 불확실한 상태였습니다.
목표: 5 상태 튜링 기계 중 정지하는 기계의 최대 단계 수를 증명하고, $S(5) = 47,176,870$ 임을 입증하는 것.

2. 방법론 (Methodology)

이 연구는 대규모 협업과 형식적 증명 (Formal Verification) 을 결합한 독특한 접근 방식을 사용했습니다.

A. 형식적 증명 도구: Coq

Coq-BB5: 모든 증명은 Coq 증명 보조기 (Proof Assistant) 를 사용하여 수행되었습니다. 이는 인간의 실수를 배제하고 논리적 오류가 없음을 보장합니다.
반사 (Reflection) 증명: Coq 내부에서 알고리즘을 직접 실행하여 그 결과를 증명에 활용하는 방식을 취했습니다. 즉, Coq 이 1 억 8 천만 개 이상의 튜링 기계를 직접 생성하고 시뮬레이션/분석하여 결과를 도출했습니다.

B. 탐색 공간 축소: Tree Normal Form (TNF)

문제: 5 상태 2 심볼 튜링 기계의 이론적 조합 수는 약 16.7 조 ( $1.67 \times 10^{13}$ ) 개로, 모든 기계를 분석하는 것은 불가능합니다.
해결: Brady 가 제안한 TNF(Tree Normal Form) 기법을 적용하여 검색 공간을 181,385,789 개로 축소했습니다.
- 도달 불가능한 전이 (unreachable transitions) 제거.
- 상태 및 심볼의 순열 (permutation) 중복 제거.
- 대칭성 (좌우 이동 등) 제거.

C. 결정기 (Deciders) 파이프라인

모든 181,385,789 개의 기계는 정지 여부를 판단하기 위해 일련의 자동화된 "결정기 (Deciders)" 파이프라인을 통과했습니다.

루프 감지 (Loops): 기계가 유한한 시간 내에 동일한 구성 (또는 공간 이동된 구성) 으로 반복되는지 감지하여 무한 루프를 판별합니다. (약 95% 의 비정지 기계 해결)
n-gram Closed Position Set (NGramCPS): 테이프의 국소적 구성을 n-gram 으로 모델링하여 닫힌 집합을 형성하고, 정지 전이가 도달할 수 없음을 증명합니다. (약 99.89% 의 비정지 기계 해결)
반복 단어 목록 (RepWL): 테이프 상의 반복되는 패턴을 정규식 (Regular Expression) 으로 추상화하여 비정지성을 증명합니다.
유한 자동화 축소 (FAR) 및 가중치 FAR (WFAR): 튜링 기계의 구성을 유한 상태 자동기 (NFA) 나 가중치 자동기로 축소하여 정지하지 않음을 증명합니다. 이는 Coq-BB5 에서 검증기로 (Verifier) 사용되었습니다.
긴 정지 기계 (Long Halters): 정지하는 기계는 최대 47,176,870 단계까지 시뮬레이션하여 정지 시점을 확인합니다.

D. 희귀 기계 (Sporadic Machines) 처리

자동화된 결정기로 해결되지 않은 13 개의 기계는 개별적인 수학적 증명이 필요했습니다. 이들은 "Sporadic Machines"로 불리며, Coq 에서 수동으로 작성된 증명을 통해 처리되었습니다.

대표적 예시:
- Skelet #1: $5.41 \times 10^{51}$ 단계의 혼돈 기간 후 무한 루프에 들어가는 기계.
- Skelet #10: 피보나치 수열을 기반으로 하는 이중 카운터.
- Skelet #17: 그레이 코드 (Gray code) 와 관련된 복잡한 변환을 수행하는 기계 (최종적으로 해결된 마지막 기계).

3. 주요 기여 및 결과 (Key Contributions & Results)

A. $S(5)$ 값의 결정

결과: $S(5) = 47,176,870$ 임이 증명되었습니다.
증명 범위: 181,385,789 개의 5 상태 튜링 기계 중 175,373,810 개는 자동화된 결정기로, 13 개는 개별 증명으로, 나머지 6,000 여 개는 다른 방법으로 모두 비정지 (Non-halting) 임이 확인되었습니다.
최대 기록: Marxen 과 Buntrock 이 발견한 기계가 실제로 5 상태 Busy Beaver 의 우승자임을 확인했습니다.

B. 추가적인 Busy Beaver 값 증명

$\Sigma(5)$ : 5 상태 기계가 정지 시 테이프에 남기는 1 의 최대 개수는 4,098임을 증명했습니다.
$S(2, 4)$ : 2 상태 4 심볼 기계의 최대 단계 수인 3,932,964를 Coq 으로 증명했습니다.
$S(4)$ 재확인: 기존 Brady 의 $S(4)=107$ 결과를 Coq 을 통해 다시 한번 검증했습니다.

C. 데이터 및 도구 공개

Coq-BB5: 전체 증명 코드는 GitHub 에서 공개되었습니다.
기계 목록: 모든 181,385,789 개의 기계와 그 정지 상태, 사용된 결정기 정보가 추출되어 공개되었습니다.
bbchallenge.org: 이 연구는 온라인 협업 플랫폼 bbchallenge.org 를 통해 수백 명의 기여자 (대부분 비학계 소프트웨어 엔지니어 및 학생) 가 참여하여 이루어졌습니다.

4. 의의 및 영향 (Significance)

수학적 검증의 새로운 표준: Busy Beaver 문제처럼 계산량이 방대하고 복잡한 문제를 형식적 증명 도구 (Coq) 로 완전히 해결한 첫 사례입니다. 이는 컴퓨터 보조 증명의 신뢰성을 극대화했습니다.
협업 연구의 모델: 수백 명의 비전문가와 전문가가 Discord 와 위키를 통해 실시간으로 소통하며 알고리즘을 개발하고 검증하는 "대규모 온라인 협업 (Massively Collaborative Online Research)"의 성공적인 사례를 보여주었습니다.
수학적 난제와의 연결:
- $S(5)$ 는 해결되었지만, $S(6)$ 이상의 값은 골드바흐 추측이나 리만 가설 같은 난제와 동급의 난이도를 가질 수 있음이 지적되었습니다.
- 6 상태 기계 중에는 "Cryptids(기생수)"라고 불리는, 정지 여부가 수학적으로 매우 어렵거나 증명 불가능할 것으로 보이는 기계들이 존재함이 확인되었습니다.
인공지능 및 자동화: 이 연구는 기계 지능 (AI) 이 복잡한 수학적 추론을 수행할 수 있는지에 대한 벤치마크로 활용될 수 있습니다. 실제로 Coq-BB5 의 일부 명제는 AI 시스템으로 테스트되었습니다.

결론

이 논문은 단순히 $S(5)$ 의 숫자를 밝힌 것을 넘어, 형식적 증명 도구, 대규모 협업, 그리고 자동화된 알고리즘을 결합하여 수학의 가장 어려운 미해결 문제 중 하나를 해결한 방법론적 혁신을 보여줍니다. 이는 컴퓨터 과학과 수학의 경계를 허물고, 복잡한 계산 문제의 해결에 새로운 패러다임을 제시합니다.