Lumos는 언어 모델 시스템(LMS) 동작을 지정하고 공식적으로 인증하기 위한 최초의 원칙적 프레임워크입니다. 그래프를 기반으로 하는 명령형 확률적 프로그래밍 DSL로, LMS를 위한 독립적이고 동일하게 분포된 프롬프트를 생성하는 구문을 포함합니다. Lumos는 그래프를 통해 프롬프트 분포의 구조화된 뷰를 제공하며, 샘플링된 하위 그래프에서 임의의 프롬프트를 형성합니다. 통계적 인증자와의 통합을 통해 임의의 프롬프트 분포에 대한 LMS 인증을 지원합니다. Lumos는 하이브리드(운영 및 지시적) 의미론을 제공하여 사양을 엄격하게 해석할 수 있도록 합니다. Lumos는 소수의 구성 가능한 구성 요소만 사용하여 복잡한 관계형 및 시간적 사양을 포함한 기존 LMS 사양을 인코딩할 수 있습니다. 또한 새로운 속성을 지정하는 것을 용이하게 합니다. 자율 주행 시나리오에서 시각-언어 모델(VLM)에 대한 최초의 안전성 사양을 제시합니다. Lumos를 사용하여 개발했습니다. 이를 통해 최첨단 VLM Qwen-VL이 심각한 안전 실패를 보이며, 비가 오는 운전 조건에서 우회전 시나리오에서 최소 90% 확률로 부정확하고 안전하지 않은 응답을 생성하여 상당한 안전 위험을 드러냄을 보여줍니다. Lumos의 모듈식 구조는 사양의 쉬운 수정을 가능하게 하여 LMS 인증이 빠르게 변화하는 위협 환경에 발맞추도록 합니다. Lumos로 작성된 사양 프로그램은 최첨단 LMS가 나타내는 특정 실패 사례를 찾는 데 도움이 됩니다. Lumos는 LMS 동작을 지정하고 인증하기 위한 최초의 체계적이고 확장 가능한 언어 기반 프레임워크로, LMS 인증의 광범위한 채택을 위한 길을 열었습니다.