컴퓨팅의 한계에 도전한 다섯 번째 바쁜 비버 찾기

Amateur Mathematicians Find Fifth ‘Busy Beaver’ Turing Machine | Quanta Magazine

Amateur Mathematicians Find Fifth ‘Busy Beaver’ Turing Machine | Quanta Magazine

단순한 프로그램이 얼마나 복잡해질 수 있는지, 이제 연구자들이 그 비밀에 다가섰습니다.

 

약 40년 전, 독일 서부 도시 도르트문트에 수많은 컴퓨터 과학자들이 모였습니다. 그들이 추적 중이던 목표는 다소 특별했습니다. ‘바쁜 비버’라고 불리는 존재를 찾아내려 했지만, 그동안 단 네 마리만 포획됐을 만큼 흔치 않은 존재였습니다. 100명 이상의 참가자가 이 희귀한 비버를 찾기 위해 특이한 생명체들을 가져왔지만 결국 다섯 번째 비버는 그들의 손에 잡히지 않았습니다.

 

물론 이들 ‘바쁜 비버’는 실제 동물이 아닙니다. 이는 겉보기엔 단순해 보이지만 예상외로 긴 시간을 소모하며 실행되는 컴퓨터 프로그램을 의미합니다. 바쁜 비버를 찾는 여정은 수학의 대표적인 미해결 문제들과 연관되어 있으며, 컴퓨터 과학의 역사를 뒤흔든 한 ‘해결 불가능한 문제’와도 깊은 뿌리를 공유하고 있습니다. 그렇기에 이 도전은 수학자와 프로그래머에게 매력적인 목표로 자리 잡게 되었습니다. 당시 도르트문트에 모인 참가자들 중 세 명은 이후 보고서에서 이렇게 표현했습니다. “우리는 수학적 법칙과의 전쟁에서 승리할 수 없음을 알지만, 그 전투만큼은 승리하고 싶다.”

 

약 40년이 지난 후, 도르트문트 대회의 정신적 후속작이 시작되었습니다. 그 시발점은 바로 대학원생 트리스탄 스테린이 개설한 ‘바쁜 비버 챌린지’ 웹사이트였습니다. 이번에는 경쟁이 아닌 협력을 모토로 하여 누구나 이 도전에 참여할 수 있게 했습니다. 시간이 흐르며, 전통적인 학문적 배경이 없는 사람들을 포함해 전 세계에서 20명 이상의 기여자가 이 온라인 커뮤니티에 참여하게 되었습니다.

 

오늘, 연구팀은 마침내 승리를 선언했습니다. 그들은 다섯 번째 바쁜 비버가 얼마나 ‘바쁜지’를 수치로 나타내는 ‘BB(5)’의 정확한 값을 검증했습니다. 그 값은 47,176,870입니다. 이 결과를 얻기 위해 연구팀은 ‘Coq 증명 보조 프로그램’을 사용했는데, 이는 수학적 증명을 오류 없이 검증해주는 소프트웨어입니다.

 

산타페 연구소의 컴퓨터 과학자 크리스토퍼 무어는 이 성과에 대해 “이 정도 성과를 이루기 위해 그들이 이룩한 사회적, 수학적 엔지니어링은 정말 대단합니다”라고 평가했습니다.

 

아이랜드 메이누스 대학교의 컴퓨터 과학자이자 스테린의 지도 교수인 데미언 우즈는 “이렇게 빨리 해낼 줄 몰랐습니다. 정말 우사인 볼트급 성과입니다”라고 찬사를 보냈습니다.

 

‘바쁜 비버’를 찾는 여정은 궁극적으로 일종의 ‘트로피 사냥’과 같습니다. BB(5)의 특정 값이 다른 컴퓨터 과학 분야에 직접적인 응용을 갖고 있는 것은 아닙니다. 하지만 이 대담한 연구는 수학적 불가능성에 대한 도전에서 승리를 거두려는 그들만의 보람입니다. 아마도 그들이 승리하는 마지막 전투일지도 모릅니다.

멈출 것인가, 멈추지 않을 것인가

 

바쁜 비버 연구자들이 관심을 갖는 프로그램은 우리가 흔히 사용하는 프로그래밍 언어로 작성된 것이 아닙니다. 이 프로그램들은 튜링 머신이라 불리는 이론적 컴퓨터를 위한 명령어들입니다. 이 가상의 장치는 1936년, 컴퓨터 과학의 개척자 앨런 튜링이 컴퓨테이션 과정을 수학적으로 모델링하기 위해 고안한 것입니다.

 

튜링 머신은 무한히 긴 테이프를 읽고 쓰며 계산을 수행합니다. 이 테이프는 사각형 셀들로 나누어져 있으며, ‘머리’라는 장치가 한 번에 하나의 셀을 조작합니다. 각 튜링 머신은 고유한 규칙 세트를 가지고 있으며, 이 규칙에 따라 동작이 결정됩니다.

 

이 규칙 각각은 특정 셀에 도달했을 때 머리가 무엇을 해야 하는지를 정의합니다. 이는 셀에 적힌 숫자가 0인지 1인지에 따라 다르게 작동합니다. 즉, 튜링 머신의 명령어는 각 규칙에 대해 두 가지 경우를 나열한 표로 요약할 수 있습니다. 예를 들어, 첫 번째 열에는 “0을 읽으면 1로 바꾸고 오른쪽으로 한 칸 이동한 후 규칙 C를 참조할 것”이라는 규칙이 있을 수 있고, 두 번째 열에는 “1을 읽으면 그대로 두고 왼쪽으로 한 칸 이동한 후 규칙 A를 참조할 것”이라는 규칙이 있을 수 있습니다. 이러한 규칙들이 머신의 동작을 제어하며, 마지막 규칙 중 하나는 프로그램을 멈추라는 지시를 포함해 언제 멈출지를 결정합니다.

 

