使用模型检查作为预言机的基于大语言模型的事后解释器自动化测试

使用模型检查作为预言机的基于大语言模型的事后解释器自动化测试（中文全译）

翻译说明：本文是 arXiv 论文 Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle（arXiv:2608.30581）的中文全译，由智测团队翻译。原作者：Dennis Gross、Helge Spieker（Simula Research Laboratory 等）。原文以 CC BY 4.0 许可发布。译文保留原文全部章节、数据与结论；参考文献列表从略。

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

Dennis Gross

所属机构：Institut für Kommunikations- und Prüfungsforschung gGmbH

所属机构：Simula Research Laboratory, Oslo, Norway

通讯作者：

电子邮件 dennis@artigo.ai

Helge Spieker

所属机构：Simula Research Laboratory, Oslo, Norway

通讯作者：

电子邮件 dennis@artigo.ai

摘要

大语言模型（LLMs）被用作序列决策策略的事后解释器，生成关于为何选择某个动作的自然语言解释。然而，LLMs 经常生成看似合理但不正确的陈述，而且目前没有方法系统性地测试这些解释是否忠实于底层环境。两个经典的软件测试挑战阻碍了这一进程：一是缺乏解释正确性的预言机，二是测试输入（关于策略行为的自然语言查询）缺乏系统性测试用例生成所需的结构。我们同时解决了这两个问题。概率模型检查提供了测试预言机，计算精确的参考结果，据此自动对 LLM 的答案进行评分。一个事后查询类别的分类法围绕构成策略解释的环境级事实来构建输入空间；由此生成的测试用例根据特定问题的诊断难度分数进行优先级排序。在七个 MDP 环境中，测试区分了三个开放权重 LLMs：一个推理模型通过了 85% 的测试用例，一个中等规模模型通过了 70%，而一个 1B 模型低于随机基线，同时优先级排序显著地揭示出比随机选择更难的案例。我们的结果表明了在无模型设置中 LLM 生成的解释的可信度，在这些设置中使用了相同的 LLMs，但不存在预言机来验证它们。

关键词：软件测试 大语言模型 概率模型检查 可解释强化学习 测试预言机

1 引言

序列决策任务是游戏 [17]、制造 [11] 和医疗 [18] 等领域应用的核心：智能体反复观察其环境的当前状态，选择一个动作，从而随机地影响后继状态以达到固定目标。此类任务形式化建模为马尔可夫决策过程（MDPs）[29]。我们关注具有有限状态和动作的 MDPs，以及无记忆策略，后者仅基于当前状态而非过去状态和动作的历史来做每个决策。单个决策的后果会在后续步骤中展开。策略通常通过自动方式获得，例如通过深度强化学习（RL）[27]，因此人类用户往往无法访问个体选择背后的理由：学到的策略是一个神经网络，其内部计算对人类不可解释。为解决这一问题，大语言模型（LLMs）最近被用作事后解释器，在事后分析决策，而不是使策略本身设计上可解释 [6]：在策略做出决策后，提示 LLM 生成自然语言解释，说明为何在给定状态下选择了该动作。

然而，众所周知，LLMs 会产生听起来合理但不正确的陈述 [28]，这引发了一个软件测试问题：在信任这些解释之前，必须对基于 LLM 的解释器本身进行测试。测试它面临两个挑战。第一，没有测试预言机 [4]：判断解释是否正确需要了解环境和策略的真实属性。第二，输入空间是非结构化的：目前尚不清楚存在哪些类型的解释查询，以及哪些具体查询值得提出。因此，虽然先前的工作已经评估了 LLM 生成的解释 [23, 35]，甚至用它们来改进策略性能 [14]，但没有方法系统性地测试 LLM 是否真正理解底层环境并生成忠实于环境的解释。

