RvLLM: LLM Runtime Verification with Domain Knowledge
Not on the map. Why?
Abstract (arXiv)
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.
Key facts. Cited by 17 papers in the map (data through 14 Oct 2026). Builds on 35 of its 70 references that are in the map. First posted on arXiv 24 May 2025.
Builds on
35 of 70 references.
References · 35
- 2023GPT-4 Technical Reportcited by 18,396
- 2020Measuring Massive Multitask Language Understandingcited by 7,963
- 2024Qwen2.5 Technical Reportcited by 4,942
- 2021TruthfulQA: Measuring How Models Mimic Human Falsehoodscited by 2,975
- 2022Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language modelscited by 1,998
- 2023Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generationcited by 1,391
- 2023SelfCheckGPT: Zero-Resource Black-Box Hallucination Detection for Generative Large Language Modelscited by 810
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
- 2023AGIEval: A Human-Centric Benchmark for Evaluating Foundation Modelscited by 716
- 2023C-Eval: A Multi-Level Multi-Discipline Chinese Evaluation Suite for Foundation Modelscited by 708
- 2023DecodingTrust: A Comprehensive Assessment of Trustworthiness in GPT Modelscited by 518
- 2021SummaC: Re-Visiting NLI-based Models for Inconsistency Detection in Summarizationcited by 407
23 more
- 2023Trustworthy LLMs: a Survey and Guideline for Evaluating Large Language Models' Alignmentcited by 401
- 2023HaluEval: A Large-Scale Hallucination Evaluation Benchmark for Large Language Modelscited by 341
- 2023LegalBench: A Collaboratively Built Benchmark for Measuring Legal Reasoning in Large Language Modelscited by 336
- 2024Hallucination is Inevitable: An Innate Limitation of Large Language Modelscited by 332
- 2016Safety Verification of Deep Neural Networkscited by 263
- 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 228
- 2023Don't Make Your LLM an Evaluation Benchmark Cheatercited by 194
- 2023LM vs LM: Detecting Factual Errors via Cross Examinationcited by 156
- 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
- 2023Complex Claim Verification with Evidence Retrieved in the Wildcited by 110
- 2023How Many Unicorns Are in This Image? A Safety Evaluation Benchmark for Vision LLMscited by 108
- 2017Verifying Properties of Binarized Deep Neural Networkscited by 79
- 2024LLMs Will Always Hallucinate, and We Need to Live With Thiscited by 78
- 2023ChatGPT as a Factual Inconsistency Evaluator for Text Summarizationcited by 75
- 2019An Abstraction-Based Framework for Neural Network Verificationcited by 68
- 2024Red Teaming Visual Language Modelscited by 65
- 2024MultiTrust: A Comprehensive Benchmark Towards Trustworthy Multimodal Large Language Modelscited by 53
- 2024ALI-Agent: Assessing LLMs' Alignment with Human Values via Agent-based Evaluationcited by 47
- 2023BenchLMM: Benchmarking Cross-style Visual Capability of Large Multimodal Modelscited by 41
- 2023LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyondcited by 38
- 2021BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networkscited by 17
- 2024Drowzee: Metamorphic Testing for Fact-Conflicting Hallucination Detection in Large Language Modelscited by 14
- 2024CheckEmbed: Effective Verification of LLM Solutions to Open-Ended Taskscited by 10
Built on by
Citing papers per year: 2025: 2; 2026: 15.
17 papers.
Sort:
By area:
- 2025Trust but Verify! A Survey on Verification Design for Test-time Scalingcited by 8
- 2026Cryptographic Runtime Governance for Autonomous AI Systems: The Aegis Architecture for Verifiable Policy Enforcementcited by 5
- 2026AI-NativeBench: An Open-Source White-Box Agentic Benchmark Suite for AI-Native Systemscited by 3
- 2025Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systemscited by 2
- 2026LLM-enabled Applications Require System-Level Threat Monitoringcited by 2
- 2026Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimizationcited by 2
- 2026Evaluating LLM-Generated ACSL Annotations for Formal Verificationcited by 1
- 2026Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logiccited by 1
- 2026One-Token Verification for Reasoning Correctness Estimationcited by 1
- 2026Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflowscited by 1
- 2026Representation Transitions Reveal Emerging Safety Risks in Multi-Turn LLM Agentscited by 1
- 2026ATLAS-RTC: Closing the Loop on LLM Agent Output with Token-Level Runtime Controlcited by 0
5 more
- 2026Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Studycited by 0
- 2026TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamplescited by 0
- 2026Who Holds the Pen? Let Specifications, Not Agents, Sign Offcited by 0
- 2026RSure-Agent: Reliable Use of Tool Observations for Remote Sensing Agentscited by 0
- 2026One Monitor Does Not Fit All: Formalism-Agnostic Runtime Verification for Agentic AIcited by 0
- 2026One Monitor Does Not Fit All: Formalism-Agnostic Runtime Verification for Agentic AI14 Oct 2026
- 2026RSure-Agent: Reliable Use of Tool Observations for Remote Sensing Agents4 Oct 2026
- 2026Representation Transitions Reveal Emerging Safety Risks in Multi-Turn LLM Agents30 Sep 2026
- 2026Who Holds the Pen? Let Specifications, Not Agents, Sign Off24 Sep 2026
- 2026Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows20 May 2026
- 2026Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization8 May 2026
- 2026TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples8 May 2026
- 2026Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study16 Apr 2026
- 2026ATLAS-RTC: Closing the Loop on LLM Agent Output with Token-Level Runtime Control29 Mar 2026
- 2026Cryptographic Runtime Governance for Autonomous AI Systems: The Aegis Architecture for Verifiable Policy Enforcement15 Mar 2026
- 2026One-Token Verification for Reasoning Correctness Estimation1 Mar 2026
- 2026LLM-enabled Applications Require System-Level Threat Monitoring23 Feb 2026
5 more
- 2026Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic20 Feb 2026
- 2026Evaluating LLM-Generated ACSL Annotations for Formal Verification14 Feb 2026
- 2026AI-NativeBench: An Open-Source White-Box Agentic Benchmark Suite for AI-Native Systems14 Jan 2026
- 2025Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems18 Nov 2025
- 2025Trust but Verify! A Survey on Verification Design for Test-time Scaling20 Aug 2025
- 2026AI-NativeBench: An Open-Source White-Box Agentic Benchmark Suite for AI-Native Systemscited by 3
- 2026Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflowscited by 1
- 2026Representation Transitions Reveal Emerging Safety Risks in Multi-Turn LLM Agentscited by 1
- 2026ATLAS-RTC: Closing the Loop on LLM Agent Output with Token-Level Runtime Controlcited by 0
- 2026TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamplescited by 0
- 2026Who Holds the Pen? Let Specifications, Not Agents, Sign Offcited by 0
- 2026One Monitor Does Not Fit All: Formalism-Agnostic Runtime Verification for Agentic AIcited by 0
- 2026One Monitor Does Not Fit All: Formalism-Agnostic Runtime Verification for Agentic AI14 Oct 2026
- 2026Representation Transitions Reveal Emerging Safety Risks in Multi-Turn LLM Agents30 Sep 2026
- 2026Who Holds the Pen? Let Specifications, Not Agents, Sign Off24 Sep 2026
- 2026Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows20 May 2026
- 2026TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples8 May 2026
- 2026ATLAS-RTC: Closing the Loop on LLM Agent Output with Token-Level Runtime Control29 Mar 2026
- 2026AI-NativeBench: An Open-Source White-Box Agentic Benchmark Suite for AI-Native Systems14 Jan 2026
- 2026Cryptographic Runtime Governance for Autonomous AI Systems: The Aegis Architecture for Verifiable Policy Enforcementcited by 5
- 2025Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systemscited by 2
- 2026LLM-enabled Applications Require System-Level Threat Monitoringcited by 2
- 2026Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimizationcited by 2
- 2026Evaluating LLM-Generated ACSL Annotations for Formal Verificationcited by 1
- 2026Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logiccited by 1
- 2026Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Studycited by 0
- 2026RSure-Agent: Reliable Use of Tool Observations for Remote Sensing Agentscited by 0
- 2026RSure-Agent: Reliable Use of Tool Observations for Remote Sensing Agents4 Oct 2026
- 2026Vertex-Softmax: Tight Transformer Verification via Exact Softmax Optimization8 May 2026
- 2026Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study16 Apr 2026
- 2026Cryptographic Runtime Governance for Autonomous AI Systems: The Aegis Architecture for Verifiable Policy Enforcement15 Mar 2026
- 2026LLM-enabled Applications Require System-Level Threat Monitoring23 Feb 2026
- 2026Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic20 Feb 2026
- 2026Evaluating LLM-Generated ACSL Annotations for Formal Verification14 Feb 2026
- 2025Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems18 Nov 2025