튜링 머신은 0과 1을 무한 테이프에 읽고 쓰면서 계산을 수행하며, 테이프는 왼쪽과 오른쪽으로 움직일 수 있습니다. 머신의 행동을 결정하는 것은 규칙의 목록입니다.
• 튜링 머신은 한 번에 하나의 규칙을 따르며, 각 규칙은 현재 셀에 무엇을 쓸지, 어디로 이동할지, 그리고 다음에 어떤 규칙을 따를지를 알려줍니다.
• 예를 들어, 규칙 A는 현재 셀에 1을 쓰고 오른쪽으로 이동한 뒤 규칙 B를 참조하라는 지시를 합니다.

• RULE A:
0을 읽으면 1을 쓰고 오른쪽으로 이동한 후 RULE B를 참조
1을 읽으면 그대로 두고 왼쪽으로 이동한 후 RULE C를 참조

RULE B:
0을 읽으면 1을 쓰고 왼쪽으로 이동한 후 RULE A를 참조
1을 읽으면 그대로 두고 오른쪽으로 이동한 후 RULE C를 참조

RULE C:
0을 읽으면 1을 쓰고 RULE A를 참조
1을 읽으면 멈춤

 

하지만 튜링 머신이 멈추는 방법이 있다고 해서, 그것이 실제로 멈출 것이라는 보장은 없습니다. 가장 단순한 경우, 몇 가지 상태를 반복하는 무한 루프에 빠질 수도 있습니다. 특정 규칙 집합을 가진 튜링 머신이 멈출지 영원히 실행될지를 확실히 알 수 있는 방법이 있을까요? 이것이 바로 ‘정지 문제’의 본질로, 바쁜 비버 사냥을 매혹적으로 만드는 어려운 문제입니다. 튜링은 이 정지 문제가 일반적인 해답을 가질 수 없음을 증명했습니다. 즉, 한 머신에 대해 작동하는 접근법이 다른 머신에서도 작동할 것이라는 보장은 없습니다.

 

정지 문제는 특정 머신에 대해서는 항상 어렵지만은 않습니다. 어떤 머신은 비교적 빠르게 멈추기도 합니다.

다른 머신은 무한 루프에 빠져 쉽게 알아챌 수 있습니다.

 

하지만 튜링 머신을 충분히 오랫동안 다루다 보면, 때로는 이러한 쉬운 분류에 저항하는 머신을 만나게 됩니다. 그 여정은 언젠가 끝날 것인가, 아니면 영원히 테이프 위를 방황하게 될 운명인가?

 

크리스토퍼 무어는 말했습니다. “충분히 오랜 시간 동안 실행하지 않으면 도대체 무엇을 하고 있는지 파악할 수 없습니다.”

그리고 “얼마나 오래 실행해야 충분한 걸까요?”

 

바쁜 비버의 시작

 

바쁜 비버 이야기는 헝가리 수학자 티보르 라도가 등장하면서 시작됩니다. 라도는 긴 여정을 겪은 인물로, 1895년 헝가리에서 태어나 토목공학을 공부하기 위해 대학에 입학했습니다. 하지만 그의 학업은 제1차 세계대전의 발발로 중단되었습니다. 러시아 전선에 파견된 그는 포로로 잡혀 시베리아의 포로 수용소에 보내졌고, 그곳에서 다른 포로의 도움으로 수학을 공부하기 시작했습니다.

 

4년 후 라도는 탈출에 성공했고, 러시아 북극을 가로질러 수천 마일을 여행해 결국 부다페스트로 돌아갔습니다. 그는 대학으로 돌아가 1920년대에 수십 편의 수학 논문을 발표한 후, 1930년 미국 오하이오 주립대학교에 교수로 부임해 35년 동안 그곳에서 일했습니다. 가장 길고 험난한 여정도 때로는 뜻하지 않게 마침표를 찍습니다.

 

말년에 라도는 계산 이론에 관심을 갖게 되었습니다. 그는 튜링의 증명 방식에 만족하지 못했는데, 튜링의 증명은 가능한 모든 튜링 머신을 고려하는 무한한 자기참조 논증이었기 때문입니다. 라도는 정지 문제의 본질을 더 단순한 형태로 추출하고자 튜링 머신을 규칙 개수에 따라 그룹으로 나누는 방식을 상상했습니다. 예를 들어, 하나의 규칙만 있는 튜링 머신의 그룹, 두 개의 규칙이 있는 튜링 머신의 그룹 등으로 나누는 것입니다. 물론 이런 그룹들은 무한히 많겠지만, 각 그룹 안의 머신들은 제한된 규칙 조합을 가질 수 있기 때문에 유한한 수로 존재하게 됩니다. 라도는 이렇게 유한한 그룹을 다루는 것이 모든 머신을 한 번에 고려하는 것보다 훨씬 더 단순하다고 판단했습니다.

 