在本文中，我们提出了一种自动化方法来测试序列决策策略的基于 LLM 的事后解释器。我们通过概率模型检查 [3] 解决预言机问题：给定环境的形式化模型和用时态逻辑（如 PCTL）[19] 指定的属性，模型检查器穷尽分析状态空间并计算例如达到目标或违反安全条件的精确概率。这些结果是精确的并带有形式保证，因此可作为可靠的预言机，据此自动对 LLM 的答案进行评分。为了构建测试输入空间，我们引入了一个事后查询类别的分类法，指导生成有针对性的测试查询，例如在某个状态下哪些动作是最优的或某个状态是否是安全关键的，并按类别显示不同 LLMs 在哪里成功或失败。这些查询针对环境级事实，如最优性和安全性，任何策略决策的事后解释都由这些事实组成。由于并非每个状态对每个查询都同样具有信息量，我们通过特定问题的诊断分数对测试输入进行优先级排序，例如非最优动作的比例，并选择排名最高的状态进行测试。我们的方法需要环境的形式化模型，但这一限制仅适用于测试，不适用于其影响：形式化模型为 LLM 的推理能力提供了测量工具。通过这种受控设置获得的测试结果由此表明在无模型设置中 LLM 生成的解释的可信度，在这些设置中应用相同的 LLMs，但不存在预言机来验证它们。

2 相关工作

我们的工作涉及四个研究领域：序列决策的可解释性、LLMs 作为事后解释器、LLMs 的测试与评估，以及 AI 系统的模型检查。

序列决策的可解释性。

大量关于可解释强化学习（XRL）[34] 的工作生成学习策略的事后解释，例如通过策略摘要 [30]、显著图 [33] 和奖励分解 [25]，以及最近通过使用 LLMs 作为事后解释器 [6]。所有这些方法都侧重于生成解释；相比之下，我们测试这样的解释器是否生成忠实于底层环境的解释。

LLMs 作为事后解释器。

越来越多的工作使用 LLMs 作为学习策略的事后解释器，提示它们生成自然语言描述，说明智能体为何选择给定动作 [42, 26, 7, 22, 43]。在这类工作中，解释仅针对近似参考进行评估，例如人类研究 [45] 和 LLM-as-a-judge [5]。相比之下，我们根据来自概率模型检查的精确地面真值对解释进行评分，并按照事后查询类别的分类法组织。

LLMs 的测试与评估。

除了对解释的研究外，广泛的文献直接测试 LLMs，范围从行为测试套件 [31] 和幻觉基准 [24, 21] 到具有可验证地面真值的基准，例如 PlanBench [39]，它通过自动验证器对 LLM 计划进行评分；ML 系统缺乏可靠的测试预言机是一个众所周知的挑战 [44, 4]。然而，当存在精确地面真值时，它测试的是 LLM 自身的任务表现，而不是其对另一个系统决策的解释的忠实性。我们使用概率模型检查作为测试预言机来实现这一目的。

AI 系统的模型检查。

概率模型检查已用于通过对策略诱导的马尔可夫链进行模型检查来根据 PCTL 属性验证学习策略 [2, 10, 15]，也与可解释性方法 [16, 1] 和 LLMs 结合使用，要么生成反事实以进行策略修复 [13]，要么作为待验证的策略 [12]。在所有这些工作中，待验证的对象是策略。相比之下，我们使用模型检查作为测试预言机：其精确结果作为地面真值，据此我们对 LLM 生成解释的忠实性进行评分。

3 背景

我们介绍贯穿全文的概率系统、概率模型检查、LLMs 和软件测试概念，以及后续部分使用的符号。

3.1 概率系统

我们将序列决策建模（见图 1）为马尔可夫决策过程（MDP），一个元组 $\mathcal{M}=(S,s_{0},\mathit{Act},P,\mathit{AP},L)$，其中 $S$ 是有限状态集，$s_{0}\in S$ 是初始状态，$\mathit{Act}$ 是有限动作集，$P:S\times\mathit{Act}\times S\to[0,1]$ 是转移函数，对每个启用动作 $a$ 满足 $\sum_{s^{\prime}}P(s,a,s^{\prime})=1$，$\mathit{AP}$ 是原子命题的有限集，$L:S\to 2^{\mathit{AP}}$ 是标签函数，将每个状态映射到在该状态中成立的原子命题集。我们写 $\mathit{Act}(s)\subseteq\mathit{Act}$ 表示在状态 $s$ 中启用的动作。在每个状态下，智能体选择一个动作 $a$，环境从分布 $P(s,a,\cdot)$ 中抽取下一个状态。例如，在一个打滑的网格世界中，动作 right 可能以概率 0.8 到达预期方块，否则漂移到垂直邻居。标签标识感兴趣的状态：目标状态是那些标记为 goal 的状态，即 $\{s:\textit{goal}\in L(s)\}$，不安全集 $U\subseteq S$ 通过 unsafe 标签类似定义。（确定性、无记忆）策略 $\pi:S\to\mathit{Act}$ 在每个状态中选择一个动作；此类策略足以实现我们考虑的最优可达概率。固定 $\pi$ 解决所有选择并将 MDP 折叠为诱导的离散时间马尔可夫链（DTMC），其行为完全由 $P$ 和 $\pi$ 决定。

