RvLLM: LLM Runtime Verification with Domain Knowledge
Authors: Yedi Zhang
Sun Yi Emma
Annabelle Lee Jia En
Jin Song Dong
Venue: NeurIPS 2025 poster ()
Keywords: Runtime Verification
Specification
Domain Knowledge
Large Language Model
Primary area: evaluation
TL;DR: A runtime verification framework of LLMs with domain knowledge.

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 constraints in a lightweight and intuitive manner, supporting later runtime monitoring 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. RvLLM operates in two main stages: interpretation and reasoning. During interpretation, it derives interpretations of the specification based on the context, which then guide the reasoning process to identify inconsistencies. When new knowledge is derived, RvLLM issues a follow-up query to the LLM to further verify the consistency. We evaluate RvLLM on three representative tasks: violation detection against Singapore Rapid Transit Systems Act, numerical comparison, and inequality solving. Experimental results show 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 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.

RvLLM: LLM Runtime Verification with Domain Knowledge
Yedi Zhang*
Sun Emma National University of Singapore Singapore
National University of Singapore Singapore
Annabelle Lee Jia En National University of Singapore Singapore
Jin Song Dong National University of Singapore Singapore
Abstract
Large language models (LLMs) have emerged as a dominant AI paradigm due their exceptional text understanding and generation capabilities. However, their tendency to generate inconsistent erroneous outputs challenges their relia- bility, especially high-stakes domains requiring accuracy and trustworthiness. Existing research primarily focuses on detecting and mitigating model misbehav- ior in general-purpon scenarios, often overlooking the potential of integrating domain-specific knowledge. In this work, advance misbehavior detection by incorporating domain knowledge. The core idea to design a general specification language that enables domain experts customize domain-speciff constraints in a lightweight and intuitive manner, supporting later runtime monitoring of LLM outputs. To achieve this, design novel specification language ESL and in- troduce a runtime verification framework RvLLM to validate LLM output against domain-specifie constraints defined in ESL. RvLLM operates in two main stages: interpretation and reasoning. During interpretation, it derives interpretations of the specification based the context, which then guide the reasoning process iden- tify inconsistencies. When new knowledge is derived, RvLLM issues follow-up query the LLM to further verify the consistency. We evaluate RvLLM on three representative tasks: violation defection against Singapore Rapid Transit Systems Act, numerical comparison, and inequality solving. Experimental results show 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 a lack of formal guarantees during inference, and our framework offers potential long-tern solution by leveraging expert domain knowledge to rigorously and efficiently verify LLM outputs.
Introduction
operating on predefined and deterministic rules, large language learn data representation and processing automatically from the training datasets, achieving human-like or even superhuman performance, and have driven significant
Unlike rule-based systems
52
models (LLMs) I
23
62
advancements in various practical applications [10 33 55 44 24]. However, their non-deterministic
and unpredictable nature sometimes leads to inconsistent erroneous outputs [3] 49 posing
significant risks in safety-critical or Knowledge-intensive domains. Recent studies [6] 5 have shown
"Corresponding author
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

that such misbehavior in LLMs cannot be fully eliminated, underscoring the urgent need for dedicated verification and validation methodologies to enhance the reliability of LLLM-generatee outputs.
primarily aims to establish comprehensive benchmarks to evaluate the overall model performance against domain-agnostie criteria- accuracy, coherence, and fairness-in alignment with the intended application. While these approaches effectively assess general behavior and reveal edge cases that may provoke unexpected responses, they are limited to predefined benchmarks and lack the specificity needed to address domain-specific assessment needs. LLM verification, instead, may serve as a complementary mechanism to LLM testing by providing formal guarantees on model behavior. Despite substantial progress over the past decade in neural network verification [8] [9] [9 34 59 48 65), existing methods exhibit notable limitations: they are primarily tailored to simpler model architectures-sut such as deep or convolutional networks and classification tasks, struggling to scale to the complexity of modern Al models and their diverse functionalities. Furthermore, these approaches target general properties such as robustness and fairness, making them ill-suited for Nomain-speciinn properties. Therefore, developing a dedicated verification paradigm tailored to LLMs is crucial for ensuring certified and reliable outputs.
LLM testing [67
27
30
68
in the late 20th century can be attributed to their inability to handle incomplete information and poor scalability in real-world complexity. Defining comprehensive rule sets for open domains has been proven infeasible [52] 28 We argue that such rules can only be statistically approximated capability exemplified by LLMs. However, this approximation cannot substitute for explicit rule encoding, and learning- -ased models remain inherently unreliable, particularly in edge cases demanding strict adherence to domain-specific requirements. This highlights the need for verifying explicitly defined rules in a lightweight and incremental manner for practical deployment and maintainability.
On the other hand, the decline of rule-based expert systems 25
31
22
This paper. Building on these foundations, we propose runtime verification with domain knowledge as a sustainable solution to ensuring reliable LLM behavior, motivated by two key insights: i) Runtime verification offers a lightweight yet rigorous means to bridge testing and formal verification by assessing system behavior against formal properties during execution; ii) Existing work primarily focuses on generic misbehavior detection while often overlooking the critical role of domain-speciff expertise. Integrating such knowledge is crucial for handling edge cases and enhancing LLM reliability in specialized tasks, where domain knowledge can significantly improve performance.
To achieve this, we introduce RvLLM, an innovative runtime verification framework tailored to LLMs ensure reliable outputs, partieularly against axiomatic domain specifications. The idea is to automatically check whether the LLM LLM-generated responses adhere to domain-specific constraints expressed in simple, adaptable specification language. This simplicity and flexibility empower domain experts to encode their knowledge and formally define constraints that capture the expected behavior of LLMs specialized applications. To support this, we introduce ESL, general language tailored for encoding rule-based domain expertise. ESL integrates natural language with formal logic to ensure the adaptability the natural language settings of LLMs while enabling the structured and formal representation of properties to verify. This design allows for the rigorous specification of domain-specific criteria across diverse LLM applications.
Figure D presents an overview of our proposed framework. Given an ESL specification provided by domain experts, RvLLM first extracts relevant information from the LLM's context and outputs to interpret the specification, generating a set of propositional formulae along with truth assignments for the corresponding propositions. Following normalization step, these formulae are transformed into a standard form and subsequently validated using forward chaining procedure. This process either detects inconsistencies due to logical contradictions or infers new knowledge. Once new knowledge is inferred, the query generation module issues targeted queries, evaluates the LLM responses, and detects inconsistencies when outputs contradict the previously inferred knowledge.
Experimental results. We evaluate the effectiveness of RvLLM through experiments on three representative tasks: violation detection against Singapore Rapid Transit Systems Act (51), numerical comparison, and inequality solving, using diverse set of LLMs. The experimental results show that RvLLM significantly enhances the reliability of LLM output in these domain-specific tasks. In the violation detection task, employing RvLLM as complementary mechanism increases the true positive rate (TPR) by 15.7% to 50.2% across various models. In the numerical comparison task, RvLLM detects nearly all errors in the LLM responses across 100 randomly generated questions. In the inequality solving task, RvLLM facilitates systematic analysis of the step-by-step reasoning

---

Interpretation Abstraction
Interpeetation
Rule-like Formula Transformation
Domaia Experts
Spec.
Contest
Rule-like propocitonal formulay
& Value-assigued propositions
Consistent
Inconsistent
Consistent
Query related to p
?
Generation Ornele
Query
Forward Chaining
Inconsistent
Output
Knowledge derived
Figure 1: An overview of RvLLM. Given an L.M'' context and outputs, RvLLM first extracts relevant propositions and translates the ESL specification into normalized propositional logic formulae. These are then processed through forward chaining to detect inconsistencies and infer new knowledge, which subsequently guides follow-up queries and consistency checks across successive LLM responses.
process from LLMs, effectively identifying its deviations from expert-defined specifications. These specifications are primarily grounded in fundamental algebraic inequality properties typically covered at the junior college level. Notably, despite the incomplete domain knowledge in the inequality solving task, RvLLM still achieves TPR of 50% in detecting erroneous solutions. We argue that such runtime verification approach can function rule-based or reasoning intensive domains where adherence to specific constraints is essential. We methods. Results show that RvLLM demonstrates superior performance by maintaining both high true positive and negative rates, whereas existing methods often exhibit non-negligible trade-off between these metries.
critical safeguard for LLMs, particularly in
ccasoning-intensive
further compare RvLLM with existing runtime hallucination-deteea
2 ESL: simple way of specifying domain-specific properties
In this section, we introduce a general language, Expert Specification Language (ESL), which can be customized with domain-specifen predicates by experts impose behavioral constraints LLMs.
2.1 Design guidance
In the following, we give our high-level requirements for designing specification language that encapsulates LLM behavioral constraints from the perspective of domain experts. The core objective to strike a balance between iser-friendliness and expressiveness. following regulation from Singapore Rapid Transit System Act [51]:
illustrate this with the
"No person shall consume or attempt to consume any chewing gum or bubble gum while in or upon any part of the railway premises."
Accessibility for domain experts. The primary goal of this specification language is to empower
domain experts, even those with limited programming or formal methods experience, to effectively define and enforce constraints on the LLM's behavior. To balance expressiveness and user-friendlliness. we base the specification rule on predicate logic [53] (2)). restricted to prenex normal forms [53] 20]
and consisting solely of universal quantifiers. We further constrain its quantifier- free part rule- like form (or implication), yielding a simplified variant of predicate logic expressible as (f (z) =
(()) F Specifically, both the left-hand side (LHS) and right-hand side (RHS) of the rule-like part quantifier-free predicate formulae composed of predicates applied terms that may include variables (e.g., .), constants (e.g.. "bubble gum"), and functions of terms (e.g., sin(x)). For example, ChewGum (ar) is an atomic predicate with single variable argument v, and "SGreater(Squaree is also an atomic predicate with two arguments: the function term Square(z) and the constant term
0)
Ease of customization. The specification language should be designed to support seamless cus- tomization, enabling adaptation to diverse domain-specific requirements. To facilitate this, we require each predicate in the specification to be associated with a natural language description that aligns with domain expertise. These descriptions allow customized predicates to remain clear, semanti- cally grounded, and adaptable to specific application contexts. Additionally, built-in terms such as We use instead of i there could be sequence of variables.

---

arithmetic functions can be provided to streamline constraint formulation and reduce the need for extensive customization. For example, domain expert can define their specialized atomic predicates ChewGum(ar) and InRailway(2) (z) associated with a natural language description as follows:
"ChewGum(z) == a person z consumes attempts to consume chewing gum or bubble gum." some part of railway premises."
"InRailway(()) (r) = person
Efficient interpretation. The language should also support an efficient interpretation procedure to obtain propositional formulae from the specification rule for subsequent logical verification. To this end, we remove the universal quantifier from standard predicate formulas. For example, the regulation previously mentioned, typically expressed as VY..IInRallway(11 = -ChewGum(z)) will be simplified to InRailway = -ChewGum(x))
2.2 Formalization
In this section, we formalize our specification language, ESL. We begin with the definition of Deductive Normal Form (DeNF), which serves as a foundation for the remainder of this paper.
Definition 1. Given a propositional formula 4/1 = 1/2, if t/1 disjunctive norm form (53) and 4/2 is a conjunctive norm form (53], then we call 1²1 = 122 is a deductive normal form (DeNF).
Definition 2. An ESL rule is a DeNF where each proposition is substituted by predicate.
An ESL specification comprises three components: a variable set V, a predicate set P, and an ESL rule set Rg. For each predicate f E P, an associated natural language description is required. For instance, the following ESL specification encodes the regulation aforementioned Section 2.1
VVariables:
("x">,
*Predi cates":
("ChexGun(x) (x)
parson consunes attempts conaune chesing gun gum.", "IoRallvay(1) person in aome part of railway premises"),
"Rulee":
("InRailvay(x) not ChezGun(x)")
Interpretation of ESL rules. An interpretation of an ESL rule assigns objects to variables (i.e., variable binding) in the predicate of and evaluates the truth value (True, False, or Unknown) of the resulting proposition after substitution. Note that we adopt the open-world assumption [I7] to better accommodate the open-ended nature LLMs. this work, interpretations are derived from the context and LLM outputs, serving as the domain of discourse [26]. Now, consider the following contextual scenario:
"In crowded MRT train, Alex nervously chews gum to ease stress before an interview. Suddenly, the train jolts, and the gum flies out, landing stranger's shirt. Awkward glances turn into laughter as apologies spill out, diffusing tension in the confined space."
The interpretation of the rule InRailway(a)) 7 -ChewGum(z) {InRailway(o1) True, InRailway(oz) = True, ChewGum(o1) True, ChewGum(oz) Unknown], where or 'Alex' and 02 = 'stranger'.
3 Methodologies of RvLLM
As illustrated in Figure I RvLLM conducts runtime verification through four stages: interpretation abstraction, rule normalization, forward chaining, and query generation. In this section, we detail the methodology of each stage and demonstrate its application using an example given in Figure
3.1 Interpretation abstraction
Given context and LLM outputs (the union denoted as σ)) as the domain of discourse D and an ESL specification & (V, Re), we first leverage a perception agent to obtain all possible objects from D and propositionalize much possible of the predicates defined in We call this the perception process. Then, for each rule E Re, we bind the variables in each predicate all possible objects in search-and and-ree operation, to generate the propositional formulae set. Note that, given