1962년 라도는 이러한 그룹을 이용해 ‘바쁜 비버 게임’이라는 개념을 정의했습니다. 게임을 시작하려면 특정 규칙 개수를 선택합니다. 각 머신에게 모든 셀이 0으로 채워진 테이프를 제공합니다. 일부 머신은 영원히 작동을 계속하고, 나머지는 언젠가 멈추게 됩니다. 이 중 가장 오랫동안 작동하다가 멈추는 머신이 있을 것이고, 라도는 이처럼 성실히 작동하는 머신을 ‘바쁜 비버’라고 불렀습니다. n개의 규칙을 가진 그룹에서 바쁜 비버가 멈출 때까지 걸리는 단계 수를 바쁜 비버 수 BB(n)이라 정의했습니다. 이 게임의 목표는 이 수를 정확하게 구하는 것입니다.

 

성공하려면, 멈추는 모든 머신의 실행 시간을 계산해 가장 오래 걸리는 머신을 찾아내야 합니다. 또한, 나머지 머신이 멈추지 않음을 증명해야 합니다. 실행 시간 측정은 일반적인 컴퓨터에서 튜링 머신을 시뮬레이션하면 되기 때문에 비교적 간단합니다. 하지만 어떤 머신이 영원히 작동함을 증명하는 것은 일반적인 형태로는 불가능한 정지 문제를 해결하는 일입니다.

 

“우리는 알 수 없는 영역의 가장자리를 탐험하고 있습니다.” 바쁜 비버 챌린지의 기여자인 소프트웨어 엔지니어 숀 리고키는 이렇게 말했습니다.

 

하지만 도대체 어디에서부터 알 수 없는 영역이 시작되는 걸까요? 단 몇 개의 규칙만 가진 튜링 머신은 매우 단순해 보입니다. 명함 한 장에 적힐 정도의 프로그램을 이해하는 일이 그렇게 어렵기라도 할까요?

 

브래디의 바쁜 비버 탐험대

 

한 가지 규칙을 가진 경우는 간단합니다. 사실상 두 가지 경우밖에 없기 때문입니다. 규칙이 튜링 머신에게 0을 발견하면 멈추라는 지시를 내리면, 머신은 첫 번째 단계에서 멈춥니다. 그 외의 모든 규칙은 머신이 무한히 테이프를 따라 이동하게 만들 것입니다. 모든 셀에서 0을 만나기 때문입니다. 따라서 BB(1) = 1입니다.

 

그러나 이런 초보적인 비버 이후, 단순히 종이와 연필만으로 사냥에 나선 연구자는 금세 문제에 부딪힙니다. 두 개의 규칙을 갖는 경우 이미 6,000개 이상의 다양한 튜링 머신이 고려 대상이며, 세 개의 규칙으로는 수백만 개, 네 개의 규칙으로는 수십억 개에 달합니다. 이런 수많은 경우를 수작업으로 해결하는 것은 불가능합니다. “이건 분명히 불가능합니다,”라고 리고키는 말했습니다. “설령 할 수 있다 해도 아무도 믿어주지 않을 겁니다.”

 

따라서 이 계산의 근본에 뿌리를 둔 문제는 컴퓨터의 도움이 있어야만 해결할 수 있습니다. 비교적 간단한 프로그램을 통해 BB(2) = 6임을 증명할 수 있지만, BB(3)은 이미 찾기 어려운 문제입니다. 라도가 게임을 소개한 직후, 소수의 연구자들이 이 사냥에 나섰습니다.

 

그중 한 명이 오리건 주립대학교의 수학 대학원생 앨런 브래디였습니다. 아마도 학교의 마스코트가 비버인 것에 영감을 받아, 브래디는 얼마나 많은 비버를 잡을 수 있을지 탐구하기 시작했습니다. 그는 곧, 비약적인 진전을 이루기 위해서는 중요하지 않은 차이점은 무시하는 것이 핵심이라는 사실을 깨달았습니다. 예를 들어 첫 번째 규칙이 0을 읽으면 즉시 멈추라는 지시를 내리는 다수의 규칙을 가진 머신이 있다고 가정해봅시다.

 

“나머지 전환들이 무엇을 하든 상관없습니다. 왜냐하면 바로 멈추기 때문입니다,” 리고키는 설명했습니다. 바쁜 비버 게임에서는 이러한 머신들은 모두 불필요한 중복이기 때문에, 한꺼번에 제외할 수 있습니다.

 

브래디는 이러한 과정을 튜링 머신을 시뮬레이션하는 컴퓨터 프로그램에 통합했습니다. 이 프로그램은 동일한 규칙 개수를 가진 머신들의 초기 동작의 유사성에 따라 일종의 ‘가족 트리’를 구성했습니다. 머신 간의 차이가 중요해질 때에만 트리를 여러 가지 갈래로 나누고, 시뮬레이션이 멈추거나 무한 루프에 빠지는 가지는 잘라냈습니다.

 

이 프로그램을 작성하는 것만으로도 큰일이었지만, 브래디는 이를 실행할 수 있는 컴퓨터를 찾아야 했습니다. 1964년 당시, 이는 쉬운 일이 아니었습니다. 그는 결국 90마일 떨어진 포틀랜드 교외에 위치한 영장류 연구소의 컴퓨터 사용 허가를 얻었습니다. 흥미롭게도 그 연구소는 비버턴(Beaverton)이라는 이름을 가진 지역에 있었습니다.

 

연구 도중 브래디는 자신이 뒤처졌다는 소식을 들었습니다. 라도의 대학원생인 셴 린이 이미 BB(3) = 21임을 증명한 것입니다. (그와 라도는 1965년에 이 결과를 발표했습니다. 이는 라도가 사망하기 약 1년 전이었습니다.) 실망하지 않고, 브래디는 연구를 계속 진행하여 린의 결과를 확인했고 BB(4)에 대한 부분적인 진전을 이뤘습니다. 라도는 이 경우를 “전적으로 절망적”이라고 표현했었습니다.

 

