doubleAI, 형식 검증 기반 런타임 바이너리 최적화 모델 Maxwell 공개

• doubleAI가 얼리 액세스를 시작한 코드 실행 모델(CEM) Maxwell을 발표함. 프로그램 실행 중 하드웨어와 데이터 흐름을 분석해 바이너리를 실시간으로 재작성함.
• 테스트에 의존하지 않고 형식 검증(formal verification)을 통해 원본 소스와 최적화 바이너리의 의미적 동치성을 증명해 정확성을 보장함.
• 벤치마크 결과 LTX-2.5 4K 영상 생성에서 1.86배 속도 향상을 기록함. 2개의 B200 GPU 환경에서 처리 시간을 249.4초에서 133.9초로 단축함.
• 동적 Python 기능의 형식화를 구현해 범용 Python 코드를 저수준 SIMD 또는 GPU 전용 커널로 최적화 가능함.

Technical Mechanism

• 코드와 실리콘 사이에서 작동하며, 명령어 수준이 아닌 함수 수준에서 알고리즘과 지시문을 재구성함.
• 재사용 가능한 'proof gadgets'를 활용해 모든 가능한 입력과 시나리오에 대한 동치성 증명을 구성함.
• 런타임 컨텍스트의 가정이 변경되면 원본 코드로 제어권을 반환하는 가드 메커니즘을 포함함.

Performance Details

• Blackwell 아키텍처에서 Maxwell은 하루 탐색 후 SOL-ExecBench 커널의 90%에서 NVIDIA PyTorch 베이스라인을 초과함.
• NVIDIA cuGraph의 하이퍼 최적화된 드롭인 버전을 독립적으로 생성 및 검증해 평균 3.6배 속도 향상을 달성함.
• LTX-2.5에서는 GPU 통신량을 부분 출력 기준 262 MB에서 1 MB로 줄이고, 디코더 커널 실행 횟수를 절반으로 줄이면서 동일한 시각적 품질을 유지함.