# Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle

arXiv: https://arxiv.org/abs/2608.30581 · HTML: https://mlsanity.com/paper/2608.30581/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 27 of its 43 references that are in the map.
- First posted on arXiv 31 Aug 2026.

## Builds on (most cited first, 27 of 27)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [TruthfulQA: Measuring How Models Mimic Human Falsehoods](https://mlsanity.com/paper/2109.07958/) (2021)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [Beyond Accuracy: Behavioral Testing of NLP models with CheckList](https://mlsanity.com/paper/2005.04118/) (2020)
- [PlanBench: An Extensible Benchmark for Evaluating Large Language Models on Planning and Reasoning about Change](https://mlsanity.com/paper/2206.10498/) (2022)
- [Machine Learning Testing: Survey, Landscapes and Horizons](https://mlsanity.com/paper/1906.10742/) (2019)
- [Survey on Large Language Model-Enhanced Reinforcement Learning: Concept, Taxonomy, and Methods](https://mlsanity.com/paper/2404.00282/) (2024)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [LLMs for Explainable AI: A Comprehensive Survey](https://mlsanity.com/paper/2504.00125/) (2025)
- [Towards Consistent Natural-Language Explanations via Explanation-Consistency Finetuning](https://mlsanity.com/paper/2401.13986/) (2024)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [On the Fundamental Limits of LLMs at Scale](https://mlsanity.com/paper/2511.12869/) (2025)
- [dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts](https://mlsanity.com/paper/2101.07202/) (2021)
- [Distributional Reward Decomposition for Reinforcement Learning](https://mlsanity.com/paper/1911.02166/) (2019)
- [SAFE-RL: Saliency-Aware Counterfactual Explainer for Deep Reinforcement Learning Policies](https://mlsanity.com/paper/2404.18326/) (2024)
- [A Closer Look at Reward Decomposition for High-Level Robotic Explanations](https://mlsanity.com/paper/2304.12958/) (2023)
- [Verified Probabilistic Policies for Deep Reinforcement Learning](https://mlsanity.com/paper/2201.03698/) (2022)
- [Enhancing RL Safety with Counterfactual LLM Reasoning](https://mlsanity.com/paper/2409.10188/) (2024)
- [Probabilistic Model Checking of Stochastic Reinforcement Learning Policies](https://mlsanity.com/paper/2403.18725/) (2024)
- [Model-Agnostic Policy Explanations with Large Language Models](https://mlsanity.com/paper/2504.05625/) (2025)
- [Explaining Agent Behavior with Large Language Models](https://mlsanity.com/paper/2309.10346/) (2023)
- [Turn-based Multi-Agent Reinforcement Learning Model Checking](https://mlsanity.com/paper/2501.03187/) (2025)
- [A Survey of Explainable Reinforcement Learning: Targets, Methods and Needs](https://mlsanity.com/paper/2507.12599/) (2025)
- [TalkToAgent: A Human-centric Explanation of Reinforcement Learning Agents with Large Language Models](https://mlsanity.com/paper/2509.04809/) (2025)
- [Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC](https://mlsanity.com/paper/2602.14505/) (2026)
- [Verifying Memoryless Sequential Decision-making of Large Language Models](https://mlsanity.com/paper/2510.06756/) (2025)
- [Interpret Policies in Deep Reinforcement Learning using SILVER with RL-Guided Labeling: A Model-level Approach to High-dimensional and Multi-action Environments](https://mlsanity.com/paper/2510.19244/) (2025)

## Abstract (arXiv)

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.