RvLLM: LLM Runtime Verification with Domain Knowledge

TL;DR

This paper introduces RvLLM, a runtime verification framework that uses a new specification language, ESL, to incorporate domain knowledge for detecting errors in LLM outputs across various tasks.

Contribution

The work presents a novel ESL specification language and a runtime verification framework, RvLLM, enabling domain experts to customize constraints for verifying LLM outputs in real-time.

Findings

RvLLM effectively detects erroneous outputs in multiple LLMs.

The framework is lightweight and flexible for various domain-specific tasks.

Experimental results show improved reliability of LLM outputs with RvLLM.

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.