---

The specification provided by an expert and written ESL:
"Variables.
("a "y,
"Predicates" "Rules"
[Isrreater(r.y) the number is greater than number y:?) ()) & lerç 0) IsGrester 4,y* x))?
Query: 15.2 and 15.12, which one greater?
Response by GPT 4.1 nano: 15.12 is greater than 15.2.
Level-1 interpretation 4
[ 92) True, 01 15.12.
Level-2 interpretation ly!
(Isúreater(ss, True, 10)
knowledge
under interpretation l
(sGreater(o,, oz) True,o,= 11512, 0p 152)
Inconsistentl
(IsGreater(ou, os) False)
New Query. Please output Is 151.2 greater than 162?
New Responee by GPT 4.1 nano: False.
Figure 2: Runtime verification of GPT 4.1 nano by RvLLM for number comparison task.
variable binding for a rule r E Rg, the interpretation has two different results: i) all predicates in the LHS of are propositionalized successfully with assigned truth value under the binding, which call a complete binding in this work, or ii) only part of predicates are propositionalized due to the insufficient information from the domain of discourse, which we call partial binding.
Given this distinction, we introduce two levels of interpretation in this work: Level-1 and Level-2. Specifically, Level-1 interpretation disregards all the partial variable binding and operates only the complete variable bindings. Given a partial binding, Level-2 interpretation, in contrast, employs a perception agent to instantiate all the variables that are not assigned with object in the binding, in a way such that the resultant proposition returns True given the domain of discourse.
Example 1. Consider the example in Figure 2 which illustrates our approach using simple numerical comparison question with a specification encoding a basic algebraic property of multipli- cation, the interpretation abstraction process first gets all possible objects and propositionalizes the predicate IsGreater as follows: (pu = IsGreater 02) = True. P1 = IsGreater (02, 01) = False) with 0₁ 15.2 and 02 15.12. Then, it obtain all possible variable binding (b,, b23 for the rule &6 where ,; = far + 01, + 02} and b2fx +
+ ). b, results in a formula Po A IsGreater 0) = IsGreater(15.2** +.) for vb, which is partial binding. Similarly, b2 is also par- tial. Consequently. for the Level-1 interpretation, no propositional formula is successfully generated, and the checking procedure exits with no inconsistency detected. While for the Level-2 interpretation. it successfully instantiates the variable for the partial bindings bj and ?2 with an object 03 10, and obtain an additional proposition P2 = IsGreater 0) True. Then, the updated bindings are: bj {x + 01. y 02, 03) }, b/2 = {ir + y + 2 + 03). By applying b/, we can obtain new proposition P3 IsGreater #0,, 02 +03) (SGreater(15.2444 10, 15.12 10) but with unknown truth value. Similarly, we obtain P4 = IsGreater (02* o3, 01 #0z) = IsGreater 5. 12 10, 15.2=10) = Unknown by b/2. Finally, we generate two propositional formulae: 1/ = Po A p2 + Pa via by and
2/2
A p2 p4 via b/2 for the following component.
3.2 Rule-like propositional formula transformation
Given a DeNF formula s = D, v D2 ... Dm = CIACA.... Ca. where each D; is conjunction literals 1. A A A.A..... A...AIp im, and each C, is a disjunction of literals E9 v vIS V... 1 'n.* the formula transformation module is designed to reformulate v into a set of propositional formulae I' in rule-like form, i.c., implication, such that the LHS of each formula in F is a literal conjunction and the RHS is a single literal.
To achieve this, we first transform vp to formula set I2 = (D; = C2 lie [m].j E [m]]. Then, for each single formula $i.j Dj Cj- = 1h A A... ALD, + Bn vig...... V..v..VV Viy we reformulate as the implicant formula set N Vai"" following the idea unit propagation 63
m 0 1 A A
A A
(4)
E LE (ng)
om;
RE(ng]Akpht
Finally, given DeNF bb, we obtain the corresponding reformulated rule-like propositional formula set T = Uke[m]Je[n] I" " and given DeNF set R, we use I' to denote the union of all rule-like
5

---