BB(4)는 경우의 수가 방대하기 때문에 어려운 문제였을 뿐만 아니라, 네 가지 규칙을 가진 머신은 훨씬 더 복잡한 행동을 보일 수 있었습니다. 멈추지 않는 두 가지 규칙을 가진 머신은 쉽게 탐지할 수 있는 무한 루프에 빠지고, 세 가지 규칙에서는 몇십 개의 머신이 반복 없이 영원히 실행됩니다. 이 머신들이 결코 멈추지 않음을 증명하는 데는 다른 기법이 필요했습니다. 네 가지 규칙을 가진 경우에는 이러한 비순환 무한 머신이 수천 개에 달했습니다.

 

졸업 후 브래디는 멈추지 않는 새로운 유형의 튜링 머신들을 발견하고, 이를 그림자 나무(Shadow Trees)나 꼬리를 먹는 용(Tail-Eating Dragons)과 같은 이름으로 명명했습니다. 1966년, 그는 107단계 동안 실행한 후 멈추는 네 가지 규칙의 머신을 발견했고, 이것이 바로 희귀한 네 번째 바쁜 비버일 것이라고 추측했습니다. 그의 추측은 옳았으나, 더 오래 실행되는 멈추는 머신이 없음을 증명하는 데는 1974년까지 걸렸습니다. 그 시점에서 브래디는 미국 네바다 대학교 리노 캠퍼스에서 컴퓨터 과학 교수로 일하며 전국 마라톤 대회에 출전할 정도로 장거리 달리기에 도전하고 있었습니다. 그는 자신의 증명을 내부 기술 보고서에 기록했으며, 학술지에 정식으로 발표한 것은 9년 후의 일이었습니다.

 

이로써 인류가 아는 마지막 바쁜 비버 수는 40년 이상 동안 밝혀지지 않았습니다.

 

다섯 번째 바쁜 비버 찾기

 

브래디가 그의 증명을 발표한 해는 도르트문트 대회가 열린 해이기도 했습니다. 이 대회는 다섯 번째 바쁜 비버를 찾기 위한 첫 번째 대규모 사냥이었습니다. 다섯 가지 규칙을 가진 경우 가능한 튜링 머신의 수는 무려 17조 개에 달합니다. 모든 튜링 머신을 하나씩 나열하는 데만 1밀리초당 하나씩 하더라도 500년 이상이 걸립니다. 따라서 검색 공간을 좁혀주는 브래디의 ‘가족 트리’ 기법과 같은 기술이 필수적이었지만, 프로그램의 속도 역시 매우 빨라야 성공할 가능성이 있었습니다.

 

도르트문트 대회의 참가자들은 각자 자신만의 비버 검색 프로그램을 개발하여 찾을 수 있는 가장 오랫동안 실행되는 다섯 가지 규칙의 튜링 머신을 제출했습니다. 가장 바쁜 머신은 10만 단계 이상을 거쳐 멈췄습니다. 이 대회에 대한 과학 아메리칸 지의 1984년 기사는 새로운 세대의 연구자들에게 바쁜 비버 게임을 소개했습니다. 이들 중 한 명은 곧 200만 단계에 이르러 멈추는 머신을 발견하며 도르트문트 기록을 갱신했습니다.

 

새롭게 등장한 사냥꾼 중에는 베를린의 대학원생 하이너 막센과 위르겐 분트록도 있었습니다. 그들은 여가 시간에 이 문제를 함께 연구하며 튜링 머신 시뮬레이션을 가속화하기 위한 새로운 수학적 기법을 개발했습니다. 그러나 200만 단계 기록을 넘지 못하자 그들의 관심도 차츰 줄어들었습니다. 몇 년 후인 1989년, 막센은 프로그래머로 일하고 있던 회사에서 강력한 새 컴퓨터를 구입하게 되었고, 이에 맞춰 자신의 비버 사냥 프로그램을 다시 실행해보기로 했습니다. 주말 동안 프로그램을 실행해 200만 단계 머신을 재발견하기를 기대했지만, 대신 그의 프로그램은 무려 47,176,870단계 이후 멈추는 머신을 발견했습니다.

 

처음에 그는 코드에 버그가 있다고 생각했습니다. “몇 시간 동안 디버깅을 멈추고 이상한 느낌이 들기 시작했습니다.”라고 막센은 이메일에 썼습니다. 분트록 역시 이 결과를 복제하는 데 성공했고, 이들은 1990년 초 베를린 장벽이 무너진 이후 열띤 분위기 속에서 논문을 발표했습니다. 사실 막센은 다섯 번째 바쁜 비버를 잡은 것이었지만, 나머지 머신들이 멈추지 않는다는 것을 증명하는 데는 30년 이상이 걸렸습니다.

 

2000년대 초, 불가리아의 컴퓨터 과학자 게오르기 이바노프 게오르기에프가 아슬아슬하게 접근했습니다. 당시 그는 불가리아 국영 통신회사에서 시스템 관리자였으며, 업무는 큰 노력을 요하지 않았습니다. 그는 BB(5) 문제를 두고 매일 몇 시간씩 몰두하며 멈추지 않는 새로운 유형의 머신을 찾아내기 위한 컴퓨터 프로그램을 개발했습니다. 최종 프로그램은 6,000줄에 이르는 주석이 없는 복잡한 코드였고, 실행하는 데 일주일이 넘게 걸렸습니다. 프로그램은 약 100개의 튜링 머신을 해결하지 못하고 남겼고, 그는 이들 중에서 손으로 분석해 43개의 후보를 남겼습니다.

 