智能体 → 动作 → 环境 → 新状态、奖励 → 智能体

图 1：智能体与环境交互的序列决策系统。智能体根据之前的动作从环境接收状态和奖励。然后智能体使用这些信息通过策略选择下一个动作，并将其发送给环境。

3.2 概率模型检查

给定用概率计算树逻辑（PCTL）[19] 编写的规范，模型检查器计算规范成立的概率。我们使用形式为 $\mathsf{P}_{\max}{=}?\ [\,\mathsf{F}\;\textit{goal}\,]$ 的可达性属性，读作"最终（$\mathsf{F}$）达到目标状态的最大概率是多少？"；对偶地，$\mathsf{P}_{\min}{=}?\ [\,\mathsf{F}\;\textit{unsafe}\,]$ 询问在所有策略下的最小此类概率。对于每个状态 $s$，检查器计算属性结果 $V(s)$，即从 $s$ 满足属性的最优概率，对于每个动作 $a\in\mathit{Act}(s)$ 计算动作值 $Q(s,a)$，即在 $s$ 中采取 $a$ 并在之后最优行动所获得的属性结果；我们将状态中的动作值递减排序记为 $Q_{(1)}\geq Q_{(2)}\geq\dots$。对于我们考虑的可达性属性 $\mathsf{P}_{\max}[\mathsf{F}\,\textit{goal}]$，$V$ 和 $Q$ 恰好与强化学习的值函数和动作值函数一致，在进入目标状态（使其吸收）时授予奖励 1，否则为 0，无折扣（$\gamma=1$），因此熟悉的 $V$/$Q$ 符号可以沿用。我们进一步使用危险度 $D(s)=\mathsf{P}_{\min}[\,\mathsf{F}\,U\,]$，即从 $s$ 到不安全集的最小可达概率，通过第二次模型检查运行获得。Storm [20] 等工具在可达状态上高效计算这些量。

3.3 大语言模型

大语言模型（LLM）是基于 transformer 架构 [40] 的神经网络。它在 token 上运行，即 tokenizer 将自然语言文本分割成的有限词汇表 $\mathcal{V}$ 的元素。形式上，LLM 定义了一个函数 $f_{\theta}\colon\mathcal{V}^{*}\to\Delta(\mathcal{V})$，将 token 序列映射到下一个 token 的概率分布。文本是自回归生成的：给定输入序列，模型从 $f_{\theta}$ 采样一个下一个 token，将其附加到序列中，重复直到产生指定的停止 token；得到的 token 序列解码回文本。

我们按如下方式使用 LLM 作为事后解释器。提示（prompt）是一段自然语言输入文本，描述环境、状态 $s$ 和关于 $s$ 中决策任务的查询。提示被 tokenized 并传递给模型，模型生成自然语言响应。然后解析器将此响应映射到结构化答案，如是/否判定或动作排序。

3.4 软件测试

测试在选定输入（称为测试用例）上执行被测系统（SUT），并将观察到的行为与预期行为进行比较。提供预期行为的机制是测试预言机 [4]；其缺失或不可靠，称为预言机问题 [41]，是在测试其正确输出不易知道的系统（如机器学习组件 [44]）时的中心挑战。由于执行所有可能的测试用例通常不可行，测试用例优先级排序使最有信息量的用例首先执行 [32]。在我们的设置中，SUT 是基于 LLM 的解释器；测试用例将（提取的）MDP 及其自然语言描述与状态级查询配对；模型检查器的精确结果作为测试预言机；我们的诊断状态排序实例化了测试用例优先级排序。

4 事后测试查询的分类法

模型检查器为每个状态提供了一个测试预言机：属性结果 $V(s)$ 和按其值 $Q(s,a)$ 排序的可用动作排名。任何具体策略的事后解释都分解为关于环境的状态级主张，例如，某个动作是次优的、某个状态是不安全的，或某个决策导致死胡同。我们的查询针对环境中的最优行为测试这些原子主张：在这些查询上失败的模型无法为其上运行的任何策略生成忠实的解释，因此通过这些查询是解释忠实性的必要条件。相对于特定固定策略 $\pi$ 的查询（模型检查器以相同方式分析其诱导的 DTMC）也适合同一方案。测试用例是向待测 LLM 提出的查询；我们通过自动将其答案与预言机比较来获得判定，并优先执行最具诊断性的测试用例（第 5 节）。查询沿三个维度变化：对象（属性结果或动作排名）、范围（一个状态或子集）和模式（判断一个对象或比较两个）。下面的示例说明了每个维度，但并不详尽；任何可以通过预言机回答的查询都可以以相同方式添加。

