Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle
作者: Dennis Gross, Helge Spieker
分类: cs.AI, cs.LG
发布日期: 2026-08-31
💡 一句话要点
提出基于模型检查的自动化测试方法以验证LLM生成的解释
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大型语言模型 后置解释 模型检查 自动化测试 决策政策 可信度评估 自然语言处理
📋 核心要点
- 现有方法缺乏有效的oracle来验证LLM生成的解释的正确性，且自然语言查询缺乏结构化，难以进行系统测试。
- 本文提出利用概率模型检查作为测试oracle，自动评估LLM生成的解释，并通过分类法结构化输入空间以生成测试用例。
- 实验结果显示，推理模型在85%的测试用例中表现良好，而1B模型的表现低于随机基线，表明LLM生成的解释在无模型环境下的可信度差异。
📝 摘要（中文）
大型语言模型（LLMs）被用作后置解释器，生成关于决策政策的自然语言解释。然而，LLMs常常生成看似合理但不正确的陈述，现有方法未能系统性地测试这些解释是否忠实于环境。本文提出利用概率模型检查作为测试oracle，自动计算参考结果以评估LLM的回答。同时，构建了后置查询类别的分类法，以结构化输入空间并优先生成具有特定诊断难度的测试用例。实验结果表明，在七个MDP环境中，三种开放权重的LLM表现不同，推理模型通过85%的测试用例，而1B模型的表现低于随机基线，验证了LLM生成解释的可信度。
🔬 方法详解
问题定义：本文旨在解决LLM生成的后置解释的正确性验证问题。现有方法缺乏有效的测试oracle，导致无法系统性地评估解释的可信度。
核心思路：通过引入概率模型检查作为测试oracle，提供精确的参考结果，从而自动评估LLM的输出。同时，构建后置查询的分类法，以便系统化生成测试用例。
技术框架：整体架构包括两个主要模块：首先是概率模型检查模块，负责生成参考结果；其次是基于分类法的测试用例生成模块，优先考虑具有特定诊断难度的问题。
关键创新：最重要的创新在于将概率模型检查引入LLM解释的自动化测试中，提供了一个系统化的验证框架，与传统方法相比，显著提升了测试的有效性和准确性。
关键设计：在测试用例生成中，采用了基于问题特定的诊断难度评分来优先选择测试用例，确保测试覆盖了更具挑战性的场景。
🖼️ 关键图片
📊 实验亮点
实验结果表明，推理模型在85%的测试用例中表现良好，而中型模型的通过率为70%。相比之下，1B模型的表现低于随机基线，验证了不同LLM在生成解释时的可信度差异，且优先选择的测试用例显著更具挑战性。
🎯 应用场景
该研究的潜在应用领域包括自动化决策系统、智能助手和任何依赖于LLM生成解释的系统。通过提供一种系统化的验证机制，可以提高这些系统的透明度和可信度，进而增强用户信任和接受度。
📄 摘要（原文）
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.