[2512.02966] Lumos: Let there be Language Model System Certification

Computer Science > Programming Languages arXiv:2512.02966 (cs) [Submitted on 2 Dec 2025 (v1), last revised 31 Mar 2026 (this version, v2)] Title:Lumos: Let there be Language Model System Certification Authors:Isha Chaudhary, Vedaant Jain, Prineet Parhar, Kavya Sachdeva, Avaljot Singh, Sayan Ranu, Gagandeep Singh View a PDF of the paper titled Lumos: Let there be Language Model System Certification, by Isha Chaudhary and 6 other authors View PDF Abstract:We introduce the first principled framework, Lumos, for specifying and formally certifying Language Model System (LMS) behaviors. Lumos is an imperative probabilistic programming DSL over graphs, with constructs to generate independent and identically distributed prompts for LMS. It offers a structured view of prompt distributions via graphs, forming random prompts from sampled subgraphs. Lumos supports certifying LMS for arbitrary prompt distributions via integration with statistical certifiers. We provide hybrid (operational and denotational) semantics for Lumos, providing a rigorous way to interpret the specifications. Using only a small set of composable constructs, Lumos can encode existing LMS specifications, including complex relational and temporal specifications. It also facilitates specifying new properties - we present the first safety specifications for vision-language models (VLMs) in autonomous driving scenarios developed with Lumos. Using these, we show that the state-of-the-art VLM Qwen-VL exhibits critical ...