Lumos: Let there be Language Model System Certification

TL;DR

Lumos introduces a principled framework for specifying and certifying LMS behaviors using an imperative probabilistic DSL over text-rich graphs. It provides hybrid semantics (operational and denotational) and native support for IID sampling from subgraphs, enabling probabilistic certification of diverse properties across LLMs and VLMs. The paper demonstrates expressiveness by encoding temporal, relational, and domain-knowledge specifications and designs new VLM safety tests for autonomous driving, revealing significant safety gaps in state-of-the-art models. Its modular graph-based approach separates symbolic scenario logic from domain execution, enabling rapid adaptation to evolving threats and straightforward extraction of failure cases from execution traces. The authors also provide a public implementation, underscoring Lumos as a scalable, extensible pathway toward broader LMS certification.

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 safety failures, producing incorrect and unsafe responses with at least 90% probability in right-turn scenarios under rainy driving conditions, revealing substantial safety risks. Lumos's modular structure allows easy modification of the specifications, enabling LMS certification to stay abreast with the rapidly evolving threat landscape. We further demonstrate that specification programs written in Lumos enable finding specific failure cases exhibited by state-of-the-art LMS. Lumos is the first systematic and extensible language-based framework for specifying and certifying LMS behaviors, paving the way for a wider adoption of LMS certification.

Figures (9)

• Figure 1: Question graph and multi-turn LLM conversation using a sampled graph path wang2025quantifyingrisksmultiturnconversation
• Figure 2: Syntax of a graph.
• Figure 3: An example graph
• Figure 4: Lumos syntax to express and certify LMS specifications.
• Figure 5: Subgraph sampling example code