바쁜 비버 문제, 40년 동안 지속된 컴퓨터 과학 문제가 마침내 아마추어 그룹에 의해 해결되었습니다! 이러한 획기적인 발전은 학계에 충격을 주었을 뿐만 아니라, 유명한 수학자 테렌스 타오(Terence Tao)에게도 인정을 받아 1983년 이후 이 분야에서 가장 중요한 발전으로 칭송받았습니다. Coq 증명 도우미를 사용하여 다섯 번째 바쁜 비버 숫자 BB(5)의 값이 47,176,870임을 성공적으로 확인했습니다. 이는 복잡한 수학적 문제를 해결하는 데 있어 소프트웨어 지원 증명의 큰 잠재력을 보여주고 Turing 기계 동작에 대한 통찰력을 제공합니다. 그리고 새로운 관점을 멈추는 것입니다.
컴퓨터 과학의 신비로운 영역에서 바쁜 비버 문제(Busy Beaver Problem)라는 40년 된 문제가 최근 아마추어 그룹에 의해 성공적으로 해결되었습니다. 이 성과는 학계에 센세이션을 일으켰을 뿐만 아니라, 이 소식을 소셜 미디어에 알리고 수학 연구에서 증명 보조자의 중요성을 강조한 유명한 수학자 테렌스 타오(Terence Tao)에게도 인정받았습니다.
컴퓨터 과학자인 스콧 애런슨(Scott Aaronson)도 이 발견을 높이 평가하며, 이것이 1983년 이후 바쁜 비버 기능 연구에서 가장 중요한 발전이라고 믿었습니다. 이 성과는 계산 이론의 경계에 대한 깊은 이해를 나타내며 복잡한 수학적 문제를 해결하는 데 있어 소프트웨어 지원 증명의 잠재력을 보여줍니다.
바쁜 비버 문제는 40여년 전 독일 도르트문트에서 컴퓨터 과학자들이 멈추기 전에 가장 많은 1을 쓸 수 있는 특정 튜링 기계를 찾으려고 시도했을 때 시작되었습니다. 튜링 머신(Turing machine)은 1936년 앨런 튜링(Alan Turing)이 제안한 추상 컴퓨팅 모델로, 무한히 긴 자기 테이프에서 0과 1을 읽고 쓰는 방식으로 계산을 수행합니다.
1974년 네 번째 바쁜 비버의 숫자가 결정된 후 다섯 번째 비버를 찾는 것이 공개적인 질문이 되었습니다. 이제 전 세계 20명 이상의 기여자로 구성된 온라인 커뮤니티는 Coq이라는 증명 보조 소프트웨어를 사용하여 다섯 번째 Busy Beaver 숫자 BB(5)의 값이 47,176,870임을 성공적으로 확인했습니다.
이 성과는 커뮤니티를 흥분시켰을 뿐만 아니라 발전을 우사인 볼트의 속도에 비유한 컴퓨터 과학자 데미안 우즈(Damien Woods)의 놀라움을 불러일으켰습니다. 비록 이 문제에 대한 해결책이 컴퓨터 과학의 다른 분야에 직접적으로 적용될 수는 없을지라도, 참가자들에게는 수학적 불가능성에 대한 투쟁은 그 자체로 가장 큰 보상입니다.
바쁜 비버 문제의 핵심은 튜링 기계의 동작, 특히 정지 문제에 대한 성능을 이해하는 데 있습니다. 튜링 기계의 동작은 테이블로 상상할 수 있는 일련의 규칙에 의해 정의됩니다. 각 규칙은 읽기/쓰기 헤드가 특정 상태에서 0 또는 1을 발견할 때 수행해야 하는 작업을 지정합니다.
Turing 기계는 무한 루프에 갇힐 수 있지만 작동을 멈추는지 여부를 결정하는 것은 해결되지 않은 문제로 잘 알려져 있습니다. 수학자 티보르 라도(Tibor Radó)는 이 결론에 만족하지 않았고, 따라서 튜링 기계를 규칙 수에 따라 그룹화하여 정지 문제의 본질을 탐구하기 위해 "바쁜 비버 게임"을 발명했습니다.
Allen Brady와 같은 초기 연구자들은 Turing 기계의 동작을 시뮬레이션하는 프로그램을 작성하여 이 문제를 조사했습니다. 그의 연구와 다른 연구자들의 발견은 이후의 탐험가들을 위한 토대를 마련했습니다.
2022년까지 대학원생 Tristan Stérin은 BB(5) 완성을 목표로 하는 온라인 협업 프로젝트인 Busy Beaver Challenge를 시작했습니다. 혁신적인 방법과 Coq 증명 보조자의 도움을 통해 팀은 마침내 다섯 번째 바쁜 비버를 찾는 데 성공했습니다.
이 성과는 수학의 불가능성에 대한 도전일 뿐만 아니라 컴퓨터 과학의 한계에 대한 탐구이기도 합니다. BB(5)가 확인됨에 따라 연구원들은 Coq 증명을 보완하는 사람이 읽을 수 있는 버전이 될 학술 논문 초안을 작성하고 있습니다. 동시에 BB(6) 탐사가 다음 목표가 될지도 고민하고 있다.
참조: https://www.Quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
바쁜 비버 문제에 대한 해결책은 수학 분야의 획기적인 돌파구일 뿐만 아니라, 미래 컴퓨팅 이론 연구에 새로운 방향과 아이디어를 제공합니다. 이번 성과는 더 많은 사람들이 수학과 컴퓨터 과학 연구에 참여하고 미지의 영역을 함께 탐구하도록 장려합니다.