4.1 派生概念和评分

除了背景部分介绍的 $V$、$Q$ 和 $D$ 之外，我们的查询使用以下派生概念。最优动作集 $A^{\star}(s)=\{a\in\mathit{Act}(s):Q(s,a)=\max_{a^{\prime}}Q(s,a^{\prime})\}$ 包含 $s$ 中动作值的最大化者，最劣动作集 $A^{\circ}(s)$ 类似定义为最小化者集。$V(s)=0$ 的状态是死胡同：属性不再能从该状态满足。状态 $s$ 是瓶颈当且仅当当使 $s$ 变为吸收状态时，从 $s_0$ 到目标的可达概率降至 0；这通过重新检查修改后的模型来精确判定。最后，$C_{B}(s)$ 表示 MDP 基础有向图中 $s$ 的介数中心性 [9]，如果存在某个 $a$ 使得 $P(s,a,s^{\prime})>0$，则有边 $s\to s^{\prime}$。$C_{B}$ 仅作为排序启发式方法，从不用作地面真值。评分是精确的：回答 Satisfy 查询的概率正确当且仅当它等于模型检查器的结果 $V(s)$；命名的最佳（最差）动作正确当且仅当它位于 $A^{\star}(s)$（$A^{\circ}(s)$）中；在排序查询中，等值动作可以任意排序并被评分为任一顺序正确。

4.2 对象

对象是查询读取的量，给出两个家族。

状态查询

仅关于状态的判断，独立于任何动作。

• 满足属性？ 从该状态实现属性的可能性有多大，以概率估计回答并根据 $V(s)$ 评分。

• 瓶颈？ 每次成功运行是否必须经过此状态，即没有它目标就不可达。

偏好查询

关于给定状态下动作的判断。

• 最佳动作？ 哪个动作是最优的，根据 $A^{\star}(s)$ 评分。

• 最差动作？ 哪个动作最具破坏性，根据 $A^{\circ}(s)$ 评分。

• 完整排序？ 所有动作如何排序，根据排序的动作值评分。

注意，在最佳动作测试用例上的通过判定并不意味着 LLM 作为在整个轨迹上部署的策略能够达到目标状态。

4.3 范围

局部查询读取一个状态下的对象；全局查询读取子集 $S^{\prime}\subseteq S$ 上的对象。

• 子集中的瓶颈？ 子集 $S^{\prime}$ 中是否有任何状态是瓶颈状态。

• 子集中的死胡同？ $S^{\prime}$ 是否包含死胡同状态，即 $V(s)=0$ 的状态。

4.4 模式

个体查询判断一个对象；关系查询比较两个。

• 哪个状态更有希望？ 两个状态中哪个具有更高的属性结果。

• 哪个状态更安全？ 两个状态中哪个具有更低的危险度 $D$。

• 哪个状态是瓶颈？ 给定两个状态，每次成功运行必须经过哪一个。

5 测试方法

我们的方法接受以下输入：MDP、感兴趣的 PCTL 属性（主属性，如果使用危险查询，则包括定义 $D$ 的安全属性）、待测 LLMs、第 4 节中具有提示模板和诊断评分方法的查询类别、测试预算（执行多少测试用例）和样本大小（为应对 LLM 非确定性而重复每个测试用例的次数）。它为每个 LLM 输出每个类别的判定。管道分为四个阶段。

预言机构建。

对 MDP 和 PCTL 属性进行模型检查，为每个可达状态生成属性结果 $V(s)$、动作值 $Q(s,a)$ 以及（如果需要）危险度 $D(s)$。从中我们推导出测试用例需要的预期答案：每个状态的动作排名、最优策略、死胡同（$V(s)=0$）和瓶颈状态，后者通过将候选状态设为吸收状态后重新检查可达性（第 4.1 节）。例如，对于最佳动作查询，这会生成每个状态的最优动作集 $A^{\star}(s)$，即 LLM 的答案稍后将与之比较的预期输出。

