使用模型检查作为判定标准的基于 LLM 的事后解释器自动化测试

大语言模型（LLM）被用作序列决策策略的事后解释器，用自然语言解释某个动作为何被选中。然而，LLM 常常生成看似合理但错误的陈述，而且现有方法尚不能系统地测试这类解释是否忠实于底层环境。这里有两个经典的软件测试难题：一是没有用于判断解释正确性的判定标准，二是测试输入——关于策略行为的自然语言查询——缺乏进行系统化测试用例生成所需的结构。我们同时解决这两个问题。概率模型检查提供了测试判定标准，可计算精确的参考结果，并据此自动评估 LLM 的回答。一个事后查询类别的分类体系围绕由环境层面事实构成的策略解释来组织输入空间；由此生成的测试用例根据特定问题的诊断难度分数进行优先排序。在七个 MDP 环境中，该测试将三种开源权重 LLM 区分开来：一种推理模型通过了 85% 的测试用例，一种中等规模模型通过了 70%，而一个 1B 模型的表现甚至低于随机基线；与此同时，优先排序显著筛选出了比随机选择更难的案例。我们的结果表明，在无模型设置下，LLM 生成的解释有多可信——在这种设置中使用的是同样的 LLM，但不存在可用于验证它们的判定标准。