具有基于事实、忠实、一致、可操作理由的问责制AI：VERDICT在临床试验匹配中的案例研究

# 可解释AI与基于依据、忠实、一致且可操作的决策依据：以临床试验匹配案例研究Verdict系统为例
来源：https://arxiv.org/html/2609.03366

Zikai Zhou  
机构：美国加州斯坦福大学计算机科学系  
邮箱：[[email protected]](mailto:)

Yufei Jin  
机构：美国加州洛杉矶分校Samueli电气与计算机工程系  
邮箱：[[email protected]](mailto:)

Yu-Chiang Wang, Chieh-Ju Chao  
机构：美国明尼苏达州罗切斯特市梅奥诊所

Monica S. Lam  
机构：美国加州斯坦福大学计算机科学系

###### 摘要
可解释性意味着决策可被审视、辩护和质疑。大语言模型（LLM）在这方面存在挑战：流畅的输出可能缺乏依据、不完整，或与决策过程不一致。实现可解释性需要经验证的决策依据（决策如何得出）、假设（哪些被假定而非已知）、策略一致性（相同事实获得相同处理）以及关键条件（哪些因素会改变结果）。我们提出“自忠实性”作为可解释性的自动测试方法：改变关键条件应导致决策变化。我们以临床试验匹配——这一以证据为基础的核心高风险医疗任务为例研究可解释AI。尽管基于LLM的匹配系统能较准确地将患者与试验匹配，但它们策略应用不一致，且产生的决策依据与自身决策不一致。我们提出Verdict¹（代码、提示与评估工具包：https://github.com/stanford-oval/clinical-trial-matching），这是一种基于LLM的智能体，它将决策任务、约束条件及策略转化为可满足性模理论（SMT），再通过SMT和MaxSMT求解器推导决策——从而确保策略一致性，使决策具有天然的可解释性。在SIGIR 2016和TREC 2021衍生的数据集上，Verdict在纯LLM及神经符号基线中取得了最强的决策准确率，策略应用完全一致，并生成了临床医生偏好的、基于明确假设和关键条件的决策依据，同时提升了反事实自忠实性。

## 1 引言
可解释性是指决策事后可被审视、辩护和质疑的特性：他人能询问原因、了解哪些条件是被假定而非已知、确信决策过程一致，并明确什么会改变结果（Kroll 2015；Binns 2018；Diakopoulos 2015）。可解释性是任何必须被理解、信任和执行的重大决策背后的核心操作要求。例如，它意味着向患者说明他们不符合临床试验资格的真实原因，澄清对缺失化验结果的假设，解释什么会改变结果，并确信若患者采纳建议，决策确实会被推翻。类似地，它包括向被拒贷款申请人提供拒绝的真实理由及重新申请前的明确改进方向，并确保所有资质相似的申请人获得平等对待。它还意味着判定驾驶员享有安全驾驶折扣，但需警告若其发生责任事故，该折扣将被取消。

LLM输出流畅且自信，无论其是否基于事实、完整或忠实于生成过程——即“幻觉”。在重大决策场景中，这导致四种失败模式，每种都需要应对措施：

1.  **依据性——经验证的依据**：陈述的原因未必是产生决策的真实原因——解释是为了听起来合理而生成，并非追溯推导过程。我们需要与产生决策的进程核对或由此推导的、经验证的依据。
2.  **忠实性——假设**：提供的证据常模糊或不完整；然而LLM倾向于用无根据的自信默默填补空白。我们需要明确记录每一项假设，将无声的判断转变为可审计的声明。
3.  **一致性——策略遵守**：由于LLM用语言重新推导其推理，形式上相同的案例可能在不同场合由不同逻辑决定。我们需要策略一致性来保证，当相同事实再现时，同一策略始终以相同方式应用。
4.  **可操作性——关键条件**：为具有建设性，决策应附带如何逆转的解释。我们需要提供关键条件——能改变决策的最小变化。

这四者共同构成了可解释性的支柱——有依据、忠实、一致且可操作的推理。需注意，传统意义上的“可信度”提升均未解决这些问题：更好的校准或更高的准确率仍留有这四个缺口，因为可解释性是决策及其推导的属性，而非模型的记录属性。

##### 临床试验匹配。我们以临床试验匹配为例研究可解释AI，其中临床医生希望指定处理缺失数据的策略，验证依据是否忠实于决策，并理解可能改变结果的假设和关键条件。我们发现，基于LLM的匹配系统（Jin等人，2024；Gupta等人，2024；Wornow等人，2025）虽具备合理准确度，但在所有四项可解释性标准上均显不足。另一种方法是将语言模型与符号推理结合，将匹配问题表示为SMT（可满足性模理论）公式，并由Z3等求解器（De Moura和Bjørner，2008）执行（Ye等人，2023；Olausson等人，2023；Xu等人，2026；Pan等人，2023）。SatIR（Zhou等人，2026）将插补的缺失数据表示为SMT，提高了检索准确率和召回率，但使用LLM确定最终资格。在此基础上，我们提出Verdict（可验证解释、假设披露、不变一致性和可追溯关键点），这是一个用于可解释决策的框架。给定一个检索到的候选患者，Verdict决定其是否符合试验资格。我们采用SatIR的试验表示法，但提取与每个试验相关的患者信息以提高准确性。Verdict使用SMT求解器确定资格；求解器追踪产生匹配证据和明确假设，而MaxSMT求解器（De Moura和Bjørner，2008；Bjørner等人，2015）计算关键条件——改变决策所需的最小约束变化。