2003년, 게오르기에프는 ‘스켈레트(Skelet)’라는 불가리아어 별명으로 온라인에 자신의 연구 결과를 게시했습니다. 그는 이메일에서 “학생 시절 저는 매우 말랐고, 제 동급생들이 그런 별명을 붙였습니다.”라고 설명했습니다.

 

막센은 게오르기에프에게 계속 노력하라고 격려했지만, 2년간의 집중적인 연구는 그에게 큰 부담을 남겼습니다. “이 기간이 끝났을 때, 저는 더 이상 새로운 아이디어를 만들어낼 수 없었습니다. 매우 피곤했습니다.”라고 게오르기에프는 말했습니다.

 

이는 바쁜 비버 연구자들에게 흔한 일이었습니다. 수십 년 동안 그들은 혼자 또는 두 명이 짝을 이루어 연구해 왔으며, 학계의 주목을 거의 받지 못했습니다. 이 문제를 완성하기 위해서는 집단적인 노력이 필요했습니다.

 

사냥꾼을 부르다

 

이 집단적 노력은 트리스탄 스테린으로부터 시작되었습니다. 그는 2000년대 후반 인스턴트 메신저 플랫폼에서 코딩 대회에 열정을 가진 친구를 만나면서 어린 나이에 컴퓨터 프로그래밍에 능숙해졌습니다. 하지만 곧 코딩 대회의 문화가 자신과 맞지 않음을 깨달았습니다.

 

“저는 경쟁적인 사람이 아닙니다,” 스테린은 말했습니다. “저는 문제를 보고 세 달 동안 고민하는 것이 좋지, 30분 안에 해결하려고 하는 건 별로입니다.”

 

이 호기심 가득한 정신은 스테린을 프랑스에서 아일랜드의 대학원으로 이끌었습니다. 그곳에서 그는 우즈 교수와 함께 DNA 컴퓨팅 연구를 진행하며, DNA 가닥을 이용해 알고리즘을 구현하는 방법을 탐구했습니다. 2020년 여름, 우즈는 스콧 애런슨이라는 컴퓨터 과학자가 작성한 바쁜 비버에 대한 설문 논문을 그에게 보냈습니다. 스테린은 즉시 매료되었습니다. 우즈와 함께 대형 튜링 머신의 능력에 관한 논문을 공동 집필한 후, 스테린은 BB(5) 문제에 집중하며, 마르크센과 분트록의 4,700만 단계 머신이 정말로 다섯 번째 바쁜 비버인지 증명하고자 결심했습니다.

 

“저 혼자서는 해낼 수 없다는 강한 직감이 들었어요,” 스테린은 말했습니다. “하지만 이 문제는 해결될 수 있다는 확신도 있었습니다.”

 

2022년, 트리스탄 스테린은 다섯 번째 바쁜 비버 수의 정확한 값을 결정하기 위한 온라인 협업 프로젝트 ‘바쁜 비버 챌린지’를 시작했습니다. “저 혼자서는 절대 해낼 수 없었을 겁니다,”라고 그는 말했습니다.

 

처음부터 스테린은 결론적인 증명이 제대로 문서화되고 재현 가능해야 한다는 점을 알고 있었습니다. 작은 소프트웨어 버그 하나만으로도 모든 노력이 물거품이 될 수 있었기 때문입니다. 게오르기에프의 프로그램은 매우 정교했지만, 다른 연구자들에게는 분석하기 어려운 코드였습니다.

 

“그의 코드를 검토하려고 돌아보면 포기하게 됩니다,”라고 바쁜 비버 챌린지에 합류한 소프트웨어 개발자이자 전 수학 대학원생인 저스틴 블랜차드는 말했습니다. 따라서 새로운 접근법은 사실상 처음부터 시작해야 했습니다.

 

스테린은 전통적인 접근법을 기반으로 하되, 몇 가지 조정을 추가하기로 했습니다. 그는 먼저 브래디의 가족 트리 방법을 이용해 불필요한 튜링 머신을 제거하고, 4,700만 단계 이내에 멈추는 머신을 식별하는 것으로 시작했습니다. 하지만 브래디나 그의 후계자들과는 달리, 스테린은 무한히 실행되는 머신을 걸러내는 코드를 포함하지 않았습니다. 대신, 각기 다른 튜링 머신이 멈추지 않음을 증명하기 위한 독립적인 프로그램을 활용하기로 했습니다. 이렇게 작업을 여러 부분으로 나누면 협업자들이 각 부분을 독립적으로 작업하고 결과를 상호 검토하기가 쉬워집니다.

 

2021년 말, 스테린은 첫 단계의 컴퓨터 프로그램을 작성했습니다. 이 프로그램은 BB(5)를 결정하기에 충분한 약 1억 2천만 개의 튜링 머신 목록을 생성했으며, 나머지는 모두 중복된 것으로 판명되었습니다. 그중 약 4분의 1은 마르크센과 분트록의 머신보다 일찍 멈췄으며, 8천8백만 개는 여전히 검토 대상이었습니다.

 

