Lumos: A DSL for Language Model System Certification by Isha Chaudhary

Venue: Bharti 501

Abstract: As Language Model Systems (LMS) are deployed across an expanding range of applications, aligning them with human ethics has become crucial. Although recent works propose methods to formally certify LMS properties such as fairness, correct question answering, and safety, these approaches are generally ad hoc and hard to generalize. We introduce a principled alternative: a domain-specific language, Lumos, for specifying and formally certifying LMS behaviors. Lumos is the first imperative probabilistic programming language 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. 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. 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.

Bio: Isha Chaudhary is a 4th year Computer Science Ph.D. student at the University of Illinois Urbana-Champaign, advised by Prof. Gagandeep Singh. Her research focuses on formal methods to make frontier models trustworthy. Her work has been recognized at top-tier conferences including ICLR 2025, AISTATS 2026 (spotlight), and MLSys 2024. She earned a B.Tech. in Electrical Engineering from IIT Delhi, where she was awarded the Institute Silver Medal and Prof. C.S. Jha Memorial Award. She earned an MS in CS from UIUC.