1952년 앨런 튜링은 동료와 체스를 두면서 종이에 적은 프로그램의 지시를 한 수 한 수 그대로 따랐다. 더 나은 수가 보여도 자신이 쓴 명령을 고치지 않고 기계처럼 충실히 실행했을 뿐이다. 이 장면은 이후 수십 년간 굳어진 소프트웨어의 분업 구조를 상징한다. 사람(혹은 최근에는 AI)이 프로그램이 무엇을 해야 하는지 정해 코드로 적고, 컴퓨터는 그것을 적힌 그대로 초당 수십억 번 기계적으로 수행한다. 사고는 실행 이전에만 일어나고 실행 도중이나 이후에는 일어나지 않는다.
doubleAI가 공개를 예고한 '맥스웰'(Maxwell's Daemon)은 바로 이 지점을 겨냥한다. 회사는 이를 코드 작성 모델과 구분해 '코드 실행 모델(Code Execution Model, CEM)'이라는 새로운 범주로 부른다. 코드를 작성하는 AI가 결과물을 넘기고 물러서는 것과 달리, 맥스웰은 실행 중인 프로그램 안에 머물며 데이터 흐름을 관찰하고 알고리즘과 기계 명령을 바꿔 새로운 바이너리를 내보낸다. JIT 컴파일러와 비슷하지만, 미리 정해진 변환만 적용하는 컴파일러와 달리 함수와 알고리즘 자체를 실행 시점에 다시 짠다는 점이 다르다.
소스는 그대로, 아래서 돌아가는 코드가 바뀐다
핵심은 소스 코드를 건드리지 않는다는 점이다. 개발자가(또는 코딩 에이전트가) 작성한 소스는 그대로 두고, 그 아래에서 실제로 실행되는 바이너리만 더 빠른 버전으로 교체된다. 맥스웰은 프로그램이 돌아가는 동안 병목을 찾아내고, 지금 올라가 있는 바로 그 하드웨어에 맞춰 새 버전을 조립한다. CPU와 GPU 코드를 모두 다루며, 파이썬 코드는 SIMD 같은 저수준 구현으로, 파이토치 코드는 해당 GPU에 맞춘 커널로 바꾼다. 회사는 이 방식으로 LTX의 영상 생성 모델 LTX-2.5가 동일한 출력으로 4K 영상을 거의 두 배 빠르게 생성했다고 밝혔다.
이 구조가 가능하려면 치환된 코드가 원본과 의미상 완전히 같아야 한다. 겉모습은 전혀 달라도, 같은 입력에 대해 항상 같은 결과를 내고 외부 세계에 같은 효과를 미쳐야 한다는 뜻이다. 사람이 실행 루프 안에 없는 상태에서 하루에도 여러 번 코드가 바뀌므로, 테스트만으로는 안전을 담보할 수 없다.
안전장치는 '형식 검증'
맥스웰이 내세우는 답은 형식 검증(formal verification)이다. 코드에 기계가 추론할 수 있는 정확한 수학적 의미를 부여한 뒤, 교체 전후 코드가 모든 입력과 모든 상황에서 동등함을 증명으로 확정한다. doubleAI는 이를 위해 동적 특성이 강해 형식화가 까다로운 파이썬 전체를 형식화했다고 설명한다. 파이썬은 변수의 타입이 줄마다 바뀌고, 숫자가 무엇인지나 덧셈의 의미조차 실행 중 재정의될 수 있는데, 이런 동작까지 포괄했다는 것이다. 통신이나 파일 입출력을 하는 실제 범용 코드도 대상이라고 한다.
증명 작성은 사람에게는 막대한 노동이지만, 맥스웰의 증명은 한 번만 증명해 두고 재사용하는 '증명 가젯'을 조합해 만들어진다. 작은 증명들을 합쳐 전체 단위의 증명을 조립하는, 지루하지만 AI가 사람보다 월등히 잘하는 작업이라는 설명이다. 모든 가속에 기계가 검증한 증명이 붙기 때문에, 컴파일러나 엔지니어가 위험해서 손대지 못할 과감한 변환도 정확성을 확신하며 시도할 수 있다는 것이 회사의 주장이다. 한 번 더 빠른 버전이 증명되면 그것이 다음 최적화의 출발점이 되어, 소스는 그대로인 채 프로그램이 돌아가는 내내 계속 빨라지는 '자기 개선 코드'가 된다.
실무자가 따져봐야 할 지점
국내 실무자 입장에서 매력은 분명하다. 소스를 고치지 않고 런타임에서 하드웨어와 데이터 분포에 맞춰 성능을 끌어올린다면, 코딩 에이전트와 상호 보완적으로 쓸 수 있고 연산 비용이라는 희소 자원을 아낄 수 있다. 다만 아직 얼리 액세스 예고 단계이고, 회사가 제시한 여러 근거는 독립적으로 검증되지 않았다는 점을 분명히 할 필요가 있다. 소스가 거론한 페르마의 마지막 정리나 나비에-스토크스 관련 성과, 'AI 특이점' 같은 서술은 회사 측 서사에 담긴 주장으로, 사실 여부를 그대로 받아들이기보다 참고로 두는 편이 안전하다.
기술적 한계도 명시돼 있다. 라이스 정리에 따르면 임의의 두 프로그램의 의미적 동등성을 판정하는 보편적 알고리즘은 존재하지 않는다. 회사는 이것이 보편 절차에 대한 한계일 뿐 눈앞의 특정 쌍에 대해서는 대개 증명을 적어낼 수 있다고 반박하지만, 이는 곧 모든 코드가 항상 최적화 대상이 되지는 않는다는 의미이기도 하다. 또한 관찰된 실행 조건을 전제로 코드를 특수화하는 방식인 만큼, 전제가 바뀌는 상황에 대한 방어 로직이 실제 환경에서 얼마나 견고하고 얼마만큼의 오버헤드를 남기는지는 공개 이후 직접 확인해야 할 대목이다. 실행 중 AI가 코드를 바꾼다는 개념 자체가 디버깅과 감사, 재현성 측면에서 운영 조직에 새로운 질문을 던진다는 점도 함께 고려할 문제다.