测试用例生成和优先级排序。

每个测试用例涉及单个状态（状态和偏好查询）、一对状态（模式查询）或状态子集（范围查询）。系统生成适当类型的候选测试用例，根据诊断难度 $\delta$ 对每个进行评分，并保留最高 $\delta$（最难）的用例直至测试预算；三个二元类别（瓶颈、子集瓶颈、子集死胡同）首先平衡正例和负例，然后在每类中按 $\delta$ 排序。诊断难度针对最可能被错误回答的案例，通过三种概念之一：歧义性（候选值几乎平局，因此答案 barely determined）、选择性（在众多干扰项中选择单个正确答案）和显著性（模仿真实结构的诱饵）。使用第 4 节和第 4.1 节的符号，难度为：

• 满足（歧义性）：$\delta=1-2\,|V(s)-\tfrac{1}{2}|$，属性结果最接近 $\tfrac{1}{2}$。

• 最佳动作（选择性）：$\delta=1-|A^{\star}(s)|/|\mathit{Act}(s)|$；很少动作是最优的，因此必须从众多干扰项中选出最佳。

• 最差动作（选择性）：$\delta=1-|A^{\circ}(s)|/|\mathit{Act}(s)|$，与最佳动作对称：很少动作是最差的。

• 完整排序（歧义性）：$\delta=1-\min_{i}\,(Q_{(i)}-Q_{(i+1)})$，真实排序中最小的相邻差距；等值动作评分为任一顺序正确（第 4.1 节）。

• 更有希望（歧义性）：$\delta=1-|V(s_{1})-V(s_{2})|$，两个状态的属性结果接近。

• 更安全状态（歧义性）：$\delta=1-|D(s_{1})-D(s_{2})|$，两个状态的危险度接近。

• 瓶颈（显著性）：$\delta=C_{B}(s)$；状态位于许多路径上，因此最像瓶颈。判定本身是精确的（第 4.1 节），$C_{B}$ 仅对候选进行排序。

• 哪个是瓶颈（显著性）：$\delta=C_{B}(s_{\mathit{decoy}})$，中心非瓶颈诱饵与真实瓶颈配对。

• 子集瓶颈（显著性）：$\delta=\max_{s\in S^{\prime}}C_{B}(s)$，子集中最像瓶颈的成员。

• 子集散死胡同（歧义性，负例）：$\delta=1-\min_{s\in S^{\prime}}V(s)$，最低值接近零的子集；正子集（包含死胡同，因此 $\min_{s\in S^{\prime}}V(s)=0$）在 $\delta=1$ 处平局并均匀采样。

上述 $1-\text{gap}$ 形式假设值在 $[0,1]$ 范围内，如同我们整个实验中使用的可达概率 $V,D$；更一般地，$\delta$ 随着相关差距缩小而增加，对于期望奖励属性，差距通过值范围归一化，使得 $\delta\in[0,1]$。

测试执行。

每个选定的测试用例通过模板渲染为提示，填入其状态、对或子集，并发送给每个待测 LLM，重复样本大小次数。模板是唯一依赖于环境的部件：它固定如何用词语描述状态以及询问 LLM 什么。对于完整排序查询，可能如下所示：

你是一个 5×5 网格世界中的智能体。你的目标是到达 (4,4) 处的出口，同时避开 (2,3) 处的陷阱。
当前位置：{state}。
可用动作：{actions}。
将所有可用动作从最佳到最差排序。仅以 JSON 对象形式回复，格式为 {"ranking": ["<best action>", ..., "<worst action>"]}。

在执行时，占位符从选定状态填充，例如 {state} → (1,3) 和 {actions} → up, down, left, right，LLM 返回结构化回复，例如：{"ranking": ["right", "down", "up", "left"]}。

判定。

每个答案被自动解析并与预言机比较，判定在重复次数和每个 LLM 上聚合。比较取决于类别：回答的概率与 $V(s)$ 比较相等性，命名的最佳（最差）动作与 $A^{\star}(s)$（$A^{\circ}(s)$）匹配，预测的排序与真实排序比较（允许并列），更有希望或更安全状态的答案与两个属性结果比较，声称的瓶颈针对精确瓶颈集验证，子集判定针对 $S^{\prime}$ 是否实际包含瓶颈或死胡同进行检查。

MDP ℳ + PCTL 属性
       ↓
模型检查器（Storm）
       ↓