form formulae transformed by each formula in R. i.e., I' = UVER Te. In the remainder of this paper, we use LitR (resp. Lit,) to denote the set of all the literals that appeared in R (resp. vh), The rules 4/1 and 1/2 obtained in Example are already expressed in the rule-like form.
Example 2. Consider a DeNF into an equivalent formula set r, = [311,1, 11,2, 22,1, 1222,. where V1,1 = A by = 01 V d1. 211.2 = di A bi + C22 12,1 = 02 + Ci V dı, and 222, = a2 + 02. For each single formula
(a) b1) V 02 (c1 V di) c2. We first transform e
in I we then reformulate it follows: I h. = {ar A by - = =1,01 b A A-1 q1),
#1.2 = {ai A Ab + c1 1 = {ar A -c + d1, a1 A di = c.J.
Va. = {aa Ac2), and finally
obtain the set of rule-like propositional formulae as Te = r Ui.1
UT 2n
Ur V2 ur V2.2
V2,1
3.3 Forward chaining
Given a rule set R obtained above with corresponding literal set LitR and a subset of literals Lit C Litr with predetermined truth values, the forward chaining (FC) procedure is designed to: verify consistency, and ii) infer truth values for the undefined literal ( LitR \Lit. The truth value inference of undefined literals is operated based on the inference rule of modus ponens [14), which is closely aligned with the traditional forward chaining algorithm [52) utilized in rule-based systems. However, compared to the traditional FC algorithm, which requires each rule to be strictly Horn Clause, a significant distinction between our algorithm and the traditional one is: we require that all negative literals appearing in Litz are also included in the forward chaining graph. Such an extension enables us detect the inconsistency by identifying truth values for undefined literals. For instance, consider a rule set {a A b = c} and literals defined as a = b = True and c False. In this case, the truth value of literal e is inconsistent with the inference result derived from the rule set.
To achieve it, given a rule set Is and an initially defined literals Lit with truth values, we first construct initial graph G through the following steps:
Step (Literal Nodes): Create node for each literal that appears in the rule set R'-
Step (LHS Node): Create an LHS node for each rule-like propositional formula in FR-
Step 3 (Edges): For each formula in I TR, such as 4 A ... A ln = lx+1 E Tw, add a directed edge from each literal node 4, (i e [ml) to the corresponding LHS node, and add directed edge from this LHS node to the literal node Ln+1-
Next, according the initially defined literals, we mark all the literal nodes valued True as Lit and mark all the literal nodes valued False as Lit+, based on the truth value of literals from Lit. Then, we perform forward chaining procedure on the graph G and update Lit and Lit as follows until no more update can be done or an inconsistency is detected by Lit n + 0:
Update of Lit' and Litt: : For each L.HS node encoding the rule-like formula (or implication) 4 ... A Ln + ln+1, if (4...., 42 S Lit", then we have Litt Lit 4x41 and Lit = =ith U-
Example 3. We now illustrate the graph construction and the corresponding FC procedure for the rule set T = {WI, 32 under the Level-2 2 interpretation given in Example We first obtaín all the literals as LitR = {po. P1. P2. P3. P1} with Lit = {po. p2} and Litt {pr). construct the literal nodes correspondingly. and construct the LHS node set as {po&pp2 P1 (1pp))).. Then, directed edges are added as follows: Po + Pr& P2 - &p&p2, Po& + P3. P1 - Pr & Pa + p1 &P2, Pi &pp + p4. resulting initial graph. Next, we check the logic consistency. For the LHS node Po&P2, since {po- P2] S Lit", we update Lit" = Lit = {Po, P2, P3) and Lit = Lit-U-ps = {pI, pps) where "Py True" is the new knowledge derived. For the LHS node pı &22, since p1 & Litt, there is no update Lit and Lit?, hence new knowledge inferred.
3.4 Query generation
Once RvLLM obtains the newly inferred knowledge, the query generation module generates concrete query to the target LLM related to the knowledge, and requires the LLM to analyze its truth value. For the inferred knowledge pa IsGreater 151.2, 152) = True in Example 3 we generate the corresponding query as "Iy 151.2 greater than 152?" as shown in Figure Since the target LLM returns False, an inconsistency is detected, indicating diagnostic error in the target LLM.

---

The soundness of this work-the ability to detect inconsistencies with respect to domain-specific
Clarification.
depenns on the accurate and faithful encoding of domain knowledge by the expert. Thus, the validity of RvLLM hinges on the alignment between the specification given in ESL and the underlying domain knowledge, and any misrepresentations in this encoding may compromise the soundness of the method.
4 Experiments
To evaluate the effectiveness of RvLLM, we apply it to the runtime verification of LLMs across three representative tasks that require domain-specific knowledge: violation detection against Singapore Rapid Transit Systems Act [5I], numerical comparison, and inequality solving. For a comprehensive evaluation, we include both SOTA and non-SOTA LLMs as our benchmark, including Qwen 2.5 (max, plus, turbo. 7B, 14B, 32B, 72B). GPT (4.1, 4.1 mini, 4.1 nano), Gemini 2.0 (Flash, Flash Lite), and DeepSeek-VV V3. All experiments are conducted on a machine with an Intel (R) Xcon(R) w7-2475X processor. A dedicated guideline for designing interpretation abstraction prompts for the perception agent is provided in the appendices, along with additional experimental details and descriptions of the datasets and specifications used throughout the experiments.
To ensure a comprehensive evaluation, we also compare RvLLM with other runtime approaches, including SelfCheckGPT [47] and a prompt-based augmentation method that explicitly encodes domain-specific constraints within prompts. Due to the computational overhead and API costs associated with large-scale evaluations, we restrict our comparison to cost-efficient model variants. Additional experimental results and missing implementation details/justifications can be found in (64)
4.1 Case study 1: violation detection against Singapore Rapid Transit Systems Act
For this case study, we apply RvLLM under the Level-1 interpretation evaluate the LLM's responses in detecting violations within contextual scenarios against the Singapore Rapid Transit Systems Act. In this capacity, RvLLM can be regarded as complementary mechanism enhance the LLM's capability in detecting the law violations in this study. We conduct experiments using contextual scenarios derived from (58), consisting of 304 cases in total-281 I labeled as involving violations (unsafe) and 23 as not (safe). To incorporate relevant domain knowledge, we carefully encode 31 of the 53 regulations from Singapore Rapid Transit System Act into ESL specifications. took research scientist three days to interpret the law and develop corresponding specifications one-time effort applicable for verifying any LLM application against these regulations. In this study, the same model serves both as the target LLM and as the perception agent.
Results. Table reports the violation detection results by various LLMs, with and without our framework as a complementary analysis method, where TPR and TNR denote the true positive rate and true negative rate for the violation detection, i.c.. a violation column gives the average exccution time for each scenario analysis. In the standalone LLM setting, case where the model successfully identifies violation in an unsafe
positive example. The last
true positive is defined scenario, and true negative corresponds to case where the model confirms the absence of violations in safe scenario. In the combined LLM+ setting, a true positive is recorded if either the LLM or RvLLM detects violation in an unsafe scenario, whereas a true negative is defined as case that both the LLM and RvLLM determine the absence of any violation in safe scenario. The results show that integrating RvLLM significantly enhances the TPR, improving the target LLM's capability to identify violations. However, we also observe that the integration of RvLLM can reduce the TNR in some models. This decline is primarily due to inaccuracies or incompleteness in the interpretation procedure by the perception agent. We also find that, among all evaluated models, DeepSeck-V. achieves the highest TPR in both standalone and integrated settings, demonstrating superior detection capabilitics in this domain-speciftt specific task and good performance on language understanding.
Figure 3 giiees the comparison results of RvLLM against other baseline methods. We observe that SelfCheckGPT often yields the highest TPR gains, as labels nearly all outputs as "hallucinations", resulting in near-zero TNR. This outcome is expected since SelfCheckGPT relies solely on output stability without leveraging domain knowledge, making it more suitable for open-domain generation. The prompt augmentation method (also known as --M--as-a-jddge) achieves TPR performance comparable to RvLLM but accompanied by a non-negligible TNR decrease. contrast, RvLLM achieves a better balance between TPR and TNR, yielding more reliable and interpretable results.
7

---

Table Violation detection results of LLMs with and without RVLLM against the Singapore Rapid Transit Systems Act [ST]. All percentage values are reported rounded to one decimal place.
LLM
ILM RVLLM
Performance of RVLLM
Target LLMs
Time (s)
TPR
TNR
TPR
TNR
TPR
TNR
Owen max 62
56.2%
91.3%
1%
91.3%
+29.9%
3.00
Qwen plus 62
58.4%
81.9%
+23.5%
0
5.32
Qwen turbo 62
39.1%
74.7%
+35.6%
0
1.64
Qwen 2.5 (7B) [62
16.0%
61.2%
87.0%
+45.2%
-13.0%
2.28
Qwen 2.5 (14B) 62
38.8%
95. 75.7%
80.4%
87. 17.0%
+41.6%
-8.7%
3.11
Owen (32B)
56.6%
75.7%
87.5%
95.7% 35.7%
+31.0%
2.55
Qwen 2.5 (72B)
57.3%
80.4%
95.7%
+23.1%
-4.%
2.57
GPT
57.7%
95. 7%
81.1%
91.3%
+23.5%
-4.%
3.11
GPT 4.1 mini
39.1%
95.7%
6%%
95.7%
+26.0%
0
3,94
GPT 4.1 nano
11.7%
29.9%
+18.1%
1.82
Gemini 2.0 Flash 23
37.0%
87.2%
82.6%
+50,2%
-17.4%
2.69
Gemini 2.0 Flash Lite
23
54.8%
95.7%
79.0%
95.7%
+24.2%
0
1.72
DeepSeck-VV V3
43
78.3%
87.0%
94.0%
82.6%
+15.7%
-4.3%
15.84
100%
SuTChokKPPT LiM-m---jidde
RvLIM
80%
-20%
"Ihcreass" of
"Decrease" of TNR
-00%
40%
-60%
20%
-80%
SerCheckGP
LUN ajugee
0%
-100%
GPT Target LLMs
06-13
OW
GF
GF-Lie
D8-ya
Target LLMs
(a) The increase of TPR across models.
(b) The decrease of TNR across models.
Figure 3: Performance comparison of different methods in the violation detection task, where QW, GF/GF-Lite, and DS-V3 denote Qwen, Gemini 2.0 Flash/Flash Lite, and DeepSeek- V3, respectively.
4.2 Case study 2: numerical comparison problems
For this study, we apply RvLLM under Level-2 interpretation verify the numerical comparison results produced by various LLMss It is important to note that RvLLM is inherently designed without mathematical solving capabilities and relies solely on logical inference. Without loss of generality, we randomly generate 100 questions following the guideline for increasing the likelihood of incorrect comparison results by LLMs. The specification file used here is the one shown in Figure Again, we use the same model to serve both the target LLM and the perception agent.
Results. Table gives the verification results by RvLLM numerical comparison tasks across various LLMs. Columns Con. and Incon. report the number of cases where RvLLM detects no inconsistencies and where least one inconsistency detected, following the process in Figure 2 The values in parentheses in Column Con. represent cases where the target LLM produces an erroneous comparison result on the original comparison question, yet RvLLM fails to identify any eccomsistencies-typcaaall due to incomplete interpretation by the perception agents. In contrast, the values in parentheses Column Incon. corresponds to cases where the target LLM returns correct comparison result on the original question, but RvLLM indeed detects some inconsistencies. This usually arises from two main reasons: incomplete interpretation, and ii) the target LLM producing incorrect diagnosis on newly-infereed knowledge. Overall, RvLLM effectively identifies erroneous diagnoses by the target LLM in most cases, with exceptions observed only cases for GPT 4.1 nano and mini. Among all tested models, Gemini 2.0 Flash Lite and DeepSeek- V3 show the weakest diagnostic performance, and Qwen 2.5 (7B) has the worst language understanding capabilities, failing all interpretation abstraction. Table presents presents the performance comparison across methods. Consistent with the findings case study 1, we find that RvLLM achieves the best balance, maintaining both high true positive and high true negative rates among all evaluated approaches.

---

Table 2: Verification results by RvLLM over
Table 3: Performance comparison of different
various LLMs for numerical comparison tasks.
methods for numerical comparison tasks.
Target LIMSs
Con. Incon. Fail Time (8)
Target LLMs
Methods
TPR
TNR
Owen 62
93
7
0
5.03
Qwen plus 62
99
1
0
7.01
SeltCheckGPT
196.7%
Qwen turho 62]
94
6(2)
0
2.93
Qwen plus LLM-ux-u-judgel
100%
Owen 2.5 (7B) [62]
0
0
100
N/A
Qwn 2.5 (14B) 662
90
10(7)
5.09
RvLLM
100%
100%
Qwen 2.5 (32B) 62
98
2
4.98
Sel[CheckGPT
100%%
0
Qwen 2.5 (72B) [2
96
4
6.31
GPT 4.1 mini
LLM-as-a-judge
0
100%
GPT [
98
2
4.84
GPT 4.1 mini [
92(1)
8
0
5.37
RvLLM
88.99%
100%
G.T nano
90(3)
10
0
3.73
SeltCheckGPT
87..5%
Gemini 2.0 Flash 23
9.3
7
0
4.94
Gemini Flash
23
LLM-as-aajudgel
100%
Gemini 2.0 Flash Lite 23
52
44
4
4.35
RvLLM
100% 100%
DeepSeek- V3 43
69
31(5)
0
30.87
4.3
Case study 3: inequality solving problems
For this case study, we employ RvLLM under Level-1 interpretation to verify the step-by-step reasoning process of LLMs in inequality-solving tasks. We compile a dataset of 40 inequality questions sourced from A-Level H2 Mathematics examination papers [32] and carefully design three specifications to serve as domain knowledge that RvLLM uses for verification. These specifications consist of basic algebraic inequality properties taught at the junior college level, targeting three common LLM reasoning errors in inequality solving: incorrect factorization, flawed interval analysis, and omission of endpoint or critical point checks. Given the higher interpretation complexity in this case study and the strong language processing capabilities of DeepSeek- V3, we employ it as the perception agent for all LLMs evaluated and Qwen 2.5 (32B) an alternative for comparison.
Results. Given the strong performance of RvLLM in detecting true positives, we focus the evaluation on the questions that the target LLMs answered incorrectly. The results are summarized in Table 4 Column lists the total number of questions for which the target LLM produces incorrect solutions. Columns labeled DS-V3 and QW-32B (spanning Columns 3 to 11) show the number of cases where RvLLM successfully identifies inconsistencies based on the corresponding specifications using DeepSeek-Ve V3 and Qwen 2.5 (32B) as the perception agent, respectively. Values in parentheses indicate false positives-cases where the detected inconsistency does not stem from an actual reasoning error but from inaccuracies of the perception agent during the interpretation abstraction process. Column GT gives the ground truth number of incorrect responses attributable to the rule specifications. It is important to note that we define only three specifications domain knowledge for inequality- solving tasks, which is insufficient to cover all reasoning patterns required for such problems comprehensively. As result, it is expected that RvLLM fails detect a portion of the errors due to the lack of knowledge. The final two columns give the true positive rate of RvLLM with three specifications. We find that RvLLM achieves TPR of up 50% when using DeepSeek- V3 the perception agent. This result underscores both RvLLM's potential to detect reasoning errors- even with limited domain knowledge-and and the critical role of a robust perception agent in boosting overall performance. Although TPR remains below 50% for most models, they rise markedly when restricted to ground truth cases (Column GT), suggesting substantial gains are possible with richer domain knowledge in inequality solving.
5 Related work
LLM testing. Research in this area aims to develop comprehensive benchmarks and systematic evaluation frameworks to assess LLM across general attributes such robustness, fairness, and factual consistency 45] 41 57). Robustness studies examine model resilience to adversarial input,
while faimees evaluations assess bias with respect to sensitive 66 Factual consistency detection, or hallucination detection, focuses on identifying instances in which LLMs produce plausible yet factually incorrect or unsup- ported claims [4] 38 Although large-scale benchmarks like HELM [41] and BIG-bench (54] offer task suites and metrics for performance evaluation, critical challenge remains-Baee the dynamic
paraphrasing, or noise 9 56
66
attributes like gender or race 39

---

Table Verification results by RvLLM inequality solving tasks with three specifications, defining rules related to factorization, interval analysis, and endpoints/critical points checking.
Factorization Error
Interval Error
Endpoints Error
TPR
Target LLMs
Incorrect
DS-V3 QW-32B GT DS-V3 QW-32B GT DS-V3 QW-32B GT
DS-V3
QW-32B
Owen max 62
12
1
1
2
2
3
33.3%
25%
Qwen plus 02
10
1
1
2
0
0
1
2
10%
20%
Qwen turbo 62
0
1
3
2
18.2%
9.1%%
Qwen 2.5 (7B)
62
1
3
3
2
48%
20%
Qwen 2.5 (14B)
02
18
D
Q
1
2(1)
3(1)
2
27.8%
16.7%
Qwen 2.5 (328)
62
16
Q
1
4
2
S
50%
25%
Qwen 2.5 (72B)
62
0
0
33.3%
20%
GPT 4.1
1
I(1)
1
0
0
20%
GPT 4.1 mini
1
0
50%
GPT 4.1 nano 1
10
0
0
0
1
0
20%
Gemini 2.0 Flash 23
5
0
0
0
0
0
20%
Gemini 2.0 Flash Lite 22
6
1
2
0
0
0
16.7%
16.7%
and open-ended nature of real-world deployments complicates the construction of exhaustive and representative test suites.
Runtime verification of LLMs. Runtime verification 6 21 is a dynamic analysis technique that ensures certified system behavior during execution by monitoring traces against formal specifications. Owing to its lightweight nature, runtime verification has inspired multiple efforts to verify LLM-
generated outputs runtime [13 47
46 36). However, existing approaches center on open-domain settings, where specifications are often ambiguous and informal. For instance, SelfCheckGPT 47 and CHECKEMBED 7 operationalize specifications in terms of output stability. More recently. [12] proposes fairness monitoring approach leveraging precisely defined properties in formal specifications. These specifications, informed by linear temporal logic [50) and its bounded metric variant [2). signal a shift towards formal methods for more accurate and dependable runtime verification of LLM behaviors. However, these works primarily focus on general properties and are not well-suited to domain -specff constraints for specialized tasks.
37
Expert systems with NLP. Rule-based expert systems [5 specific problems by coupling knowledge bases with inference engines to emulate expert reasoning for decades of years. To enhance usability, in the 70s, researchers integrated natural language processing (NLP), enabling interaction via simplified language, e.g., SHRDLU [60] in virtual environments and
16 [8] have effectively tackled domain-
MedLEE (35] in clinical text analysis. These systems relied symbolic parsing and controlled
vocabularies but suffered from fragile parsing, limited lexical coverage, and ambiguity, often requiring constrained input or extensive user guidance. Nevertheless, integrating NLP with rule-based reasoning for interactive, user-friendly AI, shaping later Knowledge-basee
provides a key proof-of-concee systems and natural language interfaces. Recently, the rise of LLMs has reinvigorated this paradigm. In this work, we employ a perception LLM to translate the target LLM's context and outputs into formal representations for backend reasoning. An improved version could explore other extensions of Horn clauses beyond those considered here to enhance expressiveness and completeness 4
6 Conclusion
In this work, we present the first runtime verification framework RvLLM for LLMs, which allows the incorporation of domain knowledge. To support this, we design general specification language, ESL, which enables domain experts to formally encode constraints in a lightweight yet expressive manner, supporting the rigorous verification of LLM behavior. We implement the proposed framework as a tool and evaluate its effectiveness on three representative tasks where domain knowledge plays a critical role. For each task, develop tailored specifications grounded in relevant domain expertise. Experimental results indicate that RvLLM effectively leverages expert-defined domain knowledge enable precise runtime verification of LLMs and strike good balance between TPR and TNR, compared to existing runtime methods. However, despite its good performance, the current framework suffers from limited expressiveness by ESL, restricting its ability to encode more complex domain knowledge and behavioral constraints for LLMs. Future work will focus on enriching the specification language with additional operators to improve its expressiveness and generalization.
10

---

7 Acknowledgments
This work was partially funded by the Ministry of Education, Singapore, under its Academic Research Fund Tier 3 (MOET32020-0003), Any opinions, findings, conclusions, or recommendations expressed this material are those of the author(s) and do not reflect the views of the Ministry of Education, Singapore.
References
[1] Achiam, J., Adler. S., Agarwal, S., Ahmad, L., Akkaya, I,, Aleman, F.L., Almeida. D., Altenschmidt, J.,
Altman, S., Anadkat. S., et al.: Gpt-4 technical report. arXiv preprint arXiv:2303.08774 (2023)
[2] Alur, Feder, Henzinger, T.A.: The benefits relaxing punetuality, Journal of the ACM (JACM)
43(1), 116-146 (1996)
[3] Armstrong. K.: Chatgpt: Us lawyer admits using ai case research, httpp://www. bbc. www/neww///c//e/.co srld-us-con waw.-ussaaaaaa-88355350 65735769 (2023)
[4] Babka, M., Balyo, T., Čepek, O., Gurský, Š., Kučera, P., Vlček, V:: Complexity issues related to propagation completeness. Artificial Intelligence 203, 19-34 (2013)
[5] Banerjee, S., Agarwal, A.. Singla, S.: Llms will always hallucinate. and we need to live with this. arXiv preprint ar ar.iv:2409.0577 057446 (2024)
[6] Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. Lectures on Runtime Verification: Introductory and Advanced Topies pp. 1-33 (2018)
[7] Besta, M.. Paleari, L.,, Kubicek, A., Nyczyk, P., Gerstenberger, R., Iff, P.. Lehmann, T., Niewiadomski, H. Hoefler, T.: Checkembed: Effective verification of Ilm solutions open-ended tasks, arXiv preprint arXiv:2406.025: (2024)
Bunel, R., Lu, J., Turkaslan, I., Torr, P.H.S.,, Kohli, P., Kumar, M.P:: Branch and bound for piecewise linear neural network verification. Mach. Learn. Res. 21, 42:1-42:39 (2020)
[9] Cai, R., Song, Z. Guan, D., Chen, Z., Li, Y.. Luo, X., Yi, C., Kot, A.: Benchlmm: Benchmarking
cross-style visual capability of large multimodal models. In: European Conference on Computer Vision. 140-358. Springer (2024)
[10] Cascella, M., Montomoli, J., Bellini, V., Bignami, F.: Evaluating the feasibility of chatgpt in healthcare: an analysis of multiple clinical and research scenarios. Journal of medical systems 47(1), 33 (2023)
[11] Chen, J., Kim, G., Sriram, A., Durrett, G., Choi, E.: Complex claim verification with evidence retrieved in the wild. In: Proceedings of the 2024 Conference of the North American Chapter of the Association Computational Linguistics: Human Language Technologies (Volume Long Papers). pp. 3569-3587 (2024)
[12] Cheng, C.H., Wu, C.,, Ruess, H., Zhao, X., Bensalem. S.: Formal specification, assessment, and enforvement of fairness for generative ais. arXiv preprint 1eXiv:2404.1666 (2024)
[13] Cohen, R., Hamri, M., Geva, M., Gloherson, A.: Lm vs Im: Detecting factual errors via cross examination. In: Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pp- 12621-12640 (2023)
[14] Copi, L.M., Cohen, C., McMahon, K.: Introduction to logic. Routledge (2016)
[15] Daniel, M., Häjek, P., Nguyen, P.H.: Cadiag-2 and mycin-like systems. Artificial Intelligence in Medicine 9()), 241-259 (1997)
[16] Denning, PJJ.: Towards a science of expert systems. IEEE Intelligent Systems 1(02), 80-83 (1986)
[17] Drummond, N., Shearer, R.: The open world assumption. In: eSI workshop: the closed world of databases meets the open world of the semantic weh. vol. 15. (2006)
[18] Durkin, J.: Expert systems: a view of the field. IEEE Intelligent Systems 11(02), 56-63 (1996)
[19] Elboher. Y.Y., Gottschlich, J., Katz, G.: An abstraction based framework for neural network verification. In: Proceedings of the 32nd International Conference Computer Aided Verification. pp. 43 65 (2020)

---

[20] Enderton, H.B.; A mathematical introduction to logic. Elsevier (2001)
[21] Falcone, Y., Havelund, K., Reger, G.: tutorial on runtime verification. Engineering dependable software
systems pp. 141-175 (2013)
[22] Forsyth, R.: Expert systems: principles and case studies. Chapman & Hall, Ltd. (1984)
[23] Gemini, T.: Gemini: A family of highly capable multimodal models (2024),
2312. 11806
[24] Guha, N., Nyarko, J., Ho, D., Ré, C., Chilton, A., Chohlas- Wood, A., Peters, A., Waldon, B., Rockmore, D., Zambrano, D., et al.: Legalbench: A collaboratively built benchmark for measuring legal reasoning in
large language models. Advances Neural Information Processing Systems 36, 44123 44279 (2023)
[25] Hayes-Roth, F., Waterman, D.A., Lenat, D.B.: Building expert systems. Addison-Wesley Longman Publishing Co., Inc. (1983)
[26] Hein, J.L.: Discrete mathematics. Jones & Bartlett Learning (2003)
[27] Hendryeks, D., Burns, C., Basart, S., Zou, A., Mazcika, M., Song, D., Steinhardt, J.: Mcasuring massive multitask language understanding. In: 9th International Conference on Learning Representations, ICLR
2021, Virtual Event, Austria, May 3-7, 2021 (2021)
[28] Hernández-Onan Orallo, J.: The measure of all minds: evaluating natural and artificial intelligence. Cambridge University Press (2017)
[29] Huang, X., Kwiatkowska, M., Wang. S., Wu, M.: Safety verification of deep neural networks. In: Proceed- ings of the 29th International Conference on Computer Aided Verification. pp. 3-29 (2017)
[30] Huang, Y., Bai, Y., Zhu, Z., Zhang, J. Zhang, J., Su, T., Liu, J., Lv, C., Zhang. Y., Fu, Y., et al.: C- eval: multi-level multi-discipline chinese evaluation suite for foundation models, Advances Neural Information Processing Systems 36 (2024)
[31] Jackson, P:: Introduction expert systems (1990)
[32] Junior college test papers in level: A-level, http:p//www..eppppprse...ooooooa (2024)
[33] Kasneci, E., SeBler, K., Kücheeann, S., Bannert, M., Dementieva, Fischer, F., Gasser, U., Groh, G., Günnemann, S., Hüllermeier, E., et al.: Chatgpt for good? on opportunities and challenges of large language models for education. Learning and individual differences 103, 102274 (2023)
[34] Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, MJJ.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Proceedings of the 29th International Conference on Computer Aided Verification, pp. 97-117 (2017)
[35] Krauthammer, M.. Hripesak. G.: A knowledge model for the interpretation and visualization of nlp-parsed discharged summaries. In: Proceedings of the AMIA Symposium, p. 339 (2001)
[36] Laban, P., Kryšciñiski, W., Agarwal, D., Fabbri, A.R., Xiong, C., Joty, S., Wu, C.S.: Llms as factual reasoners: Insights from existing benchmarks and beyond. arXiv preprint arXiv:2305.1452 1304. (2023)
[37] Laban, P., Schnabel, T., Bennett, P.N., Hearst, M.A.: Summac: Re-visiting nli- nli-based models for incon- sistency detection in summarization. Transactions of the Association for Computational Linguistics 10. 163-177 (2022)
[38] Li, Cheng, X., Zhao, W.X., Nie, J.Y., Wen, J.R.: Halueval: A large-scale hallucination evaluation benchmark for large language models. In: Proceedings the 2023 Conference on Empirical Methods in Natural Language Processing, pp. 6449-6464 (2023)
[39] Li, M., Li, L., Yin, Y., Ahmed, M., Liu, Z., Liu, Q.: Red teaming visual language models. In: Findings of the Association for Computational Linguistics ACI 2024. pp. 3326-3342 (2024)
[40] Li, N., Li, Y., Liu, Y., Shi, L., Wang, K., Wang, H.: Drowzee: Mctamorphic testing for fact-conflicting hallucination detection in large language models. Proccedings of the ACM on Programming Languages 8(OOPSLA2), 1843-1872 (2024)
[41] Liang, P., Bommasani. R., Lee. T., Tsipras, D., Soylu, D., Yasunaga, M.. Zhang. Y., Narayanan, D., Wu, Y.,
Kumar, A., al.: Holistic evaluation of language models, arXiv preprint X.X.:221110911110 (2022)
12

---

[42] Lin. S., Hilton, J., Evans, O.: Truthfulqa: Measuring how models mimic human falsehoods. In: Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume I: Long Papers). pp. 3214-3252 (2022)
[43] Liu, A.. Feng, B., Xue, B., Wang, B., Wu, B., Lu, C., Zhao, C., Deng. C., Zhang, C., Ruan, C.,, et al.: Deepseek-v3 technical report. arXiv preprint arXiv:2412.19493 (2024)
[44] Liu, J., Xia, C.S., Wang, Y., Zhang, L.: Is your code generated by chatgpt really correct? rigorous evaluation of large language models for code generation. Advances Neural Information Processing Systems 36, 21558 21572 (2023)
[45] Liu. Y., Yao. Y., Ton. J.F., Zhang. X., Guo, R.. Cheng, H., Klochkov, Y., Taufiq, M.F. Li, H.: Trust- worthy Ilms: a survey and guideline for evaluating large language models' aligument, arXiv preprint arXiv:2308.053/1 003704 (2023)
[46] Luo, Z., Xie, Q. Ananiadou, S.: Chatgpt as a factual inconsistency evaluator for text summarization. arXiv preprint 1xXiv2203311662 (2023)
[47] Manakul, P., Liusie, A., Gales, M.: Selfcheckgpt: Zero-resource black-box hallucination detection for generative large language models. In: Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pp. 9004-9017 (2023)
[48] Narodytska, N., Kasiviswanathan, S.P., Ryzhyk, L.. Sagiv, M.. Walsh, T.: Verifying properties of binarized deep neural networks. In: Proceedings of the AAAI Conference Artificial Intelligence, pp. 6615-6624 (2018)
[49] Payne, K.: An ai chatbot pushed teen kill himself, lawsuit against its creator alleges. https: //apnews htt.///aaaaaccecccaooooooooooooa ai-lawuut suicide-- teen- artiifical--itelliggae 144ad577200822244cc0000044444400 (2024)
[50] Pnueli, A.: The temporal logic of programs. In: 18th annual symposium on foundations of computer
science (sfes 1977). pp. 46-57. icce (1977)
[51] Rapid transit systems regulations (revised edition). https://sso. agw.soo.gc.goo..... http://ss..aggc.ooo../////////// (1997)
[52] Russell, S.J., Norvig, P:: Artificial intelligence: a modern approach, pearson (2016)
[53] Shoenfield, J.R.: Mathematical logic. AK Peters/CRC Press (2018)
[54] Srivastava, A., Rastogi, A., Rao, A., Shoeb, A.A.M., Abid, A., Fisch, A., Brown, A.R., Santoro, A., Gupta, A., Garriga-Alonso, et al.: Beyond the imitation game: Quantifying and extrapolating the capahilities of language models. arXiv preprint arXiv:2206. (2022)
[55] Thirunavukarasu, A.J., Ting, D.S.J., Elangovan, K., Gutierrez, L., Tan, T.F., Ting, D.S.W.: Large language models in medicine. Nature medicine (8)., 1930-1940 (2023)
[56] Tu, H., Cui, C., Wang, 7., Zhou, Y., Zhao, B., Han, J., Zhou, W., Yao, H., Xic, C.: How many unicorns in this image? a safety evaluation benchmark for vision llms, arXiv preprint arXiv:231 1.110011111111111111111111111111 (2023)
[57] Wang, B., Chen, W., Pei, H., Xie, C.,, Kang, M., Zhang, C., Xu, C., Xiong, Z., Dutta, R., Schaeffer, R., et al.: Decodingtrust: comprehensive assessment of trustworthiness gpt models. In: NeurIPS (2023)
[58] Wang, H., Zhang, A., Duy Tai, N., Sun, J., Chua, T.S., et al.: Ali-agent: Assessing lims' alignment with human values via agent-based evaluation. Advances in Neural Information Processing Systems 37, 99040-99088 (2024)
[59] Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, CJ., Kolter, J.Z.: Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems 34 (2021)
[60] Winograd, T.:
Procedures as representation for data in computer program for understanding natural language. Tech. rep. (1971)
[61] Xu, Z., Jain, S., Kankanhalli, M.: Hallucination is inevitable: An innate limitation of large language models. arXiv preprint arXiv:2401. 11817 (2024)
[62] Yang, A., Yang. B., Zhang, B., Hui, B., Zheng, B., Yu, B., Li, C., Liu, D., Huang, F., Wei, H., et al.: Qwen2. technical report. arXiv preprint 15115 (2024)
13

---

[63] Zhang, H., Stickely, M.E.: An efficient algorithm for unit propagation. Proc. of AI-MATH 96 (1996)
[64] Zhang, Y., Emma, S.Y., En, A.I.J., Dong, J.S.: Ryllm: Lim runtime verification with domain knowledge. arXiv preprint arXiv:2505. 18585 (2025)
[65] Zhang, Y., Zhao, Z., Chen, G., Song. F., Chen, T.: BDD4BNN: A bdd-based quantitative amalysis framework for binarized neural networks. In: Proceedings of the 33rd International Conference Computer Aided Verification (CAV). pp. 175-200 (2021). https://doi.org/ http://oo...rr/0..000////1/1-3-0 10000998--3-030-86685-3
[66] Zhang, Y., Huang, Y., Sun, Y., Liu, C., Zhao, 7., Fang. 7., Wang. Y., Chen, H., Yang. X., Wei, X., al.: Multitrust: A comprehensive benchmark towards trustworthy multimodal large language models. Advances in Neural Information Processing Systems 49279-49388 (2024)
[67] Zhong, W., Cui, R., Guo, Y., Liang. Y., Lu, S., Wang. Y., Saied, A., Chen, W., Duan, N.: Agieval: human- centric benchmark for evaluating foundation models. In: Findings of the Association Computational Linguistics: NAACL 2024. pp. 2299-2292222222222 2314 (2024)
[68] Zhou, K., Zhu, Y., Chen, Z., Chen, W., Zhao, W.X., Chen, X., Lin, Y. Wen, J.R., Han, J.: Don't make your Ilm an evaluation benchmark cheater. arXiv preprint arXiv:231 1.00964 (2023)
14

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: We made the claim that: i) we introduce a novel specification language ESL for experts to encode their domain-expertise into specification rule for checking the LLM behavior (design details are given in Section(2) 2), and ii) design an innovative runtime verification framework RvLLM for LLMs with domain knowledge encoded in ESL (design
details are given in Section The experimental results are shown in Section 4
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. It is fine to include aspirational goals as motivation long it is clear that these goals are not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: Limitations are discussed in Section
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or speech-to-text system might not be used reliably provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't acknowledged
the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
15

---

Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [NA]
Justification:
We do not include theoretical results in this paper.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but they appear in the supplemental material, the authors are encouraged to provide short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification: We disclose detailed information for reproducing the main experimental results in the long-version preprint [64]. provided as separate file.
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, a No answer to this question will not perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to model. In general. releasing code and data often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
specific model and empirical evaluation, may
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) the contribution is a new model (c.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
16

---

reproducible, they 5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, described in supplemental material?
Answer: [Yes]
The code and data will be open-sources and made available on our website once they are properly organized. We also upload the preliminary version (of code) as a zip file as supplemental materials in the submission.
Justification:
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please the NeurlPS code and data submission guidelines (https://nips cc/pu blic/ httgg//ddee/deeuubmiieeseeeeeeee
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https http:ppwlllgggide/eeeoeooa/
/
cettsummmissooonlo wwwsonoliicyyyo... for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (c.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: The experimental settings and implementation details are described in Section and in the long-version preprint [64], provided as a separate PDF.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core the paper to a level of detail that is necessary appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: For all main experiments, we executed RvLLM multiple times (at least twice) assess potential variations in the results. Given that the proposed method employs fixed framework with deterministic reasoning, any observed variability can only originate from the perception agent's outputs. Our analysis confirms that such variability is minimal in practice, to the extent that it can be considered negligible. We include such claim in the appendices in the long-version preprint [64
Guidelines:
17

---

The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by enror bars, confi-
dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g.. Normally distributed errors).
should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that out of range (e.g. negative етror rates).
If error bars are reported in tables or plots. The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
We discuss computing resources in Section
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary failed experiments that didn't make into the paper).
9. Code ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification:
The research conducted in the paper conforms with the NeurIPS Code of
Ethics.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive socictal impacts and negative socictal impacts of the work performed?
Answer: [Yes]
18

---

Justification: The potential societal impacts are discussed in appendices in the long- versionsion preprint [64]
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g.. disinformation, generating fake profiles, surveillance), faimess considerations (e.g., deploymeet of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper deseribe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification:
We do not pose such risks in this paper.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: For all the data used in this work, we give the citation properly.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset used and, possible, include URL.
19

---

The name of the license (e.g., CC-BY 4.0) should be included for each asset. For scraped data from a particular source (c.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithoom wwwde.. com com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information is available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
Justification:
We do not release new assets.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA].
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According the NeurlPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
20

---

Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if' applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Question:
Answer: [Yes]
Justification: We have describe our usage of LLMs throughout the experiments part in Dection4aas well as appendices in the long-version preprint [64]
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, non-standard components.
Please refer to our LLM policy lhttps://neurips.co / http://urrpppccccooomeeeee/e//// for what should or should not be described.
21


Reviews:
[{"review_id": "AGztZLeVoy", "reviewer": "Reviewer_ywvD", "summary": "The paper introduces RvLLM, a runtime verification framework that leverages domain-specific knowledge to validate large language model (LLM) outputs. The authors design a lightweight Expert Specification Language (ESL), enabling experts to express constraints as simple pairs (rule to constraint). RvLLM’s pipeline comprises four stages: interpretation abstraction, rule normalisation, forward chaining, and query generation, to detect logical inconsistencies and then issue follow-up queries when contradictions arise. The framework is evaluated on three representative tasks, including violation detection against the Singapore Rapid Transit Systems Act, numerical comparison, and inequality solving, demonstrating substantial improvements in error detection across a variety of LLMs.", "questions": "1. One thing unclear to me is: Regarding the term verification, does RvLLM have the mathematical guarantee like formal verification, i.e., regarding soundness and completeness, or is it more like validation/detection but combining with domain knowledge?\n2. What if the domain knowledge is insufficient?", "limitations": "Yes", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n\n1. By combining formally defined ESL rules with lightweight runtime checks, RvLLM bridges the gap between general-purpose LLM error detection and domain-specific validation, like the combination of neural-symbolic with LLM, which is interesting. \n2. RvLLM was tested on legal compliance, numerical comparison, and inequality solving with a diverse set of state-of-the-art and smaller LLMs.\n3. The final stage, 'Query Generation', would be more valuable  if it could be used to analyse the inconsistency that comes with some explanation \n\nWeaknesses:\n1. Evaluation compares only to raw LLM outputs, omitting other runtime or hallucination-detection methods that the authors mentioned in the paper, such as SelfCheckGPT or CHECKEMBED, \n2. Although per-scenario times are reported (Table 1), the paper does not analyse throughput or resource usage for large-scale deployments\n3.  ESL currently handles simple logical and arithmetic predicates; it is a bit unclear to me of its ability to encode temporal, probabilistic, or fuzzy constraints.", "was_revised": true, "final_justification": "I maintain my original score as discussed with the authors/AC. The authors are encouraged to use a more suitable term, e.g., “runtime validation”, or state very clearly in the revised version that the results are subject to the assumption of certain domain knowledge, and highlight the potential risk of unsoundness; also, the limitations of the generalisation of ESL should be further explained in the paper.", "rebuttal": "## **Reply to Reviewer ywvD**\n\nWe sincerely appreciate the reviewer’s thoughtful feedback and constructive engagement with our work. In the following sections, we address each of the raised concerns and questions in detail.\n\n### **Weakness W.1: Comparison to other baseline methods**\n\nTo ensure a comprehensive evaluation, we conduct additional experiments covering all three case studies to compare our tools with 1) SelfCheckGPT (with NLI option and sampling time N = 4) and 2) an llm-as-judge (deepseek-chat) baseline method, where we explicitly encode domain-specific natural language constraints into the prompt. Due to the substantial computational overhead and API costs associated with large-scale evaluation, we opt for a cost-efficient model variant (cheaper api price). The comparative results are presented below. Note that we also report the token usage for case study 3, given the complexity and scalability of the task.\n\n#### **For Case Study 1: Violation detection against Singapore Rapid Transit Systems Act**\n\n| verified model  | Method | TPR Inc. vs Raw LLM outputs | TNR Dec. vs Raw LLM outputs|\n| - | - | - | - |\n| Qwen-plus  | SelfCheckGPT   | +41.6%  | -100%  |\n|  | LLM as judge  | +30.9%    | -56.5% |\n|  | **RvLLM**    | +23.5%    | -0%    |\n| Qwen-turbo   | SelfCheckGPT   | +60.9%    | -100%  |\n|   | LLM as judge     | +38.1%    | -47.8% |\n|     | **RvLLM**    | +35.9%    | -0%    |\n| gpt-4.1-mini      | SelfCheckGPT   | +60.9%    | -96%  |\n|    | LLM as judge    | +22.4%    | -16%   |\n|   | **RvLLM**  | +26.0%    | -3.4%  |\n| gemini-2.0-flash  | SelfCheckGPT  | +63.0%    | -100%  |\n|   | LLM as judge      | +7.8%     | -12%   |\n|    | **RvLLM**   | +50.81%   | -17%   |\n| gemini-2.0-flash-lite    | SelfCheckGPT   | +45.2% | -96% |\n|   | LLM as judge    | +18.1%    | -20%   |\n|    | **RvLLM**   | +24.9%   | -0.3%   |\n| deepseek-chat     | SelfCheckGPT   | +21.7%   | -87.0%  |\n|    | LLM as judge  | +9.6% | -65.2%  |\n|    | **RvLLM**     | +15.7%       | - 4.3%   |\n\nWe observe that RvLLM achieves more stable performance across varied models, consistently maintaining a relatively low TNR drop while improving TPR high. In contrast, SelfCheckGPT often achieves the highest TPR increases simply because it tends to label nearly all outputs as “hallucinations” in our domain-specific settings, resulting in near-zero TNR. This behavior is expected, as SelfCheckGPT relies solely on output stability without incorporating domain knowledge. It does not encode or evaluate domain-specific rules, constraints, or context-sensitive reasoning, making it more suitable for open-domain generation tasks.\n\nAs for LLM-as-judge method, we find it can achieve competitive TPR compared to RvLLM. However, its performance is also unreliable, with TPR gains typically accompanied by significant TNR drops. In contrast, RvLLM remains a better balance between TPR and TNR. This is because RvLLM leverages the LLM primarily for text understanding/reading, while delegating rule-based domain-related reasoning to an external reasoning engine, leading to more reliable and interpretable outcomes. \nWe also include two additional comparison experiments corresponding to Case Studies 2 and 3.\n\n#### **For Case Study 2**:\n| verified model  | Method | TPR | TNR |\n| - | - | - | - |\n| Qwen-plus   | SelfCheckGPT    | 0  | 96.7%  |\n|   | LLM as judge     | 0    | 0 |\n|   | **RvLLM**    | 1    | 1  |\n| Qwen-turbo  | SelfCheckGPT   | 1    | 7.29%  |\n|  | LLM as judge      | 0    | 0 |\n|    | **RvLLM**    | 1    | 97.9%  |\n| gpt-4.1-mini  | SelfCheckGPT  | 1    |0  |\n|   | LLM as judge      | 1    | 1  |\n|   | **RvLLM**    | 88.9%    | 1 |\n| gemini-2.0-flash  | SelfCheckGPT   | 87.5%   | 0%  |\n|   | LLM as judge  | 1     | 1   |\n|    | **RvLLM**    | 1   | 1   |\n| gemini-2.0-flash-lite    | SelfCheckGPT  | 1 | 0 |\n|    | LLM as judge    | 1    | 1  |\n|  | **RvLLM**  | 1   | 1   |\n| deepseek-chat     | SelfCheckGPT   | 1   | 0  |\n|   | LLM as judge   | 1 | 1  |\n|   | **RvLLM**   | 1      | 93.2% |\n\n#### **For Case Study 3**:\n\n| verified model  | Method | TPR | TNR | Token Usage Per Task|\n| - | - | - | - | - |\n| Qwen-turbo   | SelfCheckGPT (NLI)   | 1    | 0  | 9850 |\n|   | SelfCheckGPT (Prompt)   | 1    | 0  | 100527|\n|   | LLM as judge      | 1    | 0 | 1466|\n|    | **RvLLM**    | 18.2%    | 94.4%  | 4805 |\n| gpt-4.1-mini  | SelfCheckGPT (NLI)   | 1    | 2%  | 10373 |\n|  | SelfCheckGPT (Prompt)   | 1    | 0  | 158504|\n|   | LLM as judge  | 1    | 0 |  2479 |\n|   | **RvLLM**   | 50%  | 84.2% | 5683 |\n\nNote that, in the current status of rebuttal, we do not provide more comparison studies to CheckEmbed mentioned in the reviews for the following several well-justified reasons:\n\n- First, both CheckEmbed and SelfCheckGPT share the same fundamental methodology of detecting hallucinations through output stability analysis, which assumes stable outputs are less likely to be hallucinated. While this approach proves effective for general NLP tasks like summarization, it demonstrates significant limitations when applied to our domain-specific constraint verification task. Most critically, stability-based methods are fundamentally incapable of: (1) reliably detecting constraint violations, or (2) identifying the precise sources of errors - both of which constitute essential requirements for our application.\n\n- Moreover, several practical considerations further motivated our decision. The original CheckEmbed paper reports performance comparable to or slightly worse than SelfCheckGPT and LLM-as-judge methods in stability detection. Additionally, CheckEmbed currently exists only as a non-peer-reviewed preprint on arXiv. From an implementation perspective, the tool's tightly coupled architecture presents substantial engineering challenges for integration, particularly given the already significant computational costs incurred (SelfCheckGPT alone required approximately 20 million tokens across our three benchmarks). These factors collectively made CheckEmbed adaptation impractical within the rebuttal timeframe.\n\n- Nevertheless, in direct response to the reviewer's constructive feedback, we have expanded our experimental analysis during the rebuttal phase to include comprehensive comparisons with SelfCheckGPT and LLM-as-judge (implemented via DeepSeek-Chat). We maintain that these comparisons adequately demonstrate our method's superior effectiveness against this class of stability-based detection approaches. Should the reviewer consider it essential, we would be pleased to conduct additional CheckEmbed experiments during the post-deadline discussion period, contingent upon the method's continued relevance to our evaluation framework.\n\n### **Weakness W.2: Throughput and resource usage**\n\nWe collect the info of our token usage (rounding to the nearest integer) on average for each single verification task in the three case studies as follows, where 1) Raw LLM denotes the tokens used for the initial query; and 2) the RvLLM denotes the tokens used by the LLM oracle in our verification framework.\n\n| Case Study 1 | Case Study 2 | Case Study 3 |\n| - | - | - |\n| 214 (Raw LLM) + 808 (RvLLM) | 36 (Raw LLM) + 1190 (RvLLM) | 1661 (Raw LLM) + 3669 (RvLLM) | \n\n### **Weakness W.3: Generalization of ESL**\n\nWe sincerely thank the reviewer for their valuable insights concerning the potential generalization of ESL to more expressive formal logic systems. The current implementation of ESL is limited to supporting basic logical and arithmetic predicates. Enhancing ESL's expressiveness constitutes a fundamental research challenge in LLM runtime verification – a direction we explicitly identify as important future work. We also give a discussion in the conclusion.\n\nHowever, we also acknowledge that monitoring cost can be higher given the more complicated syntax and logic, and that greater involvement from domain experts may be required to define fine-grained constraints. Indeed, the user-friendliness and the expressiveness also exist in a trade-off, which is indeed an interesting and meaningful research work.\n\n### **Question Q.1: Mathematical guarantee**\n\nWhen the interpretation abstraction from natural language to ESL is correct (NL to ESL), RvLLM provides rigorous mathematical guarantees analogous to formal verification methods. Specifically, it offers complete verification coverage with respect to all domain-specific constraints encoded in ESL. As discussed in W.3, the accuracy of this interpretation abstraction is crucial - more complex logical syntax introduces greater challenges in maintaining abstraction fidelity. This fundamental trade-off between expressiveness and verifiability has motivated our current focus on simpler logical predicates and arithmetic relations in this initial framework.\n\n### **Question Q.2: What if the domain knowledge is insufficient?**\n\nWhen knowledge is insufficient, some misconduct will not be verified as an error and marked as safe, i.e., a complete but unsound verification result. \n\nIn practical applications, exhaustive and sufficient encoding of all relevant domain knowledge in a single iteration proves infeasible. A principal advantage of our framework lies in its ability to operate effectively without requiring complete domain knowledge a priori. Specifically, the system can perform verification based on currently specified constraints while supporting incremental integration of additional constraints as new domain knowledge is acquired. This design facilitates a scalable and pragmatic approach for progressively developing comprehensive domain specifications.\n\nCompared to approaches such as red teaming or dataset-based testing, our method supports incremental expansion of domain knowledge in a structured and reusable way. Moreover, the knowledge encoding process in our framework is typically a one-time effort, after which the constraints can be consistently reused across tasks and models, enabling systematic and ongoing refinement of model behavior."}, {"review_id": "16K8ZlpUXe", "reviewer": "Reviewer_9HFq", "summary": "This paper introduces RvLLM, a runtime verification framework tailored for LLMs to ensure reliable outputs. Specifically, a general language called ESL is proposed for encoding rule-based domain expertise, and ESL integrates natural language and formal logic for answer verification. Experimental results conducted on three representative tasks demonstrate the effectiveness of the proposed method.", "questions": "- Are ESL specifications authored entirely by human experts, or is there an automated or semi-automated pipeline to assist their creation?\n- Could you include additional examples or real-world scenarios to illustrate ESL’s expressiveness and breadth?", "limitations": "Yes", "rating": 3, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths: \n- The introduction of ESL offers a lightweight, intuitive way for domain experts to encode rich, domain-specific constraints\n- Experimental results on 3 representative tasks  demonstrate the effectiveness of the proposed method.\n\nWeaknesses:\n- The writing in this paper can be improved a lot. There are too many symbolic notations in the paper. In addition, introducing a concrete, running example in the Introduction would ground readers and improve accessibility.\n- ESL’s coverage of domain knowledge is unproven. There is no evaluation demonstrating its reliability across varied or unforeseen cases. I am not sure if every domain constraint can represented using ESL.\n- The evaluation uses only three carefully selected examples, raising concerns about the approach’s generalizability.", "was_revised": true, "final_justification": "My concerns are largely resolved after discussing with authors. The only concern remains is the expert effort required to apply ESL across different domains, and I would like to see more detailed statistics of this. I will increase my score from 2->3.", "rebuttal": "## **Reply to Reviewer 9HFq**\n\nWe sincerely appreciate the reviewer's valuable feedback. Below, we provide detailed responses to each concern along with additional experimental evidence to substantiate our methodology.\n\n### **Weakness 1. Writing issues**\n\nIn the current version, we have intentionally limited symbolic notation to only those elements essential for validating the methodological rigor of our approach, which is sufficient for validating the solidity of the paper's methodology. We will incorporate additional explanatory text in the appendix.\n\nTo enhance readability, we have included a concrete running example throughout the methodology section (Figure 2). \n\nIn response to the reviewer's suggestion, we are happy to either: 1) Relocate this example to the introduction section for earlier understanding, or 2) Introduce an additional illustrative example to improve conceptual understanding. \n\n\n### **Weakness 2.  Not sure if every domain constraint can be represented using ESL.**\n\nWe understand the reviewer's concern that no evaluation demonstrating ESL's reliability across varied or unforeseen cases is provided in our paper. However, indeed, designing a specification logic or language to express every domain constraint is impractical. The logic (syntax and operators) should also be dedicated to the scenario complexity level and the questions of interest. Moreover, a higher complicated specification language will face : (1) hard in hand (user-friendliness consideration), (2) requiring a more computationally intensive solving algorithm, and limit the runtime efficiency.\n\nTo illustrate the usefulness of ESL, we use daily scenarios in real life, including the Rapid Transit Systems Act, inequality solving problems, and number comparison tasks. To show the usability further, during the rebuttal period, we also include another real-world scenario about the Liquor consumption law in Singapore. By encoding related laws with ESL, RvLLM can successfully help LLMs do the violation detection tasks and monitor LLM's response related to these laws. We test on 200 liquor-consumption scenarios collected over the internet, and the TPRs are improved by up to 24.5% using RvLLM.\n\n\nClarify: we enable the natural language description into our ESL syntax, hence giving a large extent of flexibility to the expert or users to define their domain constraints they would like to set limitations on the LLM behavior.\n\n\n### **Weakness 3. Only three examples in our evaluations.**\n\nThe reason why we use three examples is not because we can only fit these three, but because at the paper submission, we successfully collected expertise from three domains. Note that each additional benchmark/domain required dedicated domain expertise to encode the constraints, as well as the testing benchmark to evaluate. \nWe would be happy to keep incorporating more domain-expertise incrementally (encoded by ESL),  collecting and enlarging our domain-expertise benchmark, i.e., exhaustive test cases given the domain-expertise settings.\n\nTo eliminate the reviewer's concern, in this rebuttal period, we also collected Singapore law about \"Liquor consumption\" on the official site, and collected 200 alcohol consumption situations on the internet to act as our evaluation benchmark. We conduct similar experiments following the experiment setting as the Case Study 1. The experimental results are given in the following table.\n\n| verified model  | LLM: TPR | LLM + RvLLM: TPR |\n| - | - | - |\n| qwen-max              | 67.5%     |   76.5%   |  \n| qwen-plus             | 66.3%     |   88.5%   |\n| qwen-turbo            | 92%       |   93.5%   |\n| gpt-4.1               | 72%       |   82% |\n| gpt-4.1-mini          | 66%   | 76.5% |\n| gpt-4.1-nano          | 20.1% | 37.7% |\n| gemini-2.0-flash      | 60.5% | 85%   |\n| gemini-2.0-flash-lite | 81%   | 81%   |\n| deepseek-chat         | 91.5% | 94.5% |\n\n\n### **Question 1. Are ESL specification authored entirely by human experts?**\n\nESL specifications are authored by human experts by default. However, to reduce their workload, experts may leverage modern AI tools, such as LLMs, to generate initial drafts of specifications, which are then required to be manually reviewed and refined. This would help avoid writing ESLs entirely from scratch, while ensuring correctness.\n\nIt is important to emphasize that fully automated generation of formal specifications remains an open challenge: no existing method can guarantee both syntactic and semantic correctness of the fully-automated generated specifications. As such, human oversight remains essential in the specification creation process.\n\n\nFinally, we stress that the need for human-authored specifications is not a new challenge introduced in our work. Specification authoring has long been a fundamental requirement in the formal methods and model checking communities. Across all existing verification and model checking tools, specifications must be written by users to accurately encode the properties they wish to verify. Our work follows this established practice.\n\n\n### **Question 2. Include additional examples or real-world scenarios to illustrate ESL's expressiveness and breadth.**\n\n\nGiven the limited rebuttal time, we include an additional example, i.e., **Singapore alcohol drinking law** (used in real-world scenarios), to illustrate the real-world usage of RvLLM. Once again, we claim that we add this example is not because this is the only fitting scenario, but the one currently we can easily obtain the related domain expertise and collect benchmarks online in time. Also note that, our case study 1 and case study 3 are all based on domain expertise in real-world scenarios, and case study 2 comes from a notorious LLM hallucination on the number comparison task, which is also an interesting real-world problem when using LLM.\n\nAlso, note that **we have provided detailed ESL encoding examples for all three real-world scenario case studies in the supplementary**."}, {"review_id": "89JaRSEvkZ", "reviewer": "Reviewer_3yxj", "summary": "This paper introduces RvLLM, a runtime verification framework for Large Language Models (LLMs), together with a lightweight Expert Specification Language (ESL). ESL enables domain experts to define task-specific rules in a hybrid syntax combining natural language and predicate logic. RvLLM operates in four stages: interpretation, rule normalization, forward chaining, and query generation. It dynamically detects inconsistencies between LLM outputs and expert-defined rules, optionally re-querying the model to verify critical facts. The framework is evaluated across three safety-critical scenarios—Singapore subway regulation checking, numerical comparison, and algebraic inequality solving—achieving substantial improvements in error detection (e.g., up to 50.2% increase in true positive rate for violation detection). Code and datasets are publicly released.", "questions": "Q1: Current examples mainly show single-premise, single-conclusion implication rules. Can ESL support more complex constructs, such as quantifiers, temporal logic, or coreference? Please discuss plans for syntax extension and usage in realistic regulation/finance corpora.\n\nQ2: Please include misssing ablations.", "limitations": "yes.", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n\nClarity: Well-structured.\n\nSignificance: Runtime verification fills a critical gap for high-stakes applications like compliance and finance.\n\nOriginality: First to combine domain rule authoring and runtime validation in a unified LLM-centric framework; the query-to-refute strategy is particularly insightful.\n\n\nWeaknesses:\n\nQuality: Lacks quantitative comparison with recent verification or self-checking baselines such as SelfCheckGPT or CHECKEMBED.\n\nSignificance: Some cases take 15–30 seconds per output, limiting real-time use.", "was_revised": true, "final_justification": "Borderline Accept (4). The paper presents an innovative, well-articulated approach to LLM verification, with sound methodology and promising results. The weaknesses (efficiency, expressiveness) are not dealbreakers, but they do limit immediate applicability.\n\nAuthors are encouraged to:\n\n- Extend ESL toward richer logic fragments.\n\n- Improve runtime performance (e.g., caching, faster perception models).\n\n- Apply RvLLM to broader, more realistic domains.", "rebuttal": "## **Reply to Reviewer 3yxj**\n\n\nWe sincerely appreciate the reviewer's insightful feedback. We provide a detailed response along with more experimental results to address the raised concerns as follows.\n\n\n### **Weakness 1. Quantitative comparison with recent baselines.**\n\nBefore presenting the comparative results, we would like to clarify the novel contributions of our work. To our knowledge, this work represents the first framework enabling runtime verification of LLMs against domain-specific knowledge, where said knowledge can be: 1) **incrementally** encoded, 2) **in an offline manner** using a user-defined specification language ESL. ESL uniquely bridges natural language and formal specifications, achieving an optimal balance between usability and mathematical rigor.\n\n\nExisting verification approaches, such as self-checking-based methods, operate under the fundamental assumption that \"output stability == non-hallucination\". While these methods can detect the presence or likelihood of hallucinations in a more general setting, RvLLM offers distinct advantages:\n\n- Verification against domain-specific constraints\n\n- Precise identification of error sources\n\n- Explanation of why outputs violate encoded knowledge\n\n\nFor a comprehensive comparison, we also conduct additional experiments with SelfCheckGPT and llm-as-judge:\n\n1) SelfCheckGPT (all embedding options: BERTScore, N-gram, NLI, NQA, and Prompt-based). Sampling size fixed at N=4 due to computational constraints.\n\n2) LLM-as-judge approach. We use DeepSeek-Chat as the judger, which demonstrated superior performance in our Case studies 1,2,3's results, and we also use it as a perception model in our Case study 3. When using deepseek-chat as the judge, we encode our natural language described domain constraints into the judge prompts.\n\n\nHere we present our experiment results:\n\n#### **For Case Study 1: Violation detection against Singapore Rapid Transit Systems Act**\n\n| verified model  | Method | TPR Inc. vs Raw LLM outputs | TNR Dec. vs Raw LLM outputs|\n| - | - | - | - |\n| Qwen-plus         | SelfCheckGPT   | +41.6%  | -100%  |\n|                   | LLM as judge    | +30.9%    | -56.5% |\n|                   | **RvLLM**              | +23.5%    | -0%    |\n| Qwen-turbo        | SelfCheckGPT   | +60.9%    | -100%  |\n|                   | LLM as judge     | +38.1%    | -47.8% |\n|                   | **RvLLM**              | +35.9%    | -0%    |\n| gpt-4.1-mini      | SelfCheckGPT   | +60.9%    | -96%  |\n|                   | LLM as judge    | +22.4%    | -16%   |\n|                   | **RvLLM**              | +26.0%    | -3.4%  |\n| gemini-2.0-flash  | SelfCheckGPT  | +63.0%    | -100%  |\n|                   | LLM as judge      | +7.8%     | -12%   |\n|                   | **RvLLM**              | +50.81%   | -17%   |\n| gemini-2.0-flash-lite    | SelfCheckGPT   | +45.2% | -96% |\n|                   | LLM as judge    | +18.1%    | -20%   |\n|                   | **RvLLM**                | +24.9%   | -0.3%   |\n| deepseek-chat     | SelfCheckGPT   | +21.7%   | -87.0%  |\n|                   | LLM as judge  | +9.6% | -65.2%  |\n|                   | **RvLLM**     | +15.7%       | - 4.3%   |\n\n\n\nWe observe that RvLLM achieves more stable performance across varied models, consistently maintaining a relatively low TNR drop while improving TPR high. In contrast, SelfCheckGPT often achieves the highest TPR increases simply because it tends to label nearly all outputs as “hallucinations” in our domain-specific settings, resulting in near-zero TNR. This behavior is expected, as SelfCheckGPT relies solely on output stability without incorporating domain knowledge. It does not encode or evaluate domain-specific rules, constraints, or context-sensitive reasoning, making it more suitable for open-domain generation tasks.\n\n\nAs for LLM-as-judge method, we find it can achieve competitive TPR compared to RvLLM. However, its performance is also unreliable, with TPR gains typically accompanied by significant TNR drops. In contrast, RvLLM remains a better balance between TPR and TNR. This is because RvLLM leverages the LLM primarily for text understanding/reading, while delegating rule-based domain-related reasoning to an external reasoning engine, leading to more reliable and interpretable outcomes.\n\n\n We also include two additional comparison experiments corresponding to Case Studies 2 and 3.\n\n\n#### **For Case Study 2:**\n\n| verified model  | Method | TPR | TNR |\n| - | - | - | - |\n| Qwen-plus         | SelfCheckGPT    | 0  | 96.7%  |\n|                   | LLM as judge     | 0    | 0 |\n|                   | **RvLLM**                | 1    | 1  |\n| Qwen-turbo        | SelfCheckGPT   | 1    | 7.29%  |\n|                   | LLM as judge      | 0    | 0 |\n|                   | **RvLLM**                | 1    | 97.9%  |\n| gpt-4.1-mini      | SelfCheckGPT  | 1    |0  |\n|                   | LLM as judge      | 1    | 1  |\n|                   | **RvLLM**                | 88.9%    | 1 |\n| gemini-2.0-flash  | SelfCheckGPT   | 87.5%   | 0%  |\n|                   | LLM as judge  | 1     | 1   |\n|                   | **RvLLM**           | 1   | 1   |\n| gemini-2.0-flash-lite    | SelfCheckGPT  | 1 | 0 |\n|                   | LLM as judge    | 1    | 1  |\n|                   | **RvLLM**              | 1   | 1   |\n| deepseek-chat     | SelfCheckGPT   | 1   | 0  |\n|                   | LLM as judge   | 1 | 1  |\n|                   | **RvLLM**   | 1      | 93.2% |\n\n\n#### **For Case Study 3:**\n\n\n| verified model  | Method | TPR | TNR | Token Usage Per Task|\n| - | - | - | - | - |\n| Qwen-turbo        | SelfCheckGPT (NLI)   | 1    | 0  | 9850 |\n|                   | SelfCheckGPT (Prompt)   | 1    | 0  | 100527|\n|                   | LLM as judge      | 1    | 0 | 1466|\n|                   | **Ours**              | 18.2%    | 94.4%  | 4805 |\n| gpt-4.1-mini      | SelfCheckGPT (NLI)   | 1    | 2%  | 10373 |\n|                   | SelfCheckGPT (Prompt)   | 1    | 0  | 158504|\n|                   | LLM as judge      | 1    | 0 |  2479 |\n|                   | **Ours**              | 50%  | 84.2% | 5683 |\n\n\nNote that the reason why RvLLM achieves lower TPR is the insufficient domain knowledge embedded in the inequality-solving tasks. With more knowledge encoded, the TPR will increase while maintaining the TNR as quite high still.\n\n\n\n### **Weakness 2.Efficiency Issue**\n\n\nSome cases take 15~30 seconds; the main reason behind this is the running time of the perception model, i.e., the oracle LLM used in RvLLM for interpretation abstraction. In the longest-running time cases, we use deepseek-chat as our interpretation abstraction perception model. By utilizing a more inference-efficient model, the running time can be largely reduced.\n\n\n### **Question 1. Extension of ESL**\n\nWe thank the reviewer for the thoughtful suggestion.\n\nExactly, extension of ESL to more complex constructs is certainly possible and is also part of our ongoing exploration. Currently, our initial trials have shown that it is feasible to expand ESL expressiveness to support richer scenarios. \n\nHowever, we also note potential concerns: as the complexity of ESL specifications increases, the accuracy of interpretation and abstraction (particularly for more intricate scenarios) may degrade. Such a trade-off highlights the importance of carefully balancing expressiveness and interpretability-accuracy in future extensions. Maybe a runtime specification refinement process would be an alternative, which allows runtime refinement of the granularity of the specification.\n\nFor future extensions to more enriched scenarios, a promising direction is to incorporate temporal operators into the specification language. Additionally, adapting the specification framework (e.g., TLA+) for smart contract verification offers a valuable and practical avenue. Ultimately, the trade-off between usability (i.e., user-friendliness and solving efficiency) and expressiveness remains a long-term research challenge.\n \n\n### **Question 2. Missing Ablation.**\n\nPlease see responses to **Weakness 1**."}, {"review_id": "plSo0tA0lM", "reviewer": "Reviewer_6smZ", "summary": "The paper proposes a method, RvLLM, for LLM output verification given a set of specifications. RvLLM uses a specification language (ESL) allowing domain experts to easily encode knowledge. At runtime, RvLLM interprets the specification given the LLM outputs to produce a set of propositions, then uses forward chaining to produce new knowledge and then query the LLM to detect inconsistencies. The experiments find that using RvLLM increases the TPR of detecting violations, while sometimes decreasing the FPR.", "questions": "- I'd suggest moving Related Work to the end before the conclusion for the flow of the paper\n- If possible it would be nice to incorporate a lightweight example into Figure 1 to give a more more intuitive understanding at the start of the paper\n- It would be interesting to see experiments where the LLM and RvLLM are different models. Particularly if a more lightweight model can effectively verify a larger model, it would decrease the overhead required to run this method.\n- Another interesting experiment would be to examine the performance scaling as the number of specifications given increases -- e.g. at L362 with 3 specifications RvLLM achieves 52.2% TPR; at what point would we observe diminishing returns from adding more specifications? This sounds important for implementing this method in practice.\n\nMinor nits:\n- L203: Typo \"bidding\" should be \"binding\"\n- Table 3: Columns are labeled DS-V1 instead of DS-V3\n- Missing reference / baseline to Maieutic Prompting by Jung et al.", "limitations": "Yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n- The method is well described and clearly formalized.\n- ESL is a nice specification method for domain experts, usable for people who are not familiar with programming and formal logic.\n- The application to transit rules violations is interesting and provides a good contrast between the mathematical domains and more natural rules.\n\nWeaknesses:\n- The paper is missing comparison to critical baselines that are mentioned in Related Work (SelfCheckGPT and CHECKEMBED). Also, simply using another LLM to verify the raw output, given just the input/output and the set of natural language rules (in the case of Singapore transit violations). Without these baseline to compare, it's difficult to judge how well the RvLLM method performs. \n- The method requires a significant up-front time investment for each domain (3 days for the Singapore transit example) -- for more complex domains and extending to general behavior specification, this seems prohibitively expensive.\n- L336-338: I think the conjecture about DeepSeek-V3 is a bit unfounded based on comparing just two domains.", "was_revised": true, "final_justification": "Thank you to the authors for the thorough response and the additional experiments! My questions and concerns have been addressed.", "rebuttal": "## **Reply to Reviewer 6smZ**\n\nWe thank the reviewer for the insightful comments and provide clarifications and additional experimental results below.\n\n### **Weakness 1. Missing Baselines**\n\nBefore presenting the comparison results with the baselines suggested by the reviewer, we would like to clarify the unique contribution of our work.\nThis is the first work enabling runtime verification of LLMs with domain knowledge, where the knowledge can be incrementally encoded offline using a user-predefined specification language, ESL. **ESL combines both natural language and formal language, striking a balance between usability and precision.**\n\nExisting verification approaches, such as self-checking methods, rely mainly on the assumption that “stable outputs == non-hallucination”, which targets general-purpose settings. In contrast, **RvLLM verifies** LLM outputs against **explicit domain constraints** and can pinpoint **why** an output violates the specified knowledge. \n\nDuring the rebuttal period, we added comparison experiments with SelfCheckGPT and LLM-as-judge. For SelfCheckGPT, we evaluated all its embedding options. Due to the space, we currently only show the most suggested one (by SelfCheckGPT’s authors), i.e., SelfCheckGPT (NLI), with a sampling size of N=4 due to the token usages. For the LLM-as-judge method, we use deepseek-chat as the judge and encode natural language based domain constraints into its judging prompts. Note that we use deepseek-chat as the judge, as it has shown strong performance in our three case studies.\n\nHere we present our experiment results:\n\n#### **For Case Study 1: Violation detection against Singapore Rapid Transit Systems Act**\n\n| verified model  | Method | TPR Inc. vs Raw LLM outputs | TNR Dec. vs Raw LLM outputs|\n| - | - | - | - |\n| Qwen-plus  | SelfCheckGPT   | +41.6%  | -100%  |\n|   | LLM as judge | +30.9% | -56.5% |\n|   | **RvLLM**  | +23.5%  | -0%    |\n| Qwen-turbo  | SelfCheckGPT   | +60.9% | -100%  |\n|  | LLM as judge | +38.1% | -47.8% |\n|  | **RvLLM**  | +35.9% | -0%  |\n| gpt-4.1-mini  | SelfCheckGPT  | +60.9%  | -96%  |\n|   | LLM as judge    | +22.4% | -16%   |\n|   | **RvLLM**   | +26.0% | -3.4%  |\n| gemini-2.0-flash  | SelfCheckGPT  | +63.0%    | -100%  |\n|    | LLM as judge  | +7.8%     | -12%   |\n|   | **RvLLM**   | +50.81%   | -17%   |\n| gemini-2.0-flash-lite | SelfCheckGPT   | +45.2% | -96% |\n|    | LLM as judge    | +18.1%    | -20%   |\n|   | **RvLLM**   | +24.9%   | -0.3%   |\n| deepseek-chat     | SelfCheckGPT   | +21.7%   | -87.0%  |\n|   | LLM as judge  | +9.6% | -65.2%  |\n|    | **RvLLM**     | +15.7%       | - 4.3%   |\n\nWe observe that  **RvLLM** achieves **more stable** performance across varied models, consistently maintaining a relatively low TNR drop while improving TPR high. In contrast, SelfCheckGPT often achieves the highest TPR increases simply because it tends to label nearly all outputs as “hallucinations” in our domain-specific settings, resulting in near-zero TNR. This behavior is expected, as SelfCheckGPT relies solely on output stability without incorporating domain knowledge. It does not encode or evaluate domain-specific rules, constraints, or context-sensitive reasoning, making it more suitable for open-domain generation tasks.\n\nAs for LLM-as-judge method, we find it can achieve competitive TPR compared to RvLLM. However, its performance is also unreliable, with TPR gains typically accompanied by significant TNR drops. In contrast, RvLLM remains a better balance between TPR and TNR. This is because RvLLM leverages the LLM primarily for text understanding/reading, while delegating rule-based domain-related reasoning to an external reasoning engine, leading to more reliable and interpretable outcomes.\nWe also include two additional comparison experiments corresponding to Case Studies 2 and 3.\n\n#### **For Case Study 2 and Case Study 3**:\n\nDue to the space limitation, please refer to the table results, which serve as a response to **Reviewer ywvD: Weakness 1**.\n\nNote that RvLLM’s relatively lower TPR in case study 3 stems from insufficient domain knowledge encoded. As more relevant knowledge is incorporated, TPR is expected to improve while still maintaining a high TNR. \n\nRegarding CheckEmbed. The reasons for not including it in the current comparison (during rebuttal) are outlined in our rebuttal W1 to Reviewer1: (1) high token cost, (2) limited time during the rebuttal period, (3) existing comparisons with SelfCheckGPT and llm-as-judge already reflect our effectiveness, and (4) CheckEmbed remains a preprint. That said, if the reviewer is still interested, we are also happy to extend our experiments with CheckEmbed in the coming weeks.\n\n### **Weakness 2. Up-front time for each domain**\n\nWe appreciate the reviewer’s concern regarding ESL authoring time. For the MRT domain, we used 31 official regulations, with the estimated 3 days reflecting total (non-continuous) working time, mainly spent interpreting legal texts rather than writing ESL rules. The annotator was a student familiar with ESL but not with MRT Law, representing a worst-case scenario. In familiar domains (e.g., math), writing rules (e.g., for inequalities) typically took under 1~10 minutes. \nImportantly, once written, ESL rules are reusable across models and tasks. Unlike red teaming or dataset-based validation, which require repeated efforts, **ESL offers a one-time setup that can be incrementally extended as needed.**\nOverall, we believe the upfront cost is reasonable and amortized, given ESL’s reusability, interpretability, and extensibility.\n\n### **Weakness 3. Conjecture about deepseek-v3 in lines 336-338**\n\nWe thank the reviewer for the feedback. We agree that the original conjecture may be too strong, given it is based on only two domains. In the revision, we will soften the presentation, present it as an empirical observation limited to the studied domains, and clarify that further investigation is needed to support any broader claims.\n\n### **Question 1. Moving related work to the end**\n\nThank you for the suggestion. We agree that moving the Related Work section before the conclusion improves the paper’s flow, and we will make this change in the revised version.\n\n### **Question 2. A lightweight example**\n\nThank you for the helpful suggestion. We agree that an early lightweight example would improve accessibility. In the revision, we will either integrate a simplified example into Figure 1 or move the existing running example (Figure 2) into the introduction to provide clearer intuition from the start.\n\n### **Question 3. Exp. when LLM and RvLLM are different models.**\n\nIn response to **Reviewer 9HFq**’s request (**Reviewer 9HFq: Weakness 3**), we conducted an additional experiment example to demonstrate RvLLM’s usability and breadth beyond the given three case studies. This new case involves alcohol consumption regulations in Singapore. We encoded 6 official rules and collected 200 real-world scenarios from the internet. In addition to standard evaluation (a similar setup to Case study 1), we also performed an ablation study treating the LLM and RvLLM as different models. The results are presented below.\n| verified LLM  | LLM as oracle used in RvLLM | LLM: TPR | LLM + RvLLM: TPR | TPR inc by RvLLM |\n| - | - | - | - | - |\n| qwen-max |  qwen-max | 67.5%    |   76.5%  |   +9% |\n|  |  qwen-turbo | 66.3%  |   71.4%  |  +5% | \n| gpt-4.1 | gpt-4.1 | 72%  |   82% |  +10% |\n| | gpt-4.1-nano  |   71.9% | 73.4% |  +1.5% |\n| gemini-2.0-flash | gemini-2.0-flash | 60.5% | 85%  |  +24.5% |\n| | gemini-2.0-flash-lite | 61.5%  | 71.5% |  +10% |\n\nThe results show a noticeable drop in TPR when using a more lightweight model as the oracle LLM in RvLLM. This suggests that RvLLM’s effectiveness depends on the oracle model’s capability, as the accurate interpretation abstraction process requires a nuanced understanding of natural language. We will include these experimental results in the revised version.\n\n### **Question 4. Long Tail Effect of Domain Knowledge in RvLLM**\n\nWe thank the reviewer for raising this important, interesting, and practical question. \nWhile accurate abstraction combined with more domain knowledge generally improves TPR, we acknowledge the potential for diminishing returns as the number of specifications grows, especially when addressing long-tail or rare reasoning errors. \n\nTo explore this, we conducted a detailed analysis on Case Study 3, examining performance as additional rules were added manually. Indeed, we identified three recurring error types that are challenging to capture under the current ESL design. Although the other typical error types were not fully experimentally analyzed, they also suggest diminishing returns from further rule additions. We will include this discussion and supporting analysis in the revised version.\n\n| verified LLM  | Incorrect Total Num | Factorization Error | Interval Error | Endpoints Error | Sign Handling Error | Simplification Error | Forgetting | Hallucination |\n| - | - | - | - | - | - | - | - | - |\n| qwen-max | 12 | 1 | 1 | 3 | 3 | 3 | 0 | 1 |\n| qwen-plus  | 10 | 2 | 0 | 2 | 1 | 1 | 3 | 1 |\n| qwen-turbo | 22 | 1 | 1 | 4 | 2 | 6 | 6 | 2 |\n| gpt-4.1 | 5  | 1 | 0 | 0 | 1 | 1 | 2 | 0 |\n| gpt-4.1-mini | 2  | 0 | 0 | 1 | 1 | 0 | 0 | 0 |\n| gpt-4.1-nano| 10 | 0 | 1 | 1 | 5 | 0 | 2 | 1 |\n| gemini-2.0-flash| 5  | 0 | 1 | 0 | 1 | 2 | 0 |1|\n| gemini-2.0-flash-lite|6|2|0|1|0|1|1|1|\n\nWe find that \"Endpoints Error,\" \"Sign Handling Error,\" \"Simplification Error,\" and \"Forgetting\" yield better returns under our benchmarks and verified LLM models, provided they can all be precisely encoded as domain constraints and embedded into RvLLM, even though the latter three remain difficult to represent accurately within the current ESL framework.\n\nAdditional error types identified:\n- Sign handling error: Algebraic computation mistakes\n- Simplification error: Incorrect simplification of inequality\n- Forgetting: Incorrectly combining results across multiple cases"}]

Author rebuttal:

Meta-review: The paper introduces a lightweight logic to be used for runtime detection of inconsistencies. The logic is a fragment of first-order logic, where the formulas are of the form DNF \implies CNF, and the predicates P(X,Y) are associated with natural language expressions. The LLM is queried to populate the grounded predicates P(a,b) to assumed to be true, and a variation of forward chaining is used to detect inconsistencies. Inconsistencies are used to reject decoding paths in the LLM.

The reviewers praised the equilibrium between a simple language suitable for modelling and an effective mechanism, demonstrated using Singapore traffic regulation.

Some of the weaknesses mentioned included that the logic might be too simple to represent complex domains, and the cost of expressing the rules in logic. The author's response focuses on the value of achieving higher robustness at the price of modelling the rules. 

The reviewers commented on the lack of comparison with verification using LLMs. The authors provided experimental results that convinced the reviewers.

Other reviewers pointed out how, as the number of rules increases, it might be harder to detect mistakes. I consider this slightly out of scope, but the authors perform an experiment adding additional rules manually and showing the different kinds of errors that might appear.

The reviewers didn’t discuss in depth the technical details of the logic and the inference mechanism, probably due to a lack of background. This is NeurIPS and is increasingly more challenging to find researchers familiar with the large body of work on using logic for AI tasks and model checking.

In my opinion, the algorithm is focused on detecting inconsistencies in tractable time, and dealing with the open domain assumption (absence of predicate P(a) does not mean we can assume -P(a)). The authors might want to look into intuitionistic logics, as they don’t include the axiom $P \lor \-P$.

The comment on Signal Temporal Logic (STL) is, honestly, irrelevant. STL is an extension of LTL, linear temporal logic. The ESL language only uses universal quantifiers. (STL is not mentioned in the manuscript, so there is nothing to fix there).

An improved version of this work should look into Datalog and other extensions of Horn clauses. Here is a recent relevant reference:
Martin Babka, Tomáš Balyo, Ondřej Čepek, Štefan Gurský, Petr Kučera, Václav Vlček,
"Complexity issues related to propagation completeness",
Artificial Intelligence, 2013, https://doi.org/10.1016/j.artint.2013.07.006.
 
Meanwhile, here is a technical detail: The transformation mentioned in L218, section 4.2, obtains horn clauses from the original ESL formulas. A detail is mentioned without full justification. For all rules with CNF of the right side, a rule is added to conclude each literal, by adding the condition that all the others are false. That is for a role $t \implies p \lor q \lor r$, rules of this form are generated: $t \land \-p \land \-q \implies r$

This transformation is equivalent to “unit propagation”! https://en.wikipedia.org/wiki/Unit_propagation
The most basic inference used in SAT solvers, and is part of the original paper on DPLL.

However, that mechanism is sound for detecting inconsistencies, but is not complete. For that, consider the SAT problem: check whether a CNF formula $\phi = \phi_1 \land \dots \land \phi_n$, where each $\phi$ is a disjunction, is satisfiable. That problem is the prototypical NP-complete problem. That formula can be converted into an ESL by just using DNF = true. We don’t even need predicate variables. In this case, ESL might not detect inconsistencies, but the formula might be unsatisfiable. (If you want a concrete example, look for trivial encodings of the https://en.wikipedia.org/wiki/Pigeonhole_principle)
However, from the purely algorithmic point of view, reducing the inference to what we can get from unit propagation makes it efficient and can detect non-trivial inconsistencies.

The informal discussion of the logic is acceptable for a paper in NeurIPS, at least nowadays. It would have been harder to accept in AAAI or in general AI journals like AIJ or JAIR.

I strongly recommend that the authors add a related work subsection connecting with relevant work, and not imply in any way that the algorithm is complete. Please do not say or imply in any way that “ESL is the first specification language that integrates both natural language and formal language”. Natural language interpretations have a long tradition in AI. It was popular in the 80s to mix expert systems with NLP.
Decision: Accept (poster)