Accountable AI with Grounded, Faithful, Consistent, Actionable Rationales: A Case Study in Clinical Trial Matching with VERDICT

AI summary

Overview

Research area: Neuro-symbolic AI for high-stakes decision-making, with clinical trial patient matching as the case study. Combines natural language processing, formal verification (SMT solvers), and clinical informatics.

Technical level: Advanced. The paper assumes familiarity with satisfiability modulo theories, LLM agent design, and clinical trial eligibility criteria, though the core accountability argument is accessible to a general AI audience.

Scope: The paper defines "accountability" in AI decisions as a four-part property (grounded, faithful, consistent, actionable) and demonstrates that an SMT-based agent called Verdict achieves it where monolithic LLM matchers fail.

What This Paper Is About

LLMs producing fluent-sounding justifications for decisions are unreliable in high-stakes settings: the explanation may not reflect the actual decision process, gaps in evidence get silently filled, identical cases get treated differently on different runs, and users cannot tell what would reverse the outcome. This paper asks whether splitting a decision task into an LLM-based language understanding stage and a solver-based decision stage can make every part of the decision — the derivation, the assumptions, and the pivot points — verifiably correct and inspectable. The authors build Verdict around clinical trial matching, where a patient's eligibility for a trial must be explained, contested, and acted upon.

Key Contributions

1. A four-pillar formulation of accountability — grounded verified rationales, faithful explicit assumptions, invariant policy consistency, and actionable pivotal conditions — with the formal definition of an accountable decision-maker returning a decision, a derivation trace, assumptions, and pivotal conditions.

2. The concept of self-faithfulness and an automatic metric for it. The paper proves that flipping a decision's declared pivotal conditions must flip the decision, and operationalizes this as PivotalFlipRate, which requires no human annotation and can be computed on any matcher.

3. The Verdict agent, which translates trial criteria, patient records, and policies into SMT constraints, derives eligibility with an SMT solver, and uses weighted MaxSMT to compute the assumptions and minimal condition changes that would reverse the verdict — making rationale-decision causality correct by construction.

4. A breadth-first empirical evaluation across two public benchmarks, three backbone LLMs per benchmark (including one open-weight model), five baselines, blinded clinician review, policy-adherence tests, counterfactual evaluation, and a manual failure analysis of all 59 TREC disagreements.

Main Findings

• Accuracy improves rather than degrades with the formal intermediate representation. Verdict posts the best F1 on every backbone tested: 0.900/0.836/0.754 on the SIGIR 2016-derived benchmark with GPT-4.1/GPT-4o/GPT-4o-mini, and 0.828/0.800/0.738 on TREC 2021 with GPT-5-mini/Claude Haiku 4.5/Qwen2.5-7B. It beats the strongest natural-language baseline by 0.04–0.10 F1 and the closest prior neuro-symbolic system (DLSC) by 0.10–0.27 F1.

• Clinicians strongly prefer Verdict's rationales. In blinded pairwise comparisons on 16 stratified patient–trial pairs from the SIGIR-derived benchmark, Verdict achieves a 90.6% tie-adjusted win rate against ZSPM and 75.0% against LlmMatch. On a 1–5 rating scale, Verdict scores 5.00 on criterion completeness, chart traceability, coherence, and actionability against ZSPM, versus 4.69/4.25/3.62/3.12 for ZSPM.

• Natural-language matchers cannot follow an explicit missing-data policy consistently. Even when policies are mechanically applied per condition and verified atomic conditions are supplied, natural-language matchers agree with the required decision in only 71–81% of cases. Verdict achieves 100% adherence for the relevant condition types.

• Stated rejection reasons often do not causally drive LLM decisions. The strongest baseline flips its verdict on only 65.0% of validated counterfactuals; LlmMatch flips on 48.9%, and explicitly prompting it to enumerate eligibility-changing conditions raises this only to 57.7%. ZSPM drops to 26.6%. Verdict's PivotalFlipRate is 1 by construction.

• Failures are concentrated upstream of the solver. Of Verdict's 59 TREC disagreements with GPT-5-mini, 53% stem from resolving unreported patient information differently than the benchmark's implicit policy, 24% from the gap between strict eligibility and TREC's broader relevance judgments, and only 17% (10 of 363 decisions, 2.8%) from semantic parsing errors.

• Smaller models can be brought up to frontier performance by distilling the formalizer. Distilling the Qwen2.5-7B formalizer raises Verdict's TREC F1 from 0.738 to 0.829, matching GPT-5-mini.

Methodology in Plain English

The researchers split clinical trial matching into two distinctly separate jobs. First, LLMs handle language: they read the trial's eligibility criteria and turn them into logical conditions (a diagnosis has a Boolean value, a lab test has a numeric range, a timing rule has a date), and they read the patient's chart to determine a value for each condition. Crucially, each condition is tagged as observed (found in the chart), imputed (filled in by an explicit policy when the chart is silent), or unresolved (no evidence and no policy applies). Second, a solver takes over: it checks whether the trial's requirements and the patient's resolved values can all be true simultaneously. If yes, the patient is eligible; if no, ineligible. The solver also emits the derivation trace.