##### 贡献
- • **将临床试验匹配构建为可解释决策问题**：给定决策、约束及其策略，可解释智能体应一致应用策略，并产生决策，同时附带（1）用户可验证的形式化推导，（2）用户可覆盖的其背后假设，及（3）用户可操作或监控的关键条件。
- • **Verdict：一个通过SMT分离语言理解与决策的可解释决策框架**：与整体式LLM匹配器不同，其不准确性局限于语言理解，而非决策逻辑，且根本原因可直接从表示中观察到。Verdict的决策附带可验证的正确推导、明确假设和关键条件。
- • **在准确性、可解释性和可操作性方面的广泛评估**：跨两个公共基准、多个模型家族、临床医生审查、策略遵守测试、反事实评估和失败分析。Verdict优于强大的纯LLM及神经符号基线，产生临床医生偏好的依据，可靠遵循策略，并具有完美的依据-决策因果关系。

图1：**Verdict概览**。整体式LLM匹配器（*上图*）一步断言资格决定。Verdict（*下图*）分解任务：LLM处理语言，将试验形式化为要求φ_t，并在策略Π下解析患者证据为o_{t,Π}，标记每个标准为已观察、已插补或未解决。求解器处理决策：SMT推导决策d及追踪γ；MaxSMT推导假设ρ和关键条件δ。最后的LLM步骤将其转化为面向临床医生的依据η。由于决策是推导而非断言产生的，每个产物均可检查、覆盖和重新运行。

## 2 可解释决策
本节，我们定义可解释决策的一般问题，并引入“自忠实性”作为可解释决策者的基本属性。

### 2.1 可解释性的定义
一个可解释的决策者不仅提供决策，还提供解释其如何推导的依据、其依赖的隐藏假设（以便在适当时可被覆盖），以及可改变以逆转决策的关键条件。

###### 定义1。给定约束规范y、案例x和策略集Π，可解释决策者定义为：Decide(y, x, Π) = (d, γ, ρ, δ)，其中d ∈ {eligible, ineligible}是资格决策，
- • *决策追踪*γ记录从输入推导d的逻辑过程；
- • *假设*ρ是决策进行时既未由x也未由Π确立的取值，表明需要哪些信息或行动来确定资格；
- • *关键条件*δ是其解决或改变会逆转决策的条件。根据定义，δ ≠ ∅。

### 2.2 可解释决策者具有自忠实性
我们提出“自忠实性”概念来评估决策者。如果决策者将某些条件识别为关键，那么改变这些条件应改变结果。这一期望双向适用。在医学中，患者可能因试验限于IV期癌症而不符合资格；若患者进展到IV期，决策应从不合格变为合格。反之，患者可能因肾功能在要求范围内而符合资格；若后续检测低于排除阈值，决策应从合格变为不合格。此概念适用于更广泛的可解释决策，不仅限于医学。例如，驾驶员可能因近期事故不符合安全驾驶折扣资格，但足够多年的无事故后可再次获得资格；反之，目前符合折扣资格的驾驶员，若发生责任事故则应失去资格。在每种情况下，所述关键条件应预期能决定决策方向。

###### 定义2。给定案例x、策略Π和决策依赖的条件值集δ，反事实构造CF(x, Π, δ)表示δ不再成立的最小修改案例。

###### 定理1。Decide函数对其关键条件具有自忠实性：如果案例的关键条件被翻转，决策也将翻转。给定约束规范y、案例x和策略Π，若(d, γ, ρ, δ) = Decide(y, x, Π)，(d', γ', ρ', δ') = Decide(y, CF(x, Π, δ), Π)，则 d ≠ d'。

### 2.3 评估自忠实性
定理1产生了一个自动评估指标，无需外部标注，可衡量决策者实现的可解释性。

###### 定义3。给定决策者实现DM、策略Π和评估实例集M = {(y1, x1), ..., (yn, xn)}，定义关键翻转率 PivotalFlipRate(DM, M, Π) = \frac{1}{|M_δ|} \sum_{j \in M_δ} \mathbb{I}\left[d_j \neq d'_j\right]，其中(d_j, γ_j, ρ_j, δ_j) = DM(y_j, x_j, Π)，(d'_j, γ'_j, ρ'_j, δ'_j) = DM(y_j, CF(x_j, δ_j), Π)。

###### 推论1。给定策略Π和评估实例集M = {(y1, x1), ..., (yn, xn)}，PivotalFlipRate(Decide, M, Π) = 1。

## 3 Verdict临床试验匹配器
图1概览了Verdict及其中间产物。我们将临床试验匹配分解为语言理解和决策：LLM将试验标准、患者记录和策略解析为形式化表示，而SMT和MaxSMT求解器推导决策及可解释依据。接下来我们定义表示并介绍Verdict算法。

### 3.1 形式化SMT表示
给定用自然语言书写的试验、患者记录和策略，临床试验匹配问题是产生患者是否符合资格的决策及可解释依据。策略定义了当患者记录中未明确时应如何解决条件。它们可编码常见做法、机构选择或默认用户假设。策略有两种类型：第一种依赖于试验的完整上下文和策略集中的其他规则；第二种纯粹取决于约束的种类。原则上，此类策略也可能依赖于约束的解决状态（例如，可用患者证据的强度或方向）；但在当前表述中，所有未解决的条件由单一未知值⊥表示。

试验表示基于SatIR（Zhou等人，2026）中引入的语义形式化。SatIR将自然语言资格标准分解为原子类型化条件及其逻辑组合，产生此处使用的试验端约束表示。Verdict通过基于患者证据固定条件并在策略下解析缺失值，将此表示从检索扩展到决策。

###### 定义4。试验t的自然语言*资格要求*形式化为逻辑表达式 φ_t = φ(c_1, ..., c_n)，其中c = (τ, V, u, ℓ) ∈ C表示...