Source-linked AI summary
Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle
Dennis Gross, Helge Spieker
TL;DR
LLM-generated post hoc explanations lack systematic faithfulness testing because correctness oracles and structured query inputs are missing. The paper combines probabilistic model checking, a query taxonomy, and diagnostic prioritization, then evaluates three open-weight models across seven MDP environments. Qwen3.5 passes 0.85 of test cases, Gemma 4 31B passes 0.70, and prioritized cases are significantly harder than random selection.
Problem
LLM explainers can produce plausible but incorrect statements, while explanation testing lacks both a correctness oracle and structured query inputs.
Method
The approach uses probabilistic model checking for exact oracle results, a taxonomy of post hoc query categories, and diagnostic scores to prioritize test cases.
Results
Qwen3.5 passes 0.85 of test cases, Gemma 4 31B passes 0.70, Gemma 3 1B scores 0.43 below the Random baseline at 0.51, and prioritization is harder than random selection at p = 0.035.
Takeaways & Limitations
The approach quantifies explanation trustworthiness and localizes which query categories and models can be trusted across the tested environments.
Takeaways & Limitations
Conclusions rely on seven exactly model-checkable environments and three open-weight LLMs, so they may not transfer to larger tasks or proprietary models.
Abstract
from arXiv · showhide
Large language models (LLMs) are used as post hoc explainers of sequential decision-making policies, producing natural-language explanations of why an action was chosen. However, LLMs often generate plausible but incorrect statements, and no existing approach systematically tests whether such explanations are faithful to the underlying environment. Two classic software testing challenges stand in the way: there is no oracle for the correctness of an explanation, and the test inputs, natural language queries about a policy's behavior, lack the structure needed for systematic test case generation. We address both. Probabilistic model checking provides the test oracle, computing exact reference results against which LLM answers are graded automatically. A taxonomy of post hoc query categories structures the input space around the environment-level facts from which policy explanations are composed; test cases generated from it are prioritized by question-specific diagnostic difficulty scores. Across seven MDP environments, the testing separates three open-weight LLMs: a reasoning model passes 85% of test cases, a mid-size model 70%, and a 1B model falls below the random baseline, while prioritization surfaces significantly harder cases than random selection. Our results indicate how trustworthy LLM-generated explanations are in model-free settings, where the same LLMs are used but no oracle exists to verify them.
1 Introduction
LLMs provide post hoc natural-language explanations for otherwise opaque sequential policies, but testing their faithfulness lacks both a correctness oracle and structured query inputs. The paper addresses these challenges with model checking, query taxonomy, and diagnostic prioritization.
- LLMs generate natural-language explanations after a policy chooses an action, because neural-network policies are not human-interpretable.
- Plausible but incorrect LLM statements make explainer testing necessary before explanations can be trusted.
- Testing lacks an oracle for explanation correctness and a structured input space for generating useful natural-language queries.
- Probabilistic model checking supplies exact environment-policy results, while a taxonomy structures queries around optimality and safety facts.
- Question-specific diagnostic scores prioritize states that are more informative for particular query categories.
2 Related Work
Prior work mainly produces explanations or evaluates LLMs with approximate references, whereas this paper tests explanation faithfulness against exact model-checking ground truth.
- The paper connects explainability, post hoc LLM explainers, LLM testing, and model checking for AI systems.
- Explainable reinforcement-learning work produces post hoc policy explanations, while this paper tests whether those explanations are faithful to the underlying environment.
- LLM explainer studies commonly judge explanations using approximate references such as human studies or LLM-as-a-judge evaluations.
- General LLM benchmarks with verifiable ground truth evaluate the LLM’s task performance, not its explanations of another system’s decisions.
- Prior model-checking work verifies policies or uses LLMs for policy-related tasks, whereas this paper uses exact results as an oracle for explanation faithfulness.
3 Background
The paper models sequential decision-making with MDPs, uses probabilistic model checking to compute exact state and action properties, and treats LLM responses as structured test outputs.
- 3.1 Probabilistic Systems: Sequential decision-making is modeled as a finite-state MDP in which actions stochastically influence successor states toward a fixed objective.
- 3.1 Probabilistic Systems: An agent receives states and rewards from the environment, then uses its policy to select actions that are sent back to the environment.
- 3.2 Probabilistic Model Checking: A PCTL model checker computes optimal property probabilities V(s), action values Q(s,a), and danger D(s) for the modeled system.
- 3.3 Large Language Models: An LLM explainer receives a prompt describing the environment, state, and query, then returns a response parsed into a structured verdict or action ranking.
- 3.4 Software Testing: The testing setup compares explainer outputs with model-checking results, using those exact results as the oracle and diagnostic rankings for prioritization.
4 A Taxonomy of Post Hoc Test Queries
The query taxonomy organizes post hoc tests by what they inspect, where they apply, and whether they judge or compare objects. These atomic environment-level tests are necessary conditions for faithful explanations.
- Query dimensions: Queries vary by object, scope, and mode: they inspect property results or action rankings, one state or a subset, and individual or relational judgments.
- Oracle-grounded categories: The oracle derives optimal and worst action sets, dead ends, and bottlenecks from V(s), Q(s,a), and related model-checking results.
- Query categories: State-level queries ask whether a property is satisfied, whether a state is a bottleneck, or whether a subset contains dead ends.
- Query categories: Action-level queries ask for the best action, worst action, or complete ranking using oracle-derived action values.
- Scope boundary: Passing best-action tests does not imply that the LLM, used as a full-trajectory policy, reaches target states.
- Query categories: Relational queries compare states by promise, safety, or bottleneck status rather than judging one state independently.
5 Testing Approach
The approach combines probabilistic model checking as an exact oracle with a taxonomy-driven test generator that prioritizes diagnostically difficult queries before automatically grading LLM answers.
- Pipeline: The pipeline accepts an MDP, PCTL properties, LLMs, query categories, a test budget, and a repetition sample size, then produces per-category verdicts for each LLM.It comprises four stages, including oracle construction, test generation and prioritization, prompt execution, and verdict comparison.
- Oracle construction: Model checking derives state property results V(s), action values Q(s,a), danger values when needed, optimal actions, dead ends, and bottleneck states.Bottlenecks are identified by re-checking reachability after making a candidate state absorbing.
- Generation and prioritization: Test cases target single states, state pairs, or state subsets, and the system retains the highest-difficulty candidates up to the test budget.Binary categories first balance positive and negative cases, then rank candidates within each class.
- Difficulty scoring: Diagnostic difficulty captures ambiguity, selectivity, or salience, emphasizing nearly tied values, few correct choices among distractors, or decoys mimicking true structure.The supplied formulas instantiate these notions for best and worst actions, rankings, state comparisons, and subset queries.
- Difficulty scoring: The difficulty formulas assume values in [0,1], while expected-reward properties normalize gaps by their value range so δ remains in [0,1].The difficulty score ranks candidates; the resulting verdict remains exact.
- Execution and verdicts: Selected cases are rendered into environment-specific prompts, sent to each LLM, repeated as specified, parsed into structured answers, and compared against category-specific oracle criteria.Comparisons check probabilities, actions, rankings up to ties, property-based preferences, bottleneck membership, and subset contents.
6 Evaluation
The evaluation tests prioritization, model discrimination, and category difficulty across seven MDPs and three open-weight LLMs. Prioritization finds harder cases overall, and model performance separates strongly by model capability.
- Research questions: The evaluation addresses whether diagnostic ranking finds non-trivial cases, whether stronger LLMs pass more tests, and whether query categories differ in difficulty.These are evaluated as RQ1, RQ2, and RQ3.
- Experimental setup: Seven MDP environments provide reachability properties whose model-checked results define the oracle.The environments include varied sequential decision-making tasks such as Frozen Lake, Wolf–Goat–Cabbage, Water Jug, and Transporter.
- Prioritization: Over 220 comparable cells, prioritization finds harder cases in 75 cells (34.1%), easier cases in 61 (27.7%), and ties in 84 (38.2%).A one-sided Wilcoxon signed-rank test favors prioritized < random at p = 0.035.
- LLM performance: The reasoning model Qwen3.5 scores 0.85, Gemma 4 31B scores 0.70, and the Random baseline scores 0.51 when averaged over environments.Under diagnostic prioritization, Gemma 3 1B scores 0.43, below random.
- LLM performance: Under diagnostic prioritization, stronger models pass more test cases than weaker models and the random baseline.The small Gemma 3 1B is below random on prioritized cases but rises to 0.55 under random selection versus random at 0.54.
- Category difficulty: The hardest categories are dead ends in subset (0.59), worst action (0.60), and bottleneck in subset (0.63), while which-is-bottleneck is easiest at 0.72.Scores are pooled over all models and both selection strategies.
7 Threats to Validity
The study’s validity is bounded by its decoding protocol, limited environments and models, handwritten templates, construct definition, and modest prioritization effect.
- Internal validity: Greedy decoding with sample size 1 captures modal rather than average LLM behavior, while structured-output parsing remains part of the verdict process.JSON-constrained decoding is used to mitigate parsing issues.
- External validity: Conclusions rely on seven exactly model-checkable environments and three open-weight LLMs, limiting transfer to larger tasks or proprietary models.Handwritten, environment-specific templates can shift absolute scores when the wording changes.
- Construct validity: The construct measures faithfulness to optimal behavior, so passing best-action cases does not establish policy-level goal achievement or causal faithfulness to the LLM’s computation.The difficulty score only ranks candidates; verdicts remain exact.
- Conclusion: The prioritization effect is statistically significant over 220 cells at p=0.035 but modest in magnitude.This qualifies the strength of the aggregate prioritization result.
8 Conclusion
The approach uses exact model checking as an oracle, structures explainer queries with a taxonomy, and prioritizes diagnostic test cases. Across seven environments and three LLMs, it discriminates between models and measures a trust gap; future work may use failures for fine-tuning.
- The approach combines probabilistic model checking as an exact oracle, a query-category taxonomy, and diagnostic scores for prioritizing tests.These components support automated grading, structured test generation, and targeted evaluation.
- Across seven environments and three LLMs, testing discriminates between models and localizes the categories where each model can be trusted.The evaluation also prioritizes significantly harder cases than random selection.
- Failed test cases are identified as a direction for future work on fine-tuning explainers.
- The work was funded by the European Union under grant agreement 101091783 for the MARS Project.
- The authors declare no competing financial interests.