Vosti: 결정론적 LLM 추론 명세화, 구현 및 검증

LLM 추론 시스템은 배치 구성(batch composition), 프롬프트 청킹(prompt chunking), 프리필/디코드 실행(prefill/decode execution), KV-캐시 재사용(KV-cache reuse), 제거(eviction) 또는 재계산(recomputation) 등 다양한 방식으로 달라질 수 있습니다. 이러한 최적화는 시스템 출력에 영향을 미치지 않아야 합니다. vLLM의 배치 불변 모드(batch-invariant mode)나 SGLang의 결정론적 모드(deterministic mode)를 포함한 프로덕션 시스템들은 이 목표를 추구하지만, 공식적인 시스템 수준 명세가 부족합니다. 우리는 결정론적 LLM 추론을 형식화했습니다: 고정된 모델과 배포 구성 하에서, 동일한 프롬프트와 초기 샘플러 상태를 가진 요청은 실행 간에 대응하는 출력 위치에서 비트 단위로 동일한 로짓(logits)을 생성해야 합니다. 우리의 테스트 결과, 이러한 프로덕션 모드들은 일부 실행 변화 조건 하에서 다른 로짓을 생성한다는 것을 발견했습니다. 이 한계를 해결하기 위해, 우리는 이 명세에 맞춰 설계 및 검증된 추론 엔진인 Vosti를 제시합니다. Vosti는 런타임 엔진 상태와 독립적으로 커널(kernels)을 선택하고 캐시된 KV 값들을 해당 논리적 토큰 접두사(logical token prefixes)에 연결합니다. 그 증명은 엔진/GPU 커널 경계에서 분해됩니다: Verus 귀납 증명(inductive proof)은 스케줄링과 페이지 기반의 접두사 공유 KV-캐시가 출력 로짓을 보존한다는 것을 확립하고, Triton 분석기(analyzer)는 배치, 쿼리 길이 및 페이지 기반 KV-캐시 레이아웃 전반에 걸쳐 비트 단위로 동일한 선택된 커널 출력을 증명합니다. Vosti는 테스트된 모든 실행 변화 조건에서 비트 단위로 동일한 로짓을 생성하며, 디코드 중심 워크로드(decode-heavy workloads)에서 vLLM의 배치 불변 모드와 비교 가능한 성능을 달성하면서도 더 강력하고 형식적으로 검증된 결정론 보장을 제공합니다.