RvLLM: LLM Runtime Verification with Domain Knowledge
Yedi Zhang, Sun Yi Emma, Annabelle Lee Jia En, Jin Song Dong
TL;DR
The paper addresses the unreliability of LLM outputs in safety-critical domains by introducing RvLLM, a runtime verification framework that enforces domain-specific constraints encoded in ESL.ESL is designed to be approachable for domain experts while enabling formal reasoning via a DeNF-based specification and predicate-rule representation.RvLLM uses a four-stage pipeline—interpretation abstraction, rule normalization, forward chaining, and query generation—to detect inconsistencies and verify LLM outputs against domain knowledge.Experiments across MRT-act violation detection, numerical comparison, and inequality solving demonstrate that RvLLM improves true-positive detection and offers a practical path toward reliable, domain-aware LLM deployments, though perception and ESL expressiveness remain areas for improvement.
Abstract
Large language models (LLMs) have emerged as a dominant AI paradigm due to their exceptional text understanding and generation capabilities. However, their tendency to generate inconsistent or erroneous outputs challenges their reliability, especially in high-stakes domains requiring accuracy and trustworthiness. Existing research primarily focuses on detecting and mitigating model misbehavior in general-purpose scenarios, often overlooking the potential of integrating domain-specific knowledge. In this work, we advance misbehavior detection by incorporating domain knowledge. The core idea is to design a general specification language that enables domain experts to customize domain-specific predicates in a lightweight and intuitive manner, supporting later runtime verification of LLM outputs. To achieve this, we design a novel specification language, ESL, and introduce a runtime verification framework, RvLLM, to validate LLM output against domain-specific constraints defined in ESL. We evaluate RvLLM on three representative tasks: violation detection against Singapore Rapid Transit Systems Act, numerical comparison, and inequality solving. Experimental results demonstrate that RvLLM effectively detects erroneous outputs across various LLMs in a lightweight and flexible manner. The results reveal that despite their impressive capabilities, LLMs remain prone to low-level errors due to limited interpretability and a lack of formal guarantees during inference, and our framework offers a potential long-term solution by leveraging expert domain knowledge to rigorously and efficiently verify LLM outputs.