당신이 수천 명의 사람들이 참여하는 거대한 '전화기 게임(telephone)'이나, 운전자의 기분에 따라 신호등이 바뀌는 도시와 같은 혼돈스러운 시스템의 미래를 예측하려고 한다고 상상해 보십시오. 컴퓨터 과학의 세계에서 이것은 **확률적 모델 검증(probabilistic model checking)**이라고 불립니다. 이는 시스템에 무작위성과 우연이 가득할 때조차, 시스템이 특정 목표(예: "모든 교수가 회의를 마친다")에 도달할 확률이 얼마나 되는지를 수학적으로 증명하는 방법입니다. 문제는 시스템에 사람이나 구성 요소가 추가될수록 가능한 시나리오의 수가 폭발적으로 증가한다는 점입니다. 이는 마치 해변의 모래알 하나하나를 세려고 하는 것과 같으며, 해변 자체가 계속 커지고 있는 상황과 같습니다. 수학적 계산이 너무 무거워져서 가장 빠른 슈퍼컴퓨터조차 답을 내놓기도 전에 메모리나 시간 부족으로 멈춰버릴 수 있습니다.

수년 동안 이 문제를 해결하기 위한 최고의 도구들은 모든 막다른 길을 보여주는 상세한 손그림 지도를 보고 미로를 탐색하는 것과 같았습니다. 이러한 도구들은 미로에 빈 공간이 많을 때(희소 역학, sparse dynamics)는 훌륭하지만, 경로가 빽빽하게 들어찬 경우(밀집 역학, dense dynamics)에는 고전합니다. 이들은 현대의 그래픽 카드(GPU)에서 발견되는 초고속 병렬 프로세서와 잘 맞지 않는 구식 방식에 의존합니다. 참고로 GPU는 오늘날의 비디오 게임과 AI의 엔진입니다.

이때 워털루 대학교 연구진이 개발한 Tessa라는 새로운 접근 방식이 등장했습니다. 전체 시스템을 모든 가능성의 지도를 그리는 대신, 수학에서 **텐서(tensor)**라고 불리는 거대한 다차원 데이터 블록으로 취급하기로 결정한 것입니다. 텐서를 단순한 스프레드시트가 아니라, 한꺼번에 찌그러뜨리고 늘리고 회전시킬 수 있는 숫자의 하이퍼 큐브(hyper-cube)라고 생각하십시오. Tessa는 "시스템이 목표에 도달할 것인가?"라는 문제를 현대의 그래픽 카드가 완벽하게 이해할 수 있는 언어로 번역함으로써, 거대하고 복잡한 시스템의 수치를 매우 짧은 시간 안에 계산해 낼 수 있습니다.

연구진은 이것이 작동할 것이라고 단순히 추측한 것이 아니라, 수학적으로 건전함을 증명한 후 이를 테스트할 도구를 구축했습니다. 연구진이 까다롭고 빽빽한 시나리오(예: 17개의 프로세서 또는 10개의 큐를 가진 모델)에 대해 Tessa를 기존의 최첨단 도구들과 비교 실험했을 때, Tessa는 100배 이상 빨랐습니다. 500단계의 호라이즌(horizon)을 포함한 특정 테스트에서는 300배 이상 빨랐습니다. 이 논문은 문제의 표현 방식을 '희소한 지도'에서 '병렬 처리가 가능한 밀집된 데이터 블록'으로 전환함으로써, 이전에는 검증할 수 없었던 규모의 시스템을 검증할 수 있는 능력을 깨울 수 있음을 보여줍니다. 이것이 모든 것을 해결하는 마법 지팡이는 아니지만(밀집된 시스템에는 잘 작동하지만, 희소한 시스템에는 그렇지 않습니다), 이전에 도달할 수 없었던 문제를 해결할 수 있는 완전히 새로운 놀이터를 열어줍니다.

Tessa의 이야기: 혼돈을 춤으로 바꾸다

Tessa가 어떻게 이 마법 같은 일을 수행하는지 더 깊이 파헤쳐 보겠습니다. N명의 교수가 휴대폰으로 설문에 참여하려는 모습을 보고 있다고 상상해 보십시오. 각 교수는 세 가지 상태 중 하나에 있습니다: 부재 중(휴대폰을 무시함), 낙서 중(설문을 보고 있음), 완료(제출 완료). 매 초마다 교수는 이메일을 확인하거나, 주의가 분산되거나, 마침내 제출 버튼을 누를 수 있습니다. 문제는? 그들은 언제든 방해를 받을 수 있다는 점입니다.

모든 사람이 특정 시간 내에 완료할 확률을 알아내기 위해, 전통적인 도구들은 모든 상태의 조합을 나열하려고 시도합니다. 만약 10명의 교수가 있다면, 이는 $3^{10}$ (59,049)개의 조합입니다. 20명이 된다면 30억 개가 넘습니다. 전통적인 도구들은 이러한 조합들을 거대한 희소 리스트(대부분의 페이지가 빈 백과사전 같은 형태)로 저장하려고 합니다. 이는 작은 그룹에서는 괜찮지만, 그룹이 커지고 상호작용이 복잡해지면(밀집되면), 리스트가 메모리에 담기에 너무 커져서 컴퓨터가 마비됩니다.

