모든 사고하는 것들
"우리가 원하는 것은 경험으로부터 배울 수 있는 기계입니다. 기계가 자체 지침을 변경할 수 있게 하는 가능성은 이를 위한 메커니즘을 제공합니다." — Alan Turing, London Mathematical Society, 1947년 2월
1952년 Alan Turing는 동료 Alick Glennie와 체스 게임을 했습니다. 그는 컴퓨터 역할을 맡아 플레이했습니다. 그는 몇 장의 종이에 체스 프로그램을 작성했고, 매 차례마다 프로그램의 지침을 한 글자도 빠짐없이 따라 움직임을 만들어냈습니다. 매 수에 약 반 시간이 걸렸습니다. 그는 패배했습니다.
그 게임 내내 Alan은 컴퓨터가 하는 일을 정확히 했습니다. 아무리 명백한 개선이 필요해 보였더라도, 그는 프로그램을 충실하게 수행했으며 한 줄도 개선하지 않았습니다.
곧이어 기계들이 등장했습니다. 그리고 프로그래밍은 그 이후로 계속 이어져 온 노동 분담 체제로 자리 잡았습니다. 인간은 프로그램이 정확히 무엇을 해야 하는지 결정하고 작성합니다. 그런 다음 컴퓨터가 그것을 지침 하나하나, 초당 수십억 번에 걸쳐, 쓰인 그대로 실행합니다. 모든 사고는 프로그램이 실행되기 전에 일어나지만, 그 과정 중이나 후에 일어나는 것은 전혀 없습니다.
지난 몇 년 동안 AI가 이 영역에 합류했습니다. 이제 AI 모델은 프로그래머와 함께 코드를 초안 작성하고 있으며, 11월의 특이점 이후로는 점점 더 그러합니다. 하지만 그들이 작성하는 코드는 여전히 동일한 컴퓨터로 전달되어, Turing가 체스 프로그램으로 했던 것과 매우 유사하게 기계적이고, 결정론적이며, 생각 없이 실행됩니다.
그렇다면 AI는 지금까지 왜 단지 코드를 작성하는 것을 돕는 역할에만 머물렀고, 그것을 실행하는 것을 돕지는 못했을까요?
만약 튜링이 보드 위에서 본 것을 바탕으로 행동할 수 있었다면, 매수마다 자신의 프로그램을 개선할 수 있었을 것이고, 그때마다 조금씩 더 잘 플레이했을 것이다. 이와 유사하게, 모든 컴퓨터 코드 조각은 그것이 실행되는 환경과 조건에 대한 완전한 “맥락적 지식”, 그리고 그를 통해 흐르는 데이터의 흐름과 결합되어 가속화되거나, 적은 자원을 사용하도록 만들거나, 또는 달리 개선될 수 있다.
doubleAI는 바로 이 작업을 수행하기 위해 새로운 범주의 모델을 구축했다.
우리는 이를 코드 실행 모델(code execution models), 또는 CEMs라고 부른다. CEMs는 인공지능을 이전에는 없었던 곳에 배치한다: 코드와 실리콘 사이. CEMs는 코드를 작성하는 모델과는 완전히 다른 제약 조건 하에서 작동한다. CEM은 실행 중인 프로그램 내부에 존재하며, 그를 통과하는 데이터 흐름을 관찰하고 진행하면서 알고리즘과 명령어를 재구성한다. 출력물은 이진 파일(binary)이며, 하드웨어에서 직접 실행된다. 인간의 개입이 없다. 따라서, 모델은 절대 오류가 나서는 안 된다. 현재까지 어떤 AI도 그 약속을 한 적이 없다. 우리가 어떻게 그렇게 하는지 계속 읽어보라.
증명, 수학, 그리고 코드
최근 형식 검증(formal verification)¹이 수학에 혁명을 일으켰다. Anthropic은 페르마의 마지막 정리(Fermat's Last Theorem)에 대한 완전한 1,300만 줄 분량의 형식적 증명을 발표했다.² Anthropic의 증명이 나온 지 사흘 만에 OpenAI는 천 년 문제 중 하나인 나비에-스토크스 방정식(Navier–Stokes equations)에 대한 유한 시간 폭발 결과(finite-time blow-up result)를 또다시 완전한 형식적 증명과 함께 발표했다. 그 이후로도, 중요한 결과에 대한 AI 작성 형식적 증명이 눈부신 속도로 등장하고 있다. 수학 자체가 재창조되고 있는 것처럼 보인다.
이것은 질문을 제기한다: 소프트웨어에도 같은 것이 가능한가? CEM에게 이 질문은 매우 중요하다. 결국, CEM은 인간 검토자 없이 매일 여러 번 실행되는 프로그램을 진화시키기 때문이다. 설령 시간이 충분하더라도, 단순 반복 테스트만으로는 불충분하다. 이것을 안전하게 수행하려면 무엇이 필요할까?
답은 수학을 새롭게 만들고 있는 바로 그 도구, 즉 *정형 검증(formal verification)*입니다. 첫 단계는 코드를 *정형화(formalise)*하는 것으로, 기계가 추론할 수 있도록 정확한 수학적 의미를 부여하는 것입니다. 그 이후부터는 코드의 동작 방식에 대한 어떤 질문이든 증명을 통해 해결될 수 있습니다.
저희가 얼리 액세스로 출시하는 첫 번째 CEM은 Maxwell’s Daemon³이라고 불리며, 좀 더 비공식적으로는 Maxwell입니다. 이 목표는 *슈퍼 최적화(superoptimisation)*입니다. 즉, 눈앞의 기계에서 코드 조각을 실행할 수 있는 가장 빠른 방법을 찾는 것입니다. Maxwell은 기존 코드를 가져와 프로그램이 실행되는 동안 알고리즘과 기계 명령어를 수정하며 새로운 바이너리 코드를 방출합니다. 이는 주석 처리 컴파일러(just-in-time compiler)가 하는 것과 유사하지만, 새로운 알고리즘의 형태에 있어서는 훨씬 더 많은 자유도를 가집니다.⁴ Maxwell이 대체하는 모든 것은 이전 코드가 가진 의미론적 동등성(semantically equivalent)을 정확히 유지해야 합니다.
결정적으로, 소스 코드에는 아무것도 변경되지 않습니다. 오히려 변화하는 것은 그 아래에서 실행되는 것들입니다. 즉, 자신이 대체하는 코드와 정확하게 동등함이 증명된 훨씬 빠른 바이너리가 됩니다. 프로그램이 실행되는 동안 Maxwell은 병목 지점(bottlenecks)과 그것이 표현되는 방식을 식별합니다. 발견한 각 병목 지점에 대해 Maxwell은 해당 기계에 맞춰 조립된 새로운 버전을 만듭니다. 소스 코드는 작성자가 인간이든 Claude Code와 같은 코딩 에이전트이든 상관없이 정확히 원래대로 유지됩니다. 따라서 Maxwell은 코딩 에이전트의 보완재입니다. 그들이 프로그램을 작성하면, Maxwell이 기계가 최적으로 실행되도록 만듭니다.
Maxwell에게 정형 검증이란 *의미론적 동등성에 대한 정형 증명(formal proofs of semantic equivalence)*의 형태를 취합니다.
두 프로그램이 의미론적으로 동등하다는 것은, 동일한 입력을 받았을 때 항상 같은 결과를 산출하고 주변 세계에 미치는 영향(effect)이 같다는 것을 의미합니다. 두 프로그램은 외관상 전혀 다를 수 있습니다. 하나는 몇 줄의 Python 코드일 수 있고 다른 하나는 Rust나 C 코드가 될 수도 있습니다. 중요한 것은, 아무리 노력해도 사용하는 사람이 이 둘을 구별할 수 없어야 한다는 것(물론, 어느 쪽이 훨씬 효율적인지는 제외하고)입니다. 동등성의 형식적 증명은 모든 가능한 입력과 모든 가능한 시나리오에 대해 한 번에 이를 확립하며, 기계가 모든 단계를 확인할 만큼 충분히 정밀한 언어로 작성됩니다.⁵
원본 (Original)
deforiginal(n): s = 0 for i in range(n): for j in range(i): s += 1 return s
대체 (Replacement)
fnreplacement(n: i64) -> i64 { n * (n - 1) / 2 }
동등성 증명 (Proof of equivalence)
requires n : int 0 ≤ n ≤ 3037000500 theoremoriginal(n) =replacement(n) by induction on n case 0:original(0) = 0 =replacement(0) case n + 1:original(n + 1) =original(n) + n = n(n − 1)/2 + n = (n + 1)n/2 =replacement(n + 1) ∎
프로그램과 증명 사이에는 *커리-하워드 대응성(Curry–Howard correspondence)*으로 알려진 깊고 잘 알려진 연결 고리가 있습니다. 본질적으로, 증명은 프로그램이며, 증명을 확인하는 것은 그 프로그램이 올바르게 구성되었는지 확인하는 것과 같습니다. 더 구체적으로 말하면, 대부분의 프로그래밍 언어는 *타입(types)*에 의해 뒷받침되는데, 이는 값이 어떤 “종류의 것”인지를 설명합니다 (예를 들어, 숫자나 텍스트 조각). 이 대응성은 타입이 수학적 명제를 설명하는 데 똑같이 사용될 수 있으며, 그 타입을 가진 값을 산출하는 프로그램은 곧 그 명제의 증명이 된다는 것을 관찰합니다. 비슷한 방식으로, 이 대응성을 통해 보조정리(lemma)는 작은 함수가 되고, 보조정리로 구성된 정리는 그것들을 호출하는 더 큰 프로그램이 됩니다. 그러면 증명을 확인하는 것은 단순히 프로그램을 타입 체크하는 것 이상이 아닙니다. 이것이 바로 *타입 이론(type theory)*이며 (간단히 말해), 대부분의 현대적인 증명 검사기가 구축되는 기반 메커니즘입니다.
doubleAI에서 우리는 형식적으로 검증된 코드에 대한 여러 돌파구를 마련했습니다.
이러한 돌파구 중 하나는 가장 역동적인 언어 중 하나인 Python 프로그래밍 언어를 완전히 형식화(formalisation)했다는 점입니다.
Python을 형식화하기가 왜 그렇게 어려울까요? Python에서는 한 줄에서 다음 줄로 값이 타입을 바꿀 수 있습니다. 사실, Python은 너무 동적이라서 무엇이 숫자이고, 두 숫자를 더한다는 것이 무슨 의미인지와 같은 기본적인 원리조차 프로그램 실행 중에 완전히 재정의될 수 있습니다. 이러한 동적인 특성이 바로 Python을 매력적인 프로그래밍 생태계로 만드는 부분입니다.
저희의 형식화는 이 모든 동작을 고려합니다. 이는 전통적으로 형식 방법(formal methods)이 제한되어 왔던 작고 독립된 함수들만을 다루지 않습니다. 오히려, 통신을 수행하거나 파일을 사용하는 등의 실제 세계에 존재하는 일반적인 범용 Python 코드를 포괄합니다. Python이 형식화됨으로써, 특정 Python 코드 조각과 그 재작성 버전이 일치한다는 주장을 공식적으로 작성하고 증명할 수 있게 됩니다.
Maxwell이 매우 강력한 이유 중 일부는 doubleAI에서 이 형식 시스템 내에서 작동하도록 훈련되었다는 점입니다. 새로운 코드를 작성할 때마다 그것의 의미적 동등성(semantic equivalence)에 대한 형식적인 증명을 함께 작성합니다.
이러한 증명들을 작성하는 것은 엄청난 작업처럼 들릴 수 있습니다. 사람에게는 그럴 것입니다. Maxwell은 사람이 아닙니다. 그 증명들은 주로 재사용 가능한 *증명 가젯(proof gadgets)*들로 구성되며, 각 가젯은 단 한 번만 증명됩니다. 또한 증명들은 조합 가능하기 때문에 전체 단위에 대한 증명이 여러 작은 증명들로부터 조립될 수 있습니다. 남는 것은 세심하고 지루한 작업이며, 이는 AI가 인간을 훨씬 능가하는 바로 그 종류의 작업입니다.
Maxwell은 CPU와 GPU 코드 모두를 처리합니다. Python 코드는 낮은 수준의 베어메탈 최적화된 코드(예: 관련성이 있는 곳에서의 직접적인 SIMD 구현 포함)로 교체됩니다. PyTorch 코드 역시 장치에 있는 특정 GPU를 위한 고도로 최적화된 커널로 대체됩니다. 이러한 최적화는 광범위하며 Python 생태계 전반의 훨씬 더 많은 움직이는 부분들을 포괄합니다.
최적화의 핵심 동인 중 하나는 프로그램이 어떻게 실행되는지에 대한 문맥 정보입니다. 이를 통해 Maxwell은 실제로 관찰한 내용에 맞춰 코드를 특화할 수 있으며, 물론 가정된 전제 조건 중 어떤 것이 변경되었을 경우에도 방어합니다. 모든 가속에는 기계 검증 증명이 수반되기 때문에, Maxwell은 과감하게 접근하여 컴파일러나 인간 엔지니어라면 감히 시도하지 못했을 변환까지 수행할 수 있으며, 그 정확성을 항상 보장받습니다.
Maxwell 같은 CEM을 구축하는 것은 상당한 공학적 노력을 필요로 합니다. Maxwell은 런타임에 매끄럽게 통합되어 병목 현상을 감지하고 전체 코드를 가속해야 하며, 이 모든 과정에서 '핫 패스(hot path)'의 속도를 저하시키지 않아야 합니다. 각각이 하나의 이야기가 될 수 있지만, 아마도 다른 날로 미루는 것이 가장 좋을 것 같습니다.
Maxwell: 기계를 위한 에이전트
지금까지 소프트웨어 분야의 AI는 프로그래머를 위해 작동하여 요청에 따라 코드를 작성한 후 자리를 비켜주는 방식이었습니다. 하지만 Maxwell은 코드와 함께 살아갑니다. 프로그램이 실행되는 동안, 해당 프로그램이 구동되는 기계를 대신하여 작동합니다. 이는 프로그램이 올라간 하드웨어와 그 사이를 흐르는 데이터의 정확한 형태 및 타입을 파악하고, 이들이 변할 때마다 코드를 지속적으로 맞춰나갑니다.
Maxwell이 특정 코드에 대해 더 빠른 버전을 증명하면, 그 버전은 다음 시도의 출발점이 되며, 소스 코드는 작성자가 남겨둔 그대로 유지되는 동안 프로그램의 속도는 계속 빨라집니다. 우리는 이것을 자체 개선(self-improving) 코드라고 생각합니다. Maxwell은 이를 자신이 구동되는 모든 기기에 인터넷 규모로 가져올 수 있습니다.
우리는 이것이 어떤 단일 프로그램을 넘어선 영역에서 중요하다고 생각합니다. 컴퓨팅 파워는 전 세계적으로 가장 부족한 자원 중 하나가 되었으며, 그 많은 부분이 충분히 빠르게 실행될 수 있음에도 불구하고 느리게 코드를 구동하는 데 사용됩니다. Maxwell이 가속화하는 모든 프로그램은 이 부족한 자원의 일부를 돌려줍니다. Maxwell은 곧 얼리 액세스로 제공될 예정입니다. Maxwell로 가득 찬 세상이 어떤 모습일지 매우 기대됩니다.
1952년, Turing은 자신의 프로그램에 쓰인 대로 정확하게 따라야 했습니다. 이제 우리의 기계는 더 이상 그럴 필요가 없습니다.
¹ 형식 검증(Formal verification)이란 컴퓨터가 모든 단계를 확인할 수 있을 만큼 정밀한 언어로 증명을 작성하는 관행입니다.
² 이 증명은 Anthropic의 AI 에이전트들이 11일 동안 작성했습니다. 이 정리를 공식화하는 것은 이전에는 2024년에 최고 수준의 인간 수학자 그룹이 시작한 5년간 공공 자금 지원 프로그램의 목표였습니다.
³ James Clerk Maxwell이 1867년에 상상했던 작은 생명체처럼, 가스의 분자를 단순히 정렬함으로써 엔트로피를 낮추는 존재 말입니다. 우리의 Maxwell은 코드에 같은 종류의 질서를 가져와 하드웨어, 데이터 및 사용 방식에 맞게 조정합니다.
⁴ 컴파일러나 torch.compile, PyPy와 같은 즉시 컴파일러(just-in-time compilers)는 엔지니어들이 사전에 작성한 변환에 한정되며, STOKE와 같은 슈퍼 최적화기(superoptimisers)는 기계어 코드의 짧고 루프가 없는 조각에 대해 단 한 번, 정적으로만 최적화합니다. Maxwell은 실제 프로그램이 실행되는 동안 전체 함수, 알고리즘을 포함하여 재작성합니다. 이는 각 버전을 정확한 하드웨어와 프로그램 흐름을 통해 실제로 흐르는 데이터에 맞게 조정하고, 변화가 생길 때마다 계속해서 재최적화하며, 테스트하는 대신 모든 코드 조각이 동등함을 증명합니다.
