BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Computer Science and Engineering - ECPv6.13.0//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Computer Science and Engineering
X-ORIGINAL-URL:https://homecse.iitd.ac.in
X-WR-CALDESC:Events for Computer Science and Engineering
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Asia/Kolkata
BEGIN:STANDARD
TZOFFSETFROM:+0530
TZOFFSETTO:+0530
TZNAME:IST
DTSTART:20260101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Asia/Kolkata:20260129T120000
DTEND;TZID=Asia/Kolkata:20260129T130000
DTSTAMP:20261010T144517
CREATED:20260124T095221Z
LAST-MODIFIED:20260124T123516Z
UID:2392-1769688000-1769691600@homecse.iitd.ac.in
SUMMARY:Lumos: A DSL for Language Model System Certification by Isha Chaudhary
DESCRIPTION:Venue: Bharti 501\nAbstract: 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.\n  \nBio: 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.
URL:https://homecse.iitd.ac.in/event/lumos-a-dsl-for-language-model-system-certification-by-isha-chaudhary/
LOCATION:Bharti 501\, IIT Campus\, Hauz Khas\, New Delhi
ORGANIZER;CN="Subodh Sharma":MAILTO:svs@cse.iitd.ac.in
END:VEVENT
END:VCALENDAR