이 머신들을 분석하기 위해, 스테린은 “시공간 다이어그램”을 통해 이들의 동작을 시각화하는 온라인 인터페이스를 구축했습니다. 이 다이어그램은 0과 1을 각각 어두운 사각형과 밝은 사각형으로 나타내는 이차원 그리드로, 각 줄은 튜링 머신의 진화를 한 단계씩 기록합니다. 첫 번째 줄은 첫 단계 이후의 테이프를, 두 번째 줄은 두 번째 단계 이후의 테이프를 보여주는 방식입니다. 이 방식으로 보면 스테린의 수많은 머신들이 다양한 패턴을 보여주며 생동감을 띠기 시작합니다. 마르크센과 분트록이 정말로 다섯 번째 바쁜 비버를 발견했다는 것을 입증하려면 이들 중 모든 머신이 영원히 실행됨을 증명해야 했습니다.

 

이 부분은 스테린 혼자서는 해낼 수 없는 작업이라는 점을 그는 알고 있었습니다. 게다가 그에게는 다른 책임도 있었습니다. 그는 친구들과 함께 소프트웨어 스타트업을 창업했고, 여전히 학위 논문을 마쳐야 했습니다. 2022년 봄, 스테린과 초기 참여자 몇 명은 독립적인 플랫폼인 디스코드에 포럼과 별도의 채팅 서버를 개설했습니다. 이제 협력자를 찾을 차례였습니다.

 

바쁜 비버의 매력에 빠지다

 

숀 리고키가 팀에 합류한 건 시간 문제였습니다. 어쩌면 운명적이었을지도 모릅니다. 그는 1985년 비버턴에서 태어났고, 바쁜 비버에 대해 처음 알게 된 것은 2004년, 대학 첫 학기를 마치던 겨울방학 때였습니다. 방학 중에 리고키는 로렌스 버클리 국립 연구소에서 응용 수학자로 일하는 아버지 테리와 함께 비버 탐색 알고리즘을 실험하기 시작했습니다.

 

한 달 후, 리고키가 다시 대학으로 돌아가 수업에 집중하고 있을 때 아버지가 전화를 걸어왔습니다. 아버지는 원조 바쁜 비버 게임의 변형을 브래디가 고안한 방식으로 테스트하다가 브래디의 기록을 깨는 머신을 발견했다고 흥분하며 말했습니다. 이들은 은퇴한 브래디에게 연락했고, 그는 매우 기뻐하며 자신의 웹사이트에 이 결과를 알렸습니다. 이 일을 계기로 숀 리고키는 전 세계의 바쁜 비버 연구자들과 이메일을 주고받기 시작했습니다.

 

“커뮤니티는 정말 환영해줬어요,”라고 그는 말했습니다. “그때 저는 완전히 바쁜 비버에 매료되었습니다.”

 

리고키에게 잊을 수 없는 만남은 대학교 2학년 여름 독일을 방문했을 때 일어났습니다. 그는 베를린으로의 짧은 여행 중 마르크센과 만났고, “바쁜 비버를 통해 언어 장벽을 넘을 수 있었습니다,”라고 말했습니다. 또한 맥주도 도움이 되었습니다. 리고키는 결국 맥주를 너무 많이 마셔서 함부르크로 돌아가는 기차를 놓쳤습니다.

 

리고키는 대학 생활 동안 내내 바쁜 비버의 매력에서 벗어나지 못했습니다. 하지만 졸업 후 직장을 구하면서 바쁜 비버 사냥은 잠시 뒷전으로 밀려났습니다. 그는 때때로 사냥에 복귀했지만 오래 지속되지는 않았습니다. 2022년 초, 그는 연구자들이 서로 소통할 수 있도록 온라인 토론 그룹을 개설했습니다. 그러던 중 5월에 스테린이 이 메일링 리스트를 발견하고 바쁜 비버 챌린지에 참여하라는 초대장을 보냈습니다. 리고키는 두 번 생각할 필요도 없었습니다.

 

프로젝트에 대한 그의 첫 기여 중 하나는 마르크센이 고안한 기술을 되살리는 것이었습니다. 이는 16년 전 베를린의 술집에서 논의했던 “폐쇄 테이프 언어 기법”이었습니다. 이 방법은 튜링 머신의 테이프에서 멈추지 않을 징후를 나타내는 패턴을 식별하는 새로운 방식이었습니다. 이 기법은 무한 루프 머신과 다양한 유형의 멈추지 않는 머신을 식별하는 프로그램의 기본 전략이었지만, 폐쇄 테이프 언어 기법은 통합된 수학적 틀을 사용하여 훨씬 더 넓은 범주의 패턴을 식별할 가능성을 가지고 있었습니다.

 

리고키는 블로그 게시글을 통해 새로운 협력자들에게 이 기법을 소개했지만, 이론적인 개념이 매우 일반적이었음에도 불구하고 모든 경우를 포괄할 수 있는 프로그램을 작성하는 방법은 알지 못했습니다. 프로젝트에 가을에 합류한 블랜차드가 곧 이 문제를 해결했지만, 그의 프로그램은 상대적으로 느렸습니다. 이후 두 명의 다른 기여자가 프로그램의 속도를 크게 향상시켰습니다. 몇 달 만에 폐쇄 테이프 언어 기법은 유망한 아이디어에서 가장 강력한 도구 중 하나로 발전했습니다. 이 기법은 게오르기에프가 남긴 43개의 문제 머신 중 10개를 해결할 수 있었고, 그의 이름을 따서 이들 머신을 ‘스켈레트 머신’이라 불렀습니다.

 

리고키는 “이건 한 사람이 기여해서는 절대 존재할 수 없었을 겁니다,”라고 말했습니다.

 

거대한 도전이 다가오다

 

