오늘은 실무랑은 거리가 좀 있는 소식이에요. 그래도 컴퓨터 과학을 좋아하는 분이라면 설렐 만한 내용이에요. GitHub에 '비지 비버(Busy Beaver)' 관련 분석 문서가 하나 올라왔어요. 내용은 상태가 딱 10개인 튜링 머신이 멈출 때까지 걸리는 시간이 그 유명한 그레이엄 수보다 크다는 거예요. 식으로 쓰면 BB(10) > 그레이엄 수인데요, 무슨 말인가 싶으시죠? 하나씩 풀어볼게요.
비지 비버가 뭐냐면
튜링 머신은 '끝없이 긴 테이프 + 그 위를 오가는 헤드 + 상태표'로 된 가장 단순한 컴퓨터 모델이에요. 헤드는 지금 칸에 적힌 기호(0 또는 1)와 자기 상태를 봐요. 그리고 세 가지를 정하는데요, 칸에 뭘 쓸지, 왼쪽과 오른쪽 중 어디로 갈지, 다음에 어떤 상태가 될지예요.
비지 비버 게임은 이런 질문이에요. 「상태를 n개만 쓸 수 있을 때, 언젠가 멈추는 머신 중에서 가장 오래 일하는 놈은 얼마나 오래 일할까?」 그 최댓값이 BB(n)이에요.
포인트는 '언젠가 멈추는'이에요. 무한 루프는 탈락이거든요. 그런데 어떤 프로그램이 멈출지, 영원히 돌지 판정하는 건 그 유명한 정지 문제예요. 일반적으로는 어떤 알고리즘으로도 풀 수 없죠. 그래서 BB(n)은 계산 불가능한 함수예요. 우리가 떠올릴 수 있는 어떤 계산 가능한 함수보다도 결국엔 더 빨리 커지고요.
실제 값을 보면 감이 와요. 단계 수 기준으로 BB(2)=6, BB(3)=21, BB(4)=107이에요. 그리고 2024년에 bbchallenge라는 온라인 협업 프로젝트가 BB(5)=47,176,870을 증명했어요. Coq이라는 증명 보조기(증명이 맞는지 컴퓨터가 한 줄씩 확인해 주는 도구)로 기계 검증까지 끝냈고요. 4개에서 5개로 늘었을 뿐인데 107이 4,700만이 된 거죠. BB(6)은 아직 몰라요. 알려진 하한만 해도 지수를 탑처럼 쌓은 걸 또 탑으로 쌓는 수준이라 평범한 표기로는 적을 수도 없어요.
그레이엄 수는 또 뭐냐면
그레이엄 수는 '실제 수학 증명에 등장한 엄청나게 큰 수'로 유명해요. 크누스의 화살표 표기로 정의하는데요.
- 3↑3 = 3³ = 27 (거듭제곱)
- 3↑↑3 = 3^(3^3) = 3^27, 약 7.6조 (거듭제곱을 탑처럼 쌓기)
- 3↑↑↑3 = 3을 약 7.6조 층 쌓은 거듭제곱 탑
- g1 = 3↑↑↑↑3, g2는 화살표를 g1개 쓴 수… 이렇게 64번 반복한 g64가 그레이엄 수예요.
저장소에 올라온 머신 읽는 법
파일 이름이 곧 머신이에요. 1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RZ0LC
bbchallenge 커뮤니티의 표준 표기법이에요. 밑줄로 나뉜 덩어리 하나가 상태 하나예요(A부터 J까지 10개). 덩어리마다 3글자짜리 묶음이 두 개 있는데, 앞은 '0을 읽었을 때' 할 일이고 뒤는 '1을 읽었을 때' 할 일이에요. 첫 덩어리 1RB0RA는 이렇게 읽어요. 「A 상태에서 0을 읽으면 1을 쓰고 오른쪽으로 가서 B 상태가 된다. 1을 읽으면 0을 쓰고 오른쪽으로 가서 A 상태를 유지한다.」 마지막 J의 1RZ에 있는 Z가 '정지'예요.
물론 이걸 직접 돌려서 멈추는 걸 볼 수는 없어요. 우주가 끝나도 안 끝나니까요. 그래서 이런 결과는 보통 테이프 위에서 반복되는 패턴부터 찾아요. 그다음 「이 구간 길이가 n이면 다음엔 f(n)이 된다」 같은 점화식으로 머신의 동작을 요약하고, 그 점화식이 화살표 표기급으로 커진다는 걸 보여요. 컴파일된 바이너리를 리버스 엔지니어링해서 원래 알고리즘을 알아내는 작업이랑 비슷하다고 보시면 돼요.
이 결과는 어떤 위치에 있을까
'그레이엄 수를 넘으려면 상태가 몇 개 필요한가'는 큰 수를 연구하는 구골로지 커뮤니티에서 오래된 주제예요. 기존에 알려진 기록들은 10개보다 많은 상태가 필요했는데요, 그걸 10개까지 끌어내렸다는 게 이번 주장의 핵심이에요.
주의할 점도 있어요. BB(5)가 확정으로 인정받은 건 Coq으로 기계 검증을 했기 때문이거든요. 이번 결과는 GitHub 문서 형태의 분석이에요. 그래서 커뮤니티 교차 검증을 거치기 전까지는 '유력한 주장' 정도로 보는 게 맞아요. 요즘 이 분야에서는 사람이 찾은 규칙을 Coq이나 Lean으로 확인하는 흐름이 자리 잡았어요. 이번 결과도 그 길을 밟을 가능성이 커요.
한국 개발자에게 주는 시사점
당장 실무에 쓸 일은 없지만 가져갈 건 있어요.
첫째, '코드가 짧다 = 동작이 단순하다'가 아니라는 극단적인 예시예요. 정적 분석 도구가 「이 루프 언젠가 끝나요?」에 완벽하게 답하지 못하는 것도 같은 이유거든요.
둘째, bbchallenge식 협업 방식이 흥미로워요. 수천만 개의 머신을 자동 판정기(decider)로 먼저 걸러내요. 그리고 남은 어려운 것에만 사람이 붙어요. 대규모 테스트 자동화랑 꽤 닮은 사고방식이죠. 간단한 사이클 판정기 정도는 주말 사이드 프로젝트로 짜보기 딱 좋아요.
셋째, Coq이나 Lean 같은 형식 검증에 관심 있다면 BB 관련 증명은 꽤 괜찮은 입문 소재예요.
마무리
밑줄 빼면 60글자짜리 프로그램이 그레이엄 수보다 오래 돈다. 계산 가능성의 경계가 생각보다 훨씬 가까이 있다는 걸 보여주는 결과예요.
여러분은 어떻게 보세요? 사람이 쓴 분석 문서만으로 이런 결과를 받아들여도 될까요? 아니면 BB(5)처럼 기계 검증까지 마쳐야 '확정'이라고 불러야 할까요?
🔗 출처: Hacker News