To produce assumptions and pivotal conditions, the authors run a weighted maximum-satisfiability solver twice. One run asks: what is the smallest set of patient values that would have to be false to make the patient eligible? The other asks the mirror question: what is the smallest set that would have to change to make an eligible patient ineligible? Whichever direction does not match the actual decision becomes the reported pivotal conditions. A final LLM call phrases all of this in clinician-readable prose, but is forbidden from inventing content — it merely verbalizes the solver's output. This architecture means that any error the system makes can be traced either to the solver (which is provably correct) or to the language stage (which is inspectable and correctable), never to a hidden reasoning step.

Why This Matters

Impact on research. The paper reframes accountability as an architectural property rather than a model-quality property, and shows it is achievable by construction rather than by better calibration or higher accuracy. The self-faithfulness metric is cheap and task-agnostic, giving the community a way to test whether an explanation actually causes a decision without human annotation. It also delivers a cautionary result: adding a symbolic solver to an LLM pipeline is not automatically sufficient — DLSC, the closest prior neuro-symbolic matcher, still trails Verdict substantially because it lacks explicit handling of missing evidence and policies.

Real-world applications:

• Clinical trial screening. Coordinators get defensible, verifiable reasons for every exclusion decision, plus a list of what tests or records would need to change for a patient to qualify.
• Credit and lending. A rejected applicant receives the actual reason for denial rather than a plausible-sounding one, along with concrete guidance on what to improve before reapplying.
• Insurance and benefits adjudication. Identical applications are provably treated identically, and policy-driven defaults for missing information are logged and overridable.
• Regulatory and compliance audit. Auditors can rerun decisions against revised assumptions and trace every claim back to its source text.

Industry relevance. Any sector under regulatory pressure to explain automated decisions — healthcare, financial services, insurance, hiring — can adopt the pattern of confining language models to information extraction and routing the decision itself through a verifiable solver. The distillation result also matters commercially: a small open-weight model brought up to frontier performance via formalizer distillation makes accountable architectures affordable at deployment scale.

Future Directions

• Reducing language-stage errors. Since 53% of remaining failures come from how unreported patient information is resolved, better formalization and evidence extraction — or learning institutional policies from historical decisions — is the highest-leverage next step.

• Stronger counterfactual validation. The current self-faithfulness evaluation relies on LLM-generated counterfactual records (roughly 80% clinician-validated) and tests only the ineligible-to-eligible direction. Multi-clinician, bidirectional, larger-scale audits would strengthen the evidence, and the eligible-to-ineligible direction remains untested empirically.

• Extending the framework beyond binary eligibility. The formalism in principle covers any constrained decision task with policies, but the paper only demonstrates trial matching. Loan approval, benefits determination, and resource allocation are natural unattested targets.

• Scaling to criteria not decidable from the chart. Cases requiring operational judgments or information outside the patient record (5% of failures here) point to a hybrid design where some conditions are delegated back to human reviewers with an explicit audit trail.

Target Audience

Researchers and practitioners building decision systems in regulated or high-stakes domains, especially clinical informatics and NLP engineers working on LLM-plus-solver architectures. Also valuable for AI ethics and policy researchers interested in operational definitions of accountability, for clinicians and trial coordinators who consume these systems, and for graduate students studying neuro-symbolic methods or explanation faithfulness — the formal definitions in Section 2 are self-contained enough to be useful even to readers who skip the implementation details.

Authors’ abstract

Accountability means a decision can be examined, justified, and contested. LLMs make this hard: fluent output may be ungrounded, incomplete, or unfaithful to the decision process. Achieving accountability requires verified rationales (how was the decision reached), assumptions (what was assumed rather than known), policy consistency (the same treatment for the same facts), and pivotal conditions (what would change the outcome). We introduce self-faithfulness as an automatic test of accountability: changing the pivotal conditions should change the decision. We examine accountable AI through clinical trial matching, a high-stakes task central to evidence-based medicine. Although LLM-based matchers match patients to trials reasonably accurately, they apply decision policies inconsistently and produce rationales that are unfaithful to their own decisions. We introduce VERDICT, an LLM-based agent that translates a decision task, its constraints, and its policy into Satisfiability Modulo Theories (SMT), then derives the decision with SMT and MaxSMT solvers -- so policies are applied consistently and decisions are accountable by construction. Across a SIGIR 2016-derived dataset and TREC 2021, VERDICT achieves the strongest decision accuracy among LLM-only and neurosymbolic baselines, applies policies with perfect consistency, and produces clinician-preferred rationales grounded in explicit assumptions and pivotal conditions, with improved counterfactual self-faithfulness.