Tessa의 통찰: 하이퍼 큐브
Tessa는 이 문제를 다르게 바라봅니다. 리스트 대신, 교수들의 상태를 밀집 텐서(dense tensor), 즉 다차원 격자로 봅니다. 만약 10명의 교수가 있다면, Tessa는 59,049개의 항목을 가진 리스트를 만드는 대신, 각 변의 길이가 3인 10차원 큐브를 만듭니다. 이는 루빅스 큐브와 같지만, 3개의 층 대신 10개의 층이 있는 형태입니다.

이것이 왜 멋질까요? 현대의 그래픽 카드(GPU)가 바로 이러한 큐브를 처리하도록 설계되었기 때문입니다. GPU는 수백만 개의 숫자에 대해 동일한 수학 연산을 동시에 수행하도록 만들어졌습니다. Tessa는 교수의 규칙("만약 ~라면" 식의 마르코프 체인 로직)을 이 큐브를 위한 일련의 명령어로 번역합니다. 미로를 한 단계씩 걸어가는 대신, Tessa는 GPU에게 이 큐브 전체를 한꺼번에 "찌그러뜨리라"고 명령합니다.

"컴파일러"의 마법
논문은 Tessa가 JAX라는 도구와 XLA라는 컴파일러를 사용한다는 점을 강조합니다. JAX를 교수의 규칙을 GPU가 유창하게 구사하는 언어로 바꿔주는 번역가라고 생각하고, XLA를 GPU가 음악을 가장 효율적으로 연주하도록 지시하는 지휘자라고 생각하십시오. XLA는 많은 작은 단계들을 하나의 크고 부드러운 움직임으로 융합하여, GPU가 멈추고 다시 시작하며 시간을 낭비하지 않게 합니다. 이것이 Tessa가 빠른 이유입니다. 하드웨어와 싸우는 대신 하드웨어와 함께 춤을 추기 때문입니다.

결과: 시간 가속화
연구진은 세 가지 유명한 "어려운" 문제들을 대상으로 Tessa를 테스트했습니다:

1. 큐(Queues): 10개의 서로 다른 대기 줄을 상상해 보십시오. Tessa는 차세대 도구보다 100배 이상 빨랐습니다.
2. 날씨 공장(Weather Factories): 날씨에 따라 공장이 가동되거나 파업하는 모델입니다. 여기서도 Tessa는 100배 이상 빨랐습니다.
3. 헤르만 프로토콜(Herman's Protocol): 프로세서들이 리더를 합의하려고 노력하는 고전적인 문제입니다. 여기서 Tessa는 500단계 앞을 내다보는 테스트에서 경쟁 도구보다 300배 이상 빨랐습니다.

논문은 또한 한계점에 대해서도 매우 명확히 밝히고 있습니다. Tessa는 모든 문제를 해결하는 만능 해결사가 아닙니다. 시스템이 매우 희소하다면(빈 공간이 많고 연결이 적다면), 전통적인 도구들이 메모리를 덜 사용하기 때문에 여전히 더 나을 수 있습니다. Tessa는 시스템이 "밀집"되어 있을 때, 즉 모든 것이 서로 연결되어 거대한 가능성의 웹을 형성할 때 빛을 발합니다.

검증을 넘어: 완벽한 설정 찾기
Tessa가 할 수 있는 또 다른 멋진 기능이 있습니다. 문제를 매끄러운 수학적 함수(텐서 프로그램)로 변환하기 때문에, **경사 하강법(gradient descent)**을 사용할 수 있습니다. 이는 AI가 고양이를 인식하거나 자동차를 운전하도록 훈련하는 데 사용되는 것과 동일한 수학입니다. 즉, Tessa는 시스템이 제대로 작동하는지 확인할 뿐만 아니라, 시스템이 제대로 작동하게 만들기 위한 완벽한 설정을 탐색할 수도 있습니다.

논문에서 연구진은 이를 "Knuth-Yao 주사위 굴리기" 문제에 사용했습니다. 그들은 두 동전의 편향값($p$와 $q$)을 조정하여 컴퓨터가 공정한 주사위를 굴리게 만들고자 했습니다. Tessa는 동전의 편향을 조절할 수 있는 '노브(knob)'로 취급했습니다. Tessa는 노브를 바꿀 때 결과가 어떻게 변하는지 계산한 다음, 오차를 최소화하도록 자동으로 노브를 조정했습니다. 단 몇 초 만에 완벽한 값($p=0.5, q=0.5$)을 찾아냈으며, 이는 Tessa가 검증뿐만 아니라 최적화에도 사용될 수 있음을 보여주었습니다.

결론
이 논문은 문제를 표현하는 방식(희소한 리스트에서 밀집된 텐서로)을 바꿈으로써 현대 하드웨어의 강력한 힘을 끌어낼 수 있음을 증명합니다. 이는 "모래알 하나하나를 세는 것"에서 "불도저를 사용하여 해변 전체를 한꺼번에 옮기는 것"으로의 전환입니다. 비록 상태 폭발 문제(상태의 수가 여전히 기하급수적으로 증가하는 문제) 자체를 해결하는 것은 아니지만, 우리가 해결할 수 있는 경계를 훨씬 더 멀리 밀어붙여, 이전에는 검증이 불가능했던 시스템을 검증할 수 있게 만듭니다. 저자들은 자신들의 수학적 근거(건전성을 증명함)와 결과(실제 벤치마크로 측정함)에 확신을 가지고 있으며, 컴퓨터 과학자들의 도구 상자에 강력한 새 도구를 제공합니다.