测试预言机 V(s), Q(s,a), D(s)
       ↓
查询分类法（对象/范围/模式）
       ↓
测试用例（按难度 δ 优先排序）
       ↓
LLM 待测（事后解释器）
       ↓
判定（每个查询类别）

prompt 值用于 δ | 预期答案 | LLM 答案
1. 预言机构建
2. 测试生成与执行

图 2：我们测试方法概述。对 MDP 针对 PCTL 属性进行模型检查生成精确测试预言机（顶部）。查询分类法构建输入空间；测试用例根据从预言机值派生的诊断难度分数 $\delta$ 进行优先级排序，并渲染为待测 LLM 的提示（底部）。通过自动将 LLM 的答案与预言机比较获得判定。

6 评估

我们评估我们的方法以回答三个研究问题。

RQ1（优先级排序）：诊断排序是否揭示非平凡案例？

RQ2（区分能力）：更强的 LLMs 是否比较弱的 LLMs 通过更多测试用例？

RQ3（难度）：查询类别的难度是否不同？

6.1 实验设置

环境。

我们使用七个 MDPs，每个都配有一个可达性属性，其模型检查结果定义预言机：Frozen Lake（一个打滑的 4×4 网格世界；在不掉入洞的情况下到达目标；一个瓶颈）、Wolf–Goat–Cabbage（过河谜题；在不形成不安全对的情况下将所有物品运送到对岸；四个瓶颈）、Water Jug（经典的水量测量谜题；在动作预算内达到目标体积；无瓶颈）、Transporter（随机运动下的取货和交付任务；收集物品并将其运送到目的地；无瓶颈）、Stock Market（随机价格波动下的交易任务；在不破产的情况下达到目标投资组合价值；无瓶颈）、Job Shop（随机作业持续时间下的调度任务；在截止日期内完成所有作业；无瓶颈）和 Dam（随机流入的水位控制任务；在满足需求的同时将水库保持在安全范围内；无瓶颈）。没有瓶颈状态的环境省略三个瓶颈类别（报告为"-"）。

LLMs。

我们测试三个通过 Ollama 服务的开放权重模型，规模递增：Gemma 3 1B [36]（小型，本地运行）、Qwen3.5 [38]（较大的云模型，具有逐步推理模式）和 Gemma 4 31B [37]（较大的云模型）。统一随机（Random）回答器作为基线；最优策略根据构造在 1 处封顶。

协议。

所有模型都在温度 0（贪婪）下解码，此时它们几乎是确定性的，因此我们使用样本大小 1。测试预算是每个类别 20 个状态，根据第 5 节的诊断难度 $\delta$ 选择。答案约束为结构化 JSON，自动解析。预言机使用 Storm 模型检查器 [20] 为每个环境计算一次，并在所有模型和类别中重用。分数是 $[0,1]$ 中通过的测试用例的比例（越高越好）。我们在 Docker 容器（16 GB RAM）中执行所有实验，运行 Ubuntu 20.04.5 LTS 的 AMD Ryzen 7 7735HS（16 线程）。对于模型检查，我们使用 Storm 1.12.0。Ollama LLMs 要么托管在同一台机器上（Docker 容器外），要么托管在 Ollama 云上，通过 REST API 访问。

6.2 结果

我们首先验证选择方法本身（RQ1），然后从表中读取 LLM 性能（RQ2），最后按难度对类别进行排名（RQ3）。表 1 报告所有 LLMs 和环境的每个类别分数，图 3 按难度对查询类别进行排名。

诊断优先级排序的效果（RQ1）。

我们比较每个类别单元格中诊断优先级排序下的分数与随机状态选择下的分数；较低的优先级分数意味着优先级排序揭示了更难的案例。在所有 220 个可比单元格中，优先级排序在 75 个单元格（34.1%）中产生更难的情况，在 61 个（27.7%）中产生更容易的情况，在 84 个（38.2%）中持平。单侧 Wilcoxon 符号秩检验在 $p=0.035$ 处拒绝原假设，支持优先级 < 随机。

与机制一致，优先级排序预计不会降低每个模型的分数，实际上也没有。只有当模型真正对预言机难度（小值差距、动作歧义、边界状态）敏感时，它才会降低分数。Random 基线根据构造不敏感；其预期分数固定在答案空间的随机水平，无论选择哪些状态，因此其优先级与随机的单元格大致均分，差距是采样噪声。小型 Gemma 3 1B 出于不同原因不敏感：如下面的模型比较所示，它在大多数类别上已经处于最低水平，因此在预言机标记为困难的案例上几乎没有进一步下降的空间。这回答了 RQ1：在诊断优先级排序下，我们获得的非平凡测试用例多于随机测试优先级排序。

