형식 검증으로 코드 최적화하는 AI 'Maxwell' 공개

핵심 요약

• doubleAI가 프로그램 실행 중 코드를 동적으로 최적화하는 '코드 실행 모델(CEM)' Maxwell을 공개했다.
• Maxwell은 실행 중인 프로그램의 병목을 감지하고 알고리즘 전체를 재작성해 더 빠른 바이너리를 생성하며, 생성된 코드는 원본과 의미적으로 완전히 동등함을 형식 검증으로 증명한다.
• 기존 JIT 컴파일러나 최적화 도구와 달리 Maxwell은 실제 하드웨어와 데이터 흐름에 맞춰 함수와 알고리즘 수준의 전체 변환을 수행하고 조건에 따라 보호 조항을 둔다.
• 형식 검증의 핵심은 두 프로그램이 모든 입력에서 같은 결과를 내고 같은 부작용을 일으킨다는 것을 수학적으로 증명하는 것이며, Maxwell은 Python을 포함한 동적 언어를 완전히 형식화했다.
• Python의 동적 특성(런타임 중 타입 변경, 연산자 재정의 등)을 포함해 실제 프로그램의 파일 통신 등 일반적 코드까지 형식화 범위에 포함시켰다.
• Maxwell의 증명은 재사용 가능한 '증명 가젯'과 조합 가능한 증명 구조로 구성되어 인간이 수동으로 하기에는 지루한 작업을 AI가 자동화한다.
• Maxwell은 CPU와 GPU 코드 모두를 처리해, Python 코드를 저수준 SIMD 구현으로, PyTorch 코드를 GPU별 최적화 커널로 변환한다.
• 프로그램 실행 맥락(메모리 크기, 데이터 패턴 등)을 관찰해 코드를 특화할 수 있으며, 전제 조건 변화 시 원본 코드로 복귀하는 가드를 둔다.
• Maxwell은 '자기 개선 코드'를 제공하는데, 한 번 증명된 최적화 버전이 다음 최적화의 시작점이 되어 프로그램이 실행되는 동안 계속 빨라진다.
• 코딩 AI(Claude Code 등)는 코드를 작성하고 Maxwell은 그것을 하드웨어에서 최적으로 실행하도록 하는 상호 보완 역할을 한다.
• 형식 검증 덕분에 일반 컴파일러나 인간 엔지니어가 위험해할 변환까지 수행할 수 있으면서도 정확성을 보장한다.
• Maxwell은 런타임에 병목을 감지해 코드를 추출하고, 핫 패스를 느리게 하지 않으면서 최적화를 적용하는 복잡한 엔지니어링을 수행한다.
• 전 세계 인터넷 규모로 모든 기계에서 실행되며, 전 지구적으로 실행 중인 코드를 최적화해 컴퓨팅 자원을 절약할 수 있다.