- 새 3-state 4-symbol Busy Beaver 챔피언 TM이 발견됐고, 정지 시 ((2 \uparrow^{15} 5) + 14)개의 0이 아닌 심볼을 남기는 것으로 계산됨
- 이 수는 Knuth up-arrow 표기로도 매우 커서, (Ack(n)=n \uparrow^n n)로 정의되는 14번째 Ackermann number를 넘는 (BB(3,4) > Ack(14)) 하한으로 정리됨
- TM의 핵심 동작은 (B(k,n,m) \to B(k,0,g_{k-1}^n(m)))에 가깝게 압축되지만, 이를 보이려면 이중 귀납법이 필요함
- Matthew House의 닫힌형 평가식 (g_k^n(0)=\frac{2 \uparrow^k (n+2)}{2}-2) 덕분에 최종 점수 (\sigma=(2 \uparrow^{15}5)+14)를 정확히 쓸 수 있게 됨
- 이 TM은 Collatz식 나머지 분기 없이도 Ackermann-level 함수를 시뮬레이션하며, 개발 중인 Inductive Proof Validator의 검증 사례로도 쓰임
새 Busy Beaver 챔피언의 규모
- Pavel Kropitz가 새 3-state 4-symbol Busy Beaver 챔피언을 발견함
- 이 TM은 “Ackermann-level” 함수를 계산할 수 있고, 정지 시 테이프에 다음 개수의 0이 아닌 심볼을 남김
- ((2 \uparrow^{15} 5) + 14)
- Knuth up-arrow 표기로도 매우 큰 값이라, 하한은 다음처럼 요약됨
- (BB(3,4) > Ack(14))
- 여기서 (Ack(14))는 (Ack(n)=n \uparrow^n n)로 정의되는 14번째 Ackermann number임
- 알려진 범위에서는 실제 탐색 중 발견된 TM 가운데 Ackermann-level 함수를 시뮬레이션할 수 있는 첫 사례임
TM 정의와 최종 구성
- TM 전이 문자열은 다음과 같음
1RB3LB1RZ2RA_2LC3RB1LC2RA_3RB1LB3LC2RC
- 전이표는 상태
A,B,C와 심볼0,1,2,3에 대해 정의됨A:1RB,3LB,1RZ,2RAB:2LC,3RB,1LC,2RAC:3RB,1LB,3LC,2RC
- 최종 구성은 다음과 같음
- (0^\infty ;; 3^{2 g_{15}^{3}(0) + 1} ;; 2^{16} ;; 1 ;; \text{ Z> } ;; 0^\infty)
- 이 구성에서 점수 (\sigma)가 정확히 계산됨
- (\sigma = 2 g_{15}^{3}(0) + 18 = (2 \uparrow^{15} 5) + 14)
발견과 검증 과정
- Pavel Kropitz는 이 TM을 2024년 4월 25일 Discord에 공유함
- 당시 코드는 사람이 읽을 수 있는 점수 하한을 지정하지 못했고, 결과를
Halt(SuperPowers(13))로 표시함- 이는 증명에 13층의 귀납 규칙이 필요함을 뜻함
- 이후 새 Inductive Proof Validator를 사용한 검증이 시작됨
- 2024년 5월 20일 검증이 완료되면서 (g_k^n(m))의 정확한 정의가 추출됐고, 이를 통해 (\sigma > 2 \uparrow^{15} 3) 하한을 얻음
- Matthew House는 2024년 5월 22일 다음의 단순한 닫힌형 평가식을 발견함
- (g_k^n(0) = \frac{ 2 \uparrow^k (n+2) }{2} - 2)
- 이 평가식으로 (\sigma)의 정확한 값을 표현할 수 있게 됨
동작 분석과 이중 귀납 증명
- 다음 구성을 정의함
- (B(k, n, m) = 0^\infty ;; 3^{2m+1} ;; 2^k ;; \text{ A> } ;; 1^n)
- 초기 구성은 241스텝 뒤 다음 상태에 도달함
- (0^\infty ;; \text{A>} ;; 0^\infty \xrightarrow{241} B(16,3,0);;2;;0^\infty)
- 핵심 규칙은 다음과 같음
- (B(k,n,m) \to B(k,0,g_{k-1}^n(m))), 단 (k \ge 1)
- (g_k)는 다음 재귀식으로 정의됨
- (g_0(m)=m+1)
- (g_{k+1}(m)=g_k^{2m+2}(0))
- 전체 동작은 거의 하나의 규칙으로 압축될 만큼 단순하지만, 이 규칙 자체는 이중 귀납법으로 증명해야 함
- 보조정리와 따름정리는
B상태가3과2^k블록을 처리해1들을 만들어내는 과정을 다룸- (3;;2^k;;\text{<B} \xrightarrow{2k+1} 2^k;;\text{<B};;1)
- (3^m;;2^k;;\text{<B} \xrightarrow{(2k+1)m} 2^k;;\text{<B};;1^m)
- 정리 3은 모든 (k \ge 1, n \ge 0, m \ge 0)에 대해 핵심 규칙이 성립함을 보임
- (k=1) 기본 사례는 (n)에 대한 귀납으로 처리됨
- 귀납 단계는 (k)에 대한 가정과 (n)에 대한 귀납 가정을 함께 사용함
정확한 값 계산
- (g_k)에는 Knuth up-arrow와 산술만 사용하는 비교적 단순한 닫힌형 평가가 있음
- 모든 (k \ge 0, m \ge 0)에 대해 다음이 성립함
- (2 g_{k+1}(m) + 4 = 2 \uparrow^k (2m+4))
- 여기서 (a \uparrow^0 b = ab)로 정의함
- 이 결과는 (k)에 대한 귀납법으로 증명됨
- 기본 사례 (k=0)에서는 (g_1(m)=2m+2)가 됨
- 귀납 단계에서는 ((2 \uparrow^k)^n) 반복 적용을 사용함
- 닫힌형은 (2 \uparrow^k 2 = 4)가 모든 (k)에서 성립하는 우연에 의존함
- 매개변수가 조금 달라져 ((2 \uparrow^k)^{2m+2}5) 형태가 됐다면 닫힌형 표현을 얻기 어려웠을 것으로 봄
- 따름정리로 모든 (k \ge 0, n \ge 0)에 대해 다음이 성립함
- (2 g_k^n(0) + 4 = 2 \uparrow^k (n+2))
- 최종 점수는 바로 다음처럼 도출됨
- (\sigma = 2 g_{15}^{3}(0) + 18 = (2 \uparrow^{15} 5) + 14)
시작 상태를 바꾼 순열 결과
- 시작 상태를
B나C로 바꾸면 더 작은 관련 결과가 나옴- (0^\infty ;; \text{B>} ;; 0^\infty \xrightarrow{86} B(7,3,0);;2;;0^\infty)
- (0^\infty ;; \text{C>} ;; 0^\infty \xrightarrow{20} B(1,3,0);;2;;0^\infty)
- 시작 상태가
B일 때의 점수는 다음과 같음- (\sigma_B = 2 g_6^3(0) + 9 = (2 \uparrow^6 5) + 5)
- 시작 상태가
C일 때는 72스텝에서 정지하며, 점수는 다음과 같음- (\sigma_C = 2 g_0^3(0) + 3 = (2 \uparrow^0 5) - 1 = 9)
B에서 시작하는 첫 순열도 또 다른 상위권 BB(3,4) TM임- 이를 TNF로 변환하면 다음 전이 문자열이 됨
1RB3RB1LC2LA_2LA2RB1LB3RA_3LA1RZ1LC2RA
Collatz식 규칙이 없는 단순성
- 이 TM의 흥미로운 점 중 하나는 예상보다 단순하다는 데 있음
- 값의 나머지에 따라 다르게 동작하는 Collatz-like 규칙이 없음
- Collatz-like TM의 지배가 끝났는지는 아직 알기 너무 이르함
- Ackermann-level Collatz-like TM이 아직 남아 있을 수 있지만, 선택 편향 때문에 바로 보이지 않을 수 있다는 추측이 있음
- 이 TM이 첫 Ackermann-level TM으로 발견된 이유는 Ackermann-level 함수 위에서 modular arithmetic을 구현하지 않아도 정지 증명이 가능할 만큼 단순했기 때문일 수 있음
Inductive Proof Validator
- 이 TM은 개발 중인 Inductive Proof Validator의 테스트 사례로 적합했음
- 프로젝트의 목표는 “귀납 증명”을 위한 표준화된 인증서 형식을 만드는 것임
- 여기서 “귀납 증명”은 전방 추론과 규칙 기반 분석 전반을 가리키는 포괄적 용어로 쓰임
- 누구든 “inductive decider”를 가지고 있으면 해당 규칙을 이 형식으로 작성하고, validator가 그 증명을 검사할 수 있게 하는 방식임
- 시스템은 아직 매우 투박하고 실제 사용 준비가 되지 않았지만, 약간의 수작업을 거쳐 이 TM을 포함한 여러 TM의 동작 증명에 사용됨