LLM 性能（RQ2）。

对所有环境平均，推理模型 Qwen3.5 最强，为 0.85，其次是 Gemma 4 31B，为 0.70，两者都明显高于 Random 基线 0.51。在诊断优先级排序下，小型 Gemma 3 1B 低于随机，为 0.43。拥有 11 亿参数，它不仅仅是猜测，而是在随机猜测只会得到随机水平的类别中做出错误答案。这种缺陷特定于优先级测试用例，这些用例恰好揭示了这些困难状态。在随机选择下，同一模型上升到 0.55，基本上与随机（0.54）持平，因此只有在基准集中于诊断查询时才会暴露。这回答了 RQ2：更强的模型比较弱模型和随机基线通过更多测试用例。

类别难度（RQ3）。

图 3 按所有模型和两种选择策略的平均分数对查询类别进行排名，因此排名反映了内在任务难度，而不是采样哪些状态的人为因素。最难的类别是子集中的死胡同（0.59）和最差动作（0.60），其次是子集中的瓶颈（0.63）；最容易的是二元瓶颈查询，关系型哪个是瓶颈变体为 0.72。这回答了 RQ3：类别的难度不同。

表 1：LLMs 在不同环境和查询类别中的性能。状态查询（满足属性、瓶颈）和偏好查询（最佳动作、最差动作、完整排序）沿对象维度变化；范围查询（子集中的瓶颈、子集中的死胡同）和模式查询（更有希望、更安全状态、瓶颈）覆盖范围和模式维度。单元格报告 $[0,1]$ 中的每个子类别分数；越高越好。每个单元格报告诊断优先级排序分数，然后是随机选择分数（优先级/随机）；优先级分数在优先级排序产生比随机选择更难（更低）分数时以粗体显示。

平均分数，两种选择策略的平均值（越低 = 越难）

Which is bottleneck      0.72
Full ranking             0.69
Satisfy property         0.69
Best action              0.67
More promising           0.66
Bottleneck (state)       0.66
Bottleneck in subset     0.63
Worst action             0.60
Safer state              0.60
Dead ends in subset      0.59

查询类别难度排名
维度：State | Preference | Scope | Mode

图 3：查询类别难度，两种选择策略（诊断优先级排序和随机）的平均值。越低越难；条形按分类法维度着色。

7 有效性威胁

内部。

判定依赖于将模型输出解析为结构化答案；我们通过 JSON 约束解码来缓解这一问题。贪婪解码与样本大小 1 捕获的是典型行为，而非平均行为。

外部。

结论基于七个（恰好可模型检查的）环境和三个开放权重 LLMs，可能无法转移到更大的任务或专有模型。模板是手写的且特定于环境；用不同的措辞描述相同的环境可能会改变绝对分数。

构造。

我们测试对最优行为的忠实性；通过最佳动作案例并不意味着 LLM 作为策略达到目标，也不意味着其措辞在因果上忠实于其自己的计算。难度 $\delta$（特别是介数中心性）仅对候选进行排序；判定保持精确。

结论。

优先级排序效应在所有 220 个单元格中具有统计显著性（$p=0.035$），但幅度适中。

8 结论

我们提出了一种自动化方法来测试基于 LLM 的事后解释器：概率模型检查作为精确测试预言机，查询类别的分类法构建输入空间，诊断分数对测试用例进行优先级排序。在七个环境和三个 LLMs 中，该方法清晰地区分了模型，按类别定位每个模型可以信任的地方，并且比随机选择优先处理显著更难的案例。由于相同的 LLMs 被部署在没有预言机的地方，这些结果量化了否则无法测量的信任差距。

未来工作包括使用失败的测试用例来微调解释器 [8]。

致谢

这项工作由欧盟在资助协议编号 101091783（MARS 项目）下资助。

利益披露。

作者声明他们没有竞争性财务利益。

署名与许可

本文是 arXiv 论文 Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle（arXiv:2608.30581）的中文全译。原文以 CC BY 4.0 许可发布。

译者：智测团队

原文链接：https://arxiv.org/abs/2608.30581

许可：CC BY 4.0