시간이 지나면서, 새로운 기여자들이 바쁜 비버 챌린지를 발견하고 문제의 여러 부분을 해결해 나갔습니다. 그러나 여전히 많은 머신들이 미해결 상태로 남아 있었으며, 그중 두 머신은 특히 악명 높은 존재로 자리 잡았습니다.

 

첫 번째는 ‘스켈레트 #1’이었습니다. 이 머신은 예측 가능한 행동과 혼란스러운 행동 사이를 반복하며 실행되었습니다. 2023년 3월, 리고키와 또 다른 기여자인 파벨 크로피츠가 이를 해결할 아이디어를 고안해냈습니다. 이들은 마르크센과 분트록의 30년 된 가속 시뮬레이션 기법을 강화한 버전을 사용하여, 질서와 혼돈 사이의 줄다리기가 결국 끝난다는 것을 발견했습니다. 그러나 그 결과가 나오기까지는 무려 ‘1조 x 1조’ 단계 이상의 시간이 걸렸습니다. 그 후에도 머신은 예외적으로 긴 반복 주기에 들어섰습니다. 대부분의 무한 루프는 1,000단계 내에 반복을 시작하지만, 스켈레트 #1은 80억 단계 이상을 거친 후에야 반복을 시작했습니다.

 

“도대체 누가 이런 걸 주문한 거죠?” 블랜차드는 말했습니다. “이건 어디에서 온 건가요? 왜 존재하는 거죠?”

 

이 머신의 행동은 너무나도 기이했고, 이 증명에는 다양한 아이디어가 복합적으로 결합되어 있어서, 리고키는 거의 5개월 동안 결과에 확신을 가질 수 없었습니다. 그 불확실성을 해소해준 것은 새로운 기여자였습니다. 폴란드 출신의 21세 자습 프로그래머인 마야 칸지올카(주로 ‘메이’로 불림)가 바로 그 인물입니다.

 

메이는 2021년 가을 학기에 바르샤바 대학교에 입학했지만, 엄격한 커리큘럼과 코로나19로 인한 원격 수업이 본인의 학습 스타일과 맞지 않아 한 학기 만에 학교를 그만두었습니다. 이후 소프트웨어 회사에서 1년 넘게 일했지만, 일의 소진감을 느끼며 더 지적 자극을 줄 수 있는 활동을 찾기 시작했습니다. 그러다 Coq라는 소프트웨어를 알게 되었고, 이를 통해 수학적 증명의 유효성을 검증하는 방법을 배우며 몰입하게 되었습니다.

 

세상에 존재하지 않는 가장 중요한 머신

 

바쁜 비버 챌린지 기여자들은 이미 증명에 컴퓨터 프로그램을 사용하고 있었지만, 종이와 펜으로 하는 증명처럼 컴퓨터 프로그램도 오류에 취약합니다. 그러나 Coq 증명에서는 모든 라인이 이전 라인에서 논리적으로 도출되지 않으면 코드가 실행되지 않기 때문에 오류가 사실상 불가능합니다. 메이에게 Coq로 증명을 구성하는 일은 게임과 같았습니다. “거의 중독성 있어요,”라고 그들은 말했습니다. “보통 시간에 시작했는데 어느새 밤이 되었고, 그리고 아침이 되었어요.”

 

Coq를 익힌 후, 메이는 이 소프트웨어를 시험할 미해결 문제를 찾기 시작했고, 그때 바쁜 비버 챌린지를 발견했습니다. 몇 주 후, 메이는 팀의 여러 증명을 Coq로 번역했고, 이 과정에서 리고키와 크로피츠의 스켈레트 #1이 멈추지 않는다는 증명도 포함되었습니다. 이제 리고키는 이 결과에 대한 확신을 가질 수 있게 되었습니다. 스테린이 강조했던 재현 가능성 이상의 높은 수준의 엄격함이 갑자기 가능해진 것입니다. 그리고 이 모든 것은 정식 교육을 받지 않은 한 ‘아마추어’ 수학자로부터 시작되었습니다.

 

“아마추어라는 의미를 잊지 말아야 합니다,” 무어는 말했습니다. “그것은 수학을 사랑하는 사람을 뜻하지, 비하의 의미가 아닙니다.”

 

댐이 터지다

 

이와 비슷한 시기에 대학원생 크리스 쉬가 두 번째 난제, ‘스켈레트 #17’ 머신에서 돌파구를 마련했습니다. 대부분의 다섯 가지 규칙을 가진 튜링 머신들은 어떻게 작동하는지 원리를 이해하고 나면 그 행동을 요약하기 쉬웠습니다. 그러나 스켈레트 #17 같은 머신을 만나면 “우주가 우리를 조롱하는구나”라는 생각이 듭니다. 메이는 이를 이렇게 표현했습니다. 스켈레트 #17의 테이프에 나타나는 패턴을 이해하는 것은 네 겹의 암호화된 비밀 메시지를 해독하는 것과 같았습니다. 하나의 암호를 풀면 전혀 다른 암호가 드러나고, 그 아래로도 두 개의 암호가 더 숨어 있었습니다. 쉬는 이 모든 암호를 해독한 후에야 머신이 멈추지 않는다는 것을 증명할 수 있었습니다.

 

쉬의 증명은 놀라운 성과였지만, Coq가 요구하는 엄밀한 수학적 형식으로는 설명하기 어려운 수학적 직관을 포함하고 있었습니다. 더욱이, 바쁜 비버 챌린지의 작업은 끝나지 않았습니다. 스켈레트 #1과 #17은 가장 어려운 문제로 보였지만, 해결되지 않은 머신들이 남아 있었고, 일부는 비효율적인 프로그램으로만 해결된 상태였습니다. 이는 세계를 설득하기에는 충분하지 않았습니다.

 

“우리는 어느 정도 재현 가능성이 있는 결과를 원했습니다,” 블랜차드는 말했습니다. “그리고 증명서에 ‘63단계: 이 프로그램을 6개월간 실행하라’고 쓰는 방식은 피하고 싶었습니다.”

 

그 후 몇 달간 커뮤니티는 남은 머신들에 대한 증명을 천천히 완성해 나갔지만, 대부분은 아직 Coq로 번역되지 않았습니다. 그런 가운데 4월에 ‘mxdys’라는 가명으로 알려진 신비한 새로운 기여자가 등장하여 이 작업을 마무리했습니다. 팀 내에서는 mxdys의 위치나 개인 정보에 대해 아는 사람이 아무도 없었습니다. 디스코드에서의 직접 메시지 대화에서 그들은 수학적 게임에 대한 오랜 관심을 언급했지만, 배경에 대한 자세한 정보는 공유하지 않았습니다.

 

5월 10일, mxdys는 디스코드 서버에 간결한 메시지를 남겼습니다. “BB(5)의 Coq 증명이 완성되었습니다.” 스테린은 1분 후에 7개의 느낌표를 연달아 남겼습니다. 몇 주 만에 mxdys는 커뮤니티의 기술을 세련되게 다듬고, 그 결과물을 4만 줄에 이르는 단일 Coq 증명으로 종합했습니다.

 

“이것은 결코 쉽게 형식화할 수 있는 일이 아닙니다,” 프랑스 국립 연구소 Inria의 Coq 전문가인 야닉 포스터는 말했습니다. “저는 아직도 긍정적인 충격을 받고 있습니다.”

 

마르크센과 분트록이 30년 넘게 전에 발견한, 4천7백만 단계 후에 멈추는 그 머신이 정말로 다섯 번째 바쁜 비버라는 사실이 증명되었습니다.

 

“이 소식은 저에게 정말 기쁩니다,” 게오르기에프는 이메일에서 썼습니다. “제 생애에 이 문제가 해결될 것이라고는 예상하지 못했습니다.”

 

그러나 또 다른 바쁜 비버 개척자에게는 이 소식이 너무 늦게 전해졌습니다. 앨런 브래디는 4월 21일에 90세의 나이로 세상을 떠났습니다. 증명이 완성되기 불과 한 달 전이었습니다.

 

비버들이 사는 곳에서

 

바쁜 비버 챌린지의 기여자들은 자신들의 결과를 정리한 공식 학술 논문 초안을 작성하기 시작했습니다. 이는 시간이 걸릴 작업입니다. 대부분의 머신들은 여러 가지 방법으로 멈추지 않음을 증명했기 때문에, 팀은 이 결과들을 하나의 증명으로 통합하는 최적의 방식을 결정해야 합니다.

 

한편, 팀의 일부는 이미 다음 바쁜 비버 수에 도전하고 있습니다. 하지만 불과 4일 전, 메이와 ‘레이첼린’이라는 다른 기여자는 BB(6)에 대한, 극복하기 어려운 장벽을 발견했습니다. 이 장벽은 정지 문제가 악명 높은 난제인 콜라츠 추측과 유사한 여섯 가지 규칙을 가진 머신입니다. 튜링 머신과 콜라츠 추측 사이의 연결성은 1993년 수학자 파스칼 미셸의 논문에서 처음 언급되었지만, 새로 발견된 ‘안티히드라’라는 별명을 가진 이 머신은 수학적으로 개념적 돌파구 없이는 풀 수 없는 가장 작은 사례로 보입니다. 이는 BB(5) 결과에 추가적인 의미를 부여하는 요소입니다.

 

“이것이 우리가 알게 될 마지막 바쁜 비버 수일 수도 있습니다,”라고 애런슨은 말했습니다.

 

바쁜 비버 문제에는 다양한 변형들이 있으며, 일부 바쁜 비버 챌린지 기여자들은 이러한 변형 문제들에 대해 연구를 계속할 계획입니다. 그러나 모두가 이 작업을 계속하려는 것은 아닙니다. 그들은 각자 자신만의 이유로 이 프로젝트에 참여했고, 이제 그들의 여정은 점차 갈라지기 시작하고 있습니다.

 

스테린은 다른 수학 분야에서 협업 온라인 프로젝트를 촉진하는 소프트웨어 도구를 개발하고자 합니다. 그는 “바쁜 비버 챌린지가 저에게 준 것은, 매우 효과적인 연구 방법이라는 깊고 깊은 확신입니다. 이것은 더 큰 무대에서 다뤄질 가치가 있습니다.”라고 말했습니다.

 

메이 역시 한 발 물러섰습니다. 그들은 현재 유럽의 국제 철도망에 흥미를 갖게 되었습니다. “아마 언젠가는 다시 바쁜 비버 연구에 돌아올 것 같지만, 지금 당장은 마음에 두고 있는 일이 아닙니다. 지금은 기차 운전사가 되는 것을 목표로 하고 있습니다.”

 

리고키는 바쁜 비버 사냥을 계속할 생각이지만, 20년간 열정적인 연구와 관심에서의 이탈을 반복하며, 미래에 대한 자신의 예측에 너무 의존하지 않게 되었다고 말합니다.

 

“정지 문제와 같아요,”라고 그는 말했습니다. “무슨 일이 일어날지는 결코 확신할 수 없습니다.”