PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Zikai Zhou, Yufei Jin, Yilin Xu, Yu-Chiang Wang, Chieh-Ju Chao, Monica S. Lam

arXiv:2609.03366v1cs.CLcs.CYcs.LO

TL;DR

LLM-based clinical-trial matchers can be accurate while producing ungrounded rationales, hidden assumptions, and inconsistent policy application. VERDICT translates the task into SMT and MaxSMT representations so solvers derive decisions and accountability artifacts; across two benchmarks, it reports stronger accuracy, perfect policy consistency, and clinician-preferred rationales, while remaining dependent on upstream LLM translation and evidence extraction.

  • Problem

    LLM matchers can be reasonably accurate yet produce ungrounded or unfaithful rationales, hide assumptions, and apply policies inconsistently in clinical-trial matching.

  • Method

    VERDICT separates language understanding from decision making by using LLMs for formalization and SMT/MaxSMT solvers to derive decisions, assumptions, and pivotal conditions.

  • Results

    VERDICT outperforms strong LLM-only and neurosymbolic baselines, follows policies reliably, produces clinician-preferred rationales, and has perfect rationale-decision causality by construction.

  • Takeaways & Limitations

    Formal methods make VERDICT’s decisions, traces, assumptions, and pivotal conditions inspectable and reviewable within its formal representation.

  • Takeaways & Limitations

    VERDICT can still be wrong when LLMs miss patient facts, extract incorrect evidence, or formalize requirements incorrectly; solver verification does not guarantee clinical correctness of the representation.

Abstract

from arXiv · show

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.

1 Introduction

Accountability requires decisions to be examined, justified, contested, and actionable, but fluent LLM outputs can remain ungrounded, unfaithful, assumption-hiding, and policy-inconsistent. VERDICT addresses these gaps by separating language understanding from SMT-based decision making and exposing verifiable derivations, assumptions, and pivotal conditions.

  • Accountability requires decisions to be examined, justified, and contested after the fact.
  • LLMs can produce fluent output that is ungrounded, incomplete, or unfaithful to the process generating a decision.
  • Verified rationales must trace the decision process, while explicit assumptions expose judgments made when evidence is ambiguous or incomplete.
  • Policy consistency requires identical facts to receive the same treatment whenever the same policy recurs.
  • Clinical-trial LLM matchers are reasonably accurate but fall short on all four accountability criteria.
  • VERDICT separates language understanding from decision making via SMT, producing formal derivations, overrideable assumptions, and actionable pivotal conditions.

2 Accountable Decision Making

The paper defines accountable decision making through a decision, its derivation, assumptions, and pivotal conditions. It introduces self-faithfulness as the requirement that changing identified pivotal conditions changes the decision, enabling automatic accountability evaluation.

  • An accountable decision maker returns a decision together with a verifiable derivation, overrideable assumptions, and actionable pivotal conditions.
  • Self-faithfulness requires changing identified pivotal conditions to change the decision in the corresponding direction.
  • The counterfactual construction CF(x, Π, δ) minimally modifies a case so that its pivotal conditions no longer hold.
  • Theorem 1 states that DECIDE flips its decision when the pivotal conditions are flipped.
  • Theorem 1 yields an automatic accountability metric that requires no external annotation.

3 VERDICT Clinical Trial Matcher

VERDICT decomposes clinical-trial matching into language formalization and symbolic decision making. LLMs construct trial and patient representations, while SMT and MAXSMT derive eligibility, traces, assumptions, and pivotal conditions that support inspectable rationales and self-faithful counterfactuals.

  • VERDICT formalizes natural-language trial requirements and resolves patient evidence under policies into structured condition representations.
  • Each patient condition records a value, resolution status, supporting evidence, and any policy-based imputation.
  • The representation distinguishes observed, imputed, and unresolved conditions, while the current formulation represents all unresolved conditions with ⊥.
  • SMT derives eligibility from the formal constraints and resolved patient values, with SAT indicating eligibility and UNSAT indicating ineligibility.
  • MAXSMT computes minimal condition changes and assumptions by treating trial constraints as hard and resolved conditions as weighted soft clauses.
  • VERDICT is self-faithful over its formal representation: counterfactually changing returned pivotal conditions flips the eligibility decision.
  • Its accountability remains bounded by possible LLM errors in translating text, extracting evidence, or applying policies.

4 Experimental Setup

The evaluation uses two independently constructed clinical-trial matching benchmarks and compares VERDICT with LLM-only and neurosymbolic systems across complementary model families. The setup includes both derived and official eligibility judgments, with all systems evaluated on shared patient–trial pairs.

  • The evaluation uses two benchmarks with independently constructed eligibility labels.
  • Benchmarks: The SIGIR 2016-derived benchmark contains 552 patient–trial pairs labeled by a five-judge GPT-5 panel and partially validated by a clinician.
  • Benchmarks: The TREC 2021 benchmark contains 363 patient–trial pairs with official eligibility judgments and was not used for method development or policy construction.
  • Systems: Baselines include optimized direct matching, chain-of-thought matching, zero-shot matching, TrialGPT-Matching, and a dynamic logical solver composition system.
  • Model suites: All systems use the same backbone and patient–trial pairs, with GPT-4.1, GPT-4o, and GPT-4o-mini tested on SIGIR and proprietary and open-weight models tested on TREC.

5 Evaluation

VERDICT preserves or improves matching accuracy while adding solver-derived rationales, explicit assumptions, policy consistency, and testable pivotal conditions. Across evaluations, natural-language matchers remain less consistent and less self-faithful, while clinicians prefer VERDICT’s rationales.

  • 5.1 Decision Accuracy: VERDICT achieves the highest F1 across all backbones on both clinical-trial benchmarks.
  • 5.1 Decision Accuracy: 0.900, 0.836, and 0.754 F1 are achieved with GPT-4.1, GPT-4o, and GPT-4o-mini on the SIGIR-derived benchmark.
  • 5.1 Decision Accuracy: 0.04–0.10 F1 over the strongest natural-language baseline and 0.10–0.27 F1 over DLSC are achieved on TREC 2021.VERDICT’s corresponding accuracies are 0.838, 0.815, and 0.697 across the three backbones.
  • 5.1 Decision Accuracy: Missing-evidence imputations account for 31/59 disagreements, while semantic parsing errors affect only 10 of 363 final decisions.The remaining disagreements include mismatches with broader TREC relevance judgments and non-chart-decidable criteria.
  • 5.2 Grounding and Actionability: Clinicians prefer VERDICT rationales, with 90.6% and 75.0% tie-adjusted win rates against ZSPM and LLMMATCH, respectively.
  • 5.2 Grounding and Actionability: VERDICT receives higher mean ratings on all five rationale dimensions against both comparators.Solver traces support completeness, traceability, and coherence, while assumptions and pivotal conditions support actionability and decision support.
  • 5.3 Consistency: Natural-language matchers follow the specified policy in only 71–81% of cases, even when policies are applied per criterion.Applying policies per criterion significantly improves adherence over structured evidence alone (McNemar’s exact test, p < 0.01).
  • 5.4 Self-Faithfulness: Natural-language matchers flip only 65.0%, 48.9%, and 57.7% of validated decisions after stated rejection conditions are addressed.The 57.7% rate is obtained by LLMMATCH-Pivotal, which explicitly enumerates changes required for eligibility.

6 Related Work

Related work combines clinical-trial matching, LLM–symbolic reasoning, faithful explanations, and algorithmic accountability. VERDICT differs by making executable representations authoritative for decisions, policies, assumptions, and pivotal conditions rather than using symbolic execution mainly to improve accuracy or reliability.

  • Clinical trial matching and retrieval: Clinical-trial matching spans executable cohort queries, LLM-based matching, and symbolic formalization for high-recall retrieval.
  • LLM–symbolic reasoning and faithful execution: Prior LLM–symbolic systems translate natural-language problems into logical forms or execute explicit reasoning representations to improve reliability.
  • LLM–symbolic reasoning and faithful execution: VERDICT uses executable representations to define the authoritative decision state from which verdicts, policies, assumptions, and pivotal conditions are mechanically derived.
  • LLM–symbolic reasoning and faithful execution: The paper argues that symbolic execution alone need not outperform strong natural-language approaches; gains require explicit treatment of missing evidence, assumptions, and decision policies.
  • Faithful explanations and accountable decisions: Accountability and faithful-explanation research motivates inspectable decisions, causal-faithfulness tests, and outcome-changing conditions.

7 Conclusion

The paper frames accountable AI as necessary for high-stakes decisions and presents VERDICT as a way to make clinical-trial matching inspectable, contestable, and reviewable. Its formal separation of language understanding from decision reasoning leaves interpretation errors possible while making reasoning errors transparent and correctable.

  • Accountability in clinical-trial matching requires reliable rationales so clinicians can verify decisions and manage care.
  • VERDICT separates language understanding from reasoning and constrains the LLM to produce explicit, auditable representations.Errors may remain in patient-record interpretation or formalization, but the decision process becomes transparent and reviewable.
  • Formal methods provide accountability, transparency, and contestability by construction for critical domains such as healthcare.

Limitations

VERDICT's accountability mechanisms remain bounded by upstream language-model errors, counterfactual-generation choices, one-direction evaluation, imperfect benchmark labels, and synthetic records.

  • Upstream representation: LLM errors in formalizing criteria, extracting evidence, or representing policies can still produce incorrect decisions despite verifiable SMT reasoning.The solvers verify reasoning over the encoded representation, not its clinical correctness.
  • Counterfactual evaluation: Counterfactual self-faithfulness estimates depend on LLM-generated patient edits and validation, although a clinician-audited subset provides adjusted estimates.End-to-end failures may also arise from rewriting or re-parsing the modified record rather than from incorrect pivotal conditions.
  • Evaluation scope: The empirical self-faithfulness test changes initially ineligible cases toward eligibility, leaving the reverse direction and evolving patient states untested.Testing both directions would provide a more complete evaluation.
  • Benchmark validity: The benchmarks imperfectly represent strict clinical eligibility because their judgments concern retrieval, SIGIR labels use a five-judge LLM panel, and missing-information policies remain implicit.The SIGIR candidate set is also restricted to top-ranked retrieved trials rather than the full corpus.
  • Data realism: Both benchmarks use synthetic patient records, which may underrepresent the noise, conflicting evidence, missingness, and temporal complexity of real electronic health records.The paper identifies testing on real records with privacy safeguards and prospective clinical review as future work.

Ethical Considerations

The paper frames VERDICT as decision support for high-stakes clinical matching, combining LLM-based interpretation with explicit, solver-derived artifacts while retaining human oversight and upstream risks.

  • Human oversight: VERDICT is intended to surface candidate matches, imputations, and assumptions, not to autonomously enroll or exclude patients.Final eligibility decisions should remain under qualified clinical and trial-site review.
  • Accountability design: Separating clinical text interpretation from eligibility reasoning makes the encoded decision explicit, rerunnable, and interpretable.The pipeline compiles criteria and patient information, evaluates their conjunction with SMT/MAXSMT, and verbalizes the solver output.
  • Residual risk: Missed evidence, incorrect extraction, or faulty formalization can still yield wrong verdicts because formal reasoning does not guarantee clinical correctness.Upstream LLM stages remain responsible for parsing trial criteria and patient records.
  • Evidence handling: Patient parsing is restricted to predicates required by each trial, and unsupported predicates remain unbound rather than being extracted indiscriminately.Separate inclusion and exclusion passes apply side-appropriate missing-evidence handling.
  • Decision procedure: The solver determines eligibility with Z3 and uses weighted optimization to compute a minimum-cost pivotal-condition flip set for ineligible patients.The combined formula is the conjunction of trial and patient constraints.
  • Review artifacts: The solver returns a decision trace, assumptions, and pivotal conditions, while the verbalizer produces a clinician-facing rationale for review.These artifacts correspond to deterministic solver stages followed by natural-language verbalization.

B Baseline implementations

The baseline implementations compare multiple LLM prompting, criterion-labeling, and aggregation strategies, with development-split selection determining the configurations reported in the main results.

  • Baseline suite: Four LLM-based baselines—LLMMATCH, CoT LLM, TrialGPT-Matching, and ZSPM—use the same patient records, trial criteria, and backbone models as VERDICT.The appendix describes each baseline's structured output, binary-verdict aggregation, and prompt.
  • TrialGPT-Matching: TrialGPT-Matching classifies inclusion and exclusion criteria separately, then adds a deterministic binary aggregation rule because its original component lacks a patient-level verdict.The permissive rule performed best on the development split and was reported in the main results.
  • ZSPM: ZSPM assigns each criterion an is_met judgment, confidence label, and rationale before aggregating criterion-level outputs into a patient-level verdict.The main evaluation maps its ternary might-be-eligible category to eligible because that mapping performed better on development data.
  • CoT LLM: CoT LLM reports the strongest chain-of-thought-shaped variant: aggregation-first verbose CoT with side-specific labels.Generic-label and single-pass CoT variants underperformed it on the development split.
  • LLMMATCH: LLMMATCH uses a two-pass prompt that produces structured per-criterion assessments before aggregating them into one eligibility verdict.Its reported configuration was selected from six prompts spanning reasoning structure, vocabulary specificity, and verbosity.
  • LLMMATCH: The strongest LLMMATCH variant was think-then-aggregate, selected on the development split and used in the main paper.The model reasons criterion by criterion before emitting the global verdict.

E.1 Pair A

The examples show how VERDICT and other matchers handle incomplete clinical evidence differently. VERDICT treats missing information as requiring confirmation while still producing an eligible decision when no exclusion is triggered.

  • Pair A: obstructive sleep apnea: VERDICT labels the obstructive-sleep-apnea case eligible because core symptoms are documented and no exclusion is triggered.It identifies missing information for later confirmation rather than treating every unmentioned criterion as disqualifying.
  • Pair A: obstructive sleep apnea: LLMMATCH returns ineligible after emphasizing that chart information about medical history, medication changes, and other criteria is unavailable.Its rationale highlights missing evidence rather than resolving those conditions under the same prescreening interpretation.
  • Pair A: obstructive sleep apnea: CoT LLM also returns eligible, applying a prescreen-doctrine interpretation to unknown criteria.Its aggregation reasoning treats unresolved, non-population-defining inclusion and exclusion criteria as satisfied or not excluded.
  • Pair B: pulmonary embolism: For the pulmonary-embolism case, VERDICT returns eligible because the patient meets the minimum age requirement and no exclusion is triggered.Diagnostic, risk-stratification, and safety criteria remain undocumented and require confirmation at screening.
  • Pair B: pulmonary embolism: The pulmonary-embolism evidence illustrates the scope of the decision: only age is confirmed, while the remaining criteria must be verified at the in-person visit.The case includes missing imaging, hemodynamic, biomarker, procedural, bleeding-risk, and follow-up information.

F Dataset Statistics

The evaluation uses a 552-pair SIGIR-derived set and an independent TREC 2021 benchmark, with analyses of coverage, system outputs, disagreement, and clinician–reference agreement. The reference panel is scalable but is not treated as a clinical gold standard.

  • Evaluation datasets: 552 of 590 SIGIR-derived patient–trial pairs receive complete five-judge coverage, yielding 278 eligible and 274 ineligible labels.The 552-pair set contains 59 patients paired with their top-10 TrialGPT-Retrieval candidates.
  • Evaluation datasets: The 38 excluded SIGIR pairs are diffusely distributed across patients and retrieval ranks, suggesting that the final set preserves the original candidate-pool structure.No patient loses more than four pairs, and dropped pairs show no monotonic retrieval-rank pattern.
  • Evaluation datasets: The TREC 2021 evaluation contains 363 pairs with compiled eligibility programs, sampled from a class-balanced pool and held out from method development.The evaluation set is near-parity at 52.3% eligible rather than reflecting the judged pool’s base rate.
  • System outputs: VERDICT and ZSPM track the reference base rate more closely than LLMMATCH and CoT LLM, which are markedly ineligibility-leaning.On the 552-pair set, VERDICT labels 55.4% eligible and ZSPM 54.0%, versus 35.0% for LLMMATCH and 36.1% for CoT LLM.
  • Reference judgments: Within the GPT-5 reference panel, 446 of 552 pairs receive unanimous 5–0 verdicts, while 106 pairs receive split judgments.The remaining pairs split 4–1 or 3–2, explaining why a single-call matcher may diverge from consensus.
  • Clinician audit: After structured re-review, clinician–reference agreement is high under both ambiguity conventions: κ=0.67 with half-credit and κ=0.97 under the lenient convention.Raw agreement is 81.3% and 96.9%, respectively; these results support relative system comparison without equating the panel with clinician-adjudicated gold.

I.7 Limitations

The audit and benchmark construction have important scope limitations. The reference labels are scalable rather than clinician-equivalent, and the clinician re-review was a single-rater, exposed, audit-and-resolve process.

  • Audit limitations: Only one expert clinician was available, so the audit cannot estimate a clinician–clinician agreement ceiling.This limits interpretation of clinician–reference agreement as a measure of clinical consensus.
  • Audit limitations: The re-review exposed the clinician to the reference panel’s verdict and reasoning rather than using blinded independent re-annotation.The design was intended to resolve disagreements by distinguishing reference errors from differing interpretations of the same chart.
  • Audit limitations: The clinician retained the ability to disagree after exposure to the reference reasoning, as shown by the single UNCHANGED case.This demonstrates non-forced agreement but does not remove the design’s exposure-related limitation.
  • Scope of claims: The authors do not claim that the LLM reference panel is clinician-equivalent.Their narrower claim concerns apparent disagreements in audit cells where reference errors would most affect system comparison.
  • Benchmark limitations: SIGIR-derived eligibility labels come from a five-judge LLM panel rather than a multi-clinician adjudication and cover only top-ranked retrieved trials.The original SIGIR judgments concern referral relevance, not eligibility, and the panel labels therefore have a restricted scope.

K Detailed Results

The detailed analyses show that VERDICT’s accuracy, rationale preferences, and counterfactual self-faithfulness remain strong under clinician review, alternative ambiguity handling, and population reweighting. Its counterfactual behavior is tied to formal decision boundaries rather than merely plausible explanations.

  • Clinician-adjusted accuracy: Clinician-adjusted accuracy preserves VERDICT’s strong ranking across backbones, with the best lenient F1 for GPT-4.1, GPT-4o, and GPT-4o-mini.Lenient and half-credit conventions produce nearly identical rankings.
  • Rationale preference: Clinicians prefer VERDICT’s rationales over ZSPM and LLMMATCH, especially for actionability, support, chart traceability, and logical consistency.The preference persists even in strata where the comparator matches the reference label and VERDICT does not.
  • Counterfactual self-faithfulness: VERDICT-E2E tests self-faithfulness by rewriting patient charts, validating the edits, and rerunning the full pipeline rather than directly changing solver atoms.This separates counterfactual rewriting and semantic-parsing errors from mismatches between rationales and formal decision boundaries.
  • Counterfactual self-faithfulness: VERDICT-E2E has the highest flip rate across modifier–validator settings when cited blockers are removed.Its flip set contains minimal patient facts, imputations, or assumptions whose changes make the constraints satisfiable.
  • Counterfactual self-faithfulness: Free-text flip targets improve LLMMATCH only limitedly, indicating that naming targets does not reliably recover the matcher’s actual decision boundary.This supports the finding that plausible rationales can omit blockers sufficient to change the model’s own verdict.
  • Overall interpretation: The appendix concludes that VERDICT combines strong accuracy with more preferred rationales and substantially better counterfactual self-faithfulness, although it is not uniformly best on every aggregate accuracy metric.These conclusions remain robust to clinician adjustment, ambiguity conventions, and population reweighting.

L Semantic Parsing Audit

The semantic-parsing audit finds high preservation of formalized eligibility meaning, while decision-level errors remain limited but consequential across patient–trial pairs. The appendix also identifies deployment boundaries involving asymmetric error costs, missingness policies, documentation disparities, and synthetic benchmark data.

  • Formalization accuracy: 99.6% condition accuracy was achieved across 1,092 atomic conditions, while 94.3% of 348 criteria were fully correct.The remaining criterion-level errors primarily involved nesting, conditional structure, negation, and omitted conditions.
  • Decision-level impact: 2.8% of final decisions were changed by semantic parsing across 363 patient–trial pairs, despite 5.7% of audited criteria containing structural or completeness issues.Semantic parsing was the smallest major identified source of end-to-end error among 59 TREC disagreements.
  • Potential risks: F1 and accuracy weight error directions equally even though false INELIGIBLE and false ELIGIBLE outcomes have different deployment harms.The missingness policy can trade precision for recall by leaving undocumented criteria UNRESOLVED rather than imputing them absent.
  • Potential risks: Missingness policy is a value judgment that can disadvantage patients with sparse documentation, and the study did not measure subgroup disparities because its synthetic charts lacked reliable demographic strata.Making the policy explicit supports auditing but is not itself a remedy.
  • Potential risks: Formal solver traces verify decisions over the encoded program, but the encoding itself remains LLM-generated and is where most residual error lives.Interfaces should give extracted evidence and source criteria at least as much prominence as solver output.
  • Deployment boundary: The evaluation uses synthetic, compact, internally consistent charts, whereas real records are longer, redundant, contradictory, and harder for temporal reasoning.Reference labels are also imperfect, with about a quarter of TREC disagreements attributed to label noise or relevance–eligibility mismatch.

N Computational Experiments

The computational appendix documents the model backbones, solver infrastructure, API and GPU budgets, runtime, dependencies, and reproducibility materials. It also records dataset and language-scope limitations relevant to interpreting the experiments.

  • API calls: VERDICT’s SIGIR matcher uses approximately 4,000 GPT-4.1 calls per cross-backbone row, while the three additional SIGIR backbones add about 12,000 calls.Baselines contribute approximately 15,000 calls across matching tables.
  • API calls: The counterfactual sweep uses about 25,000 calls across three cells and seven systems, and the five-judge reference panel uses 2,950 GPT-5 calls plus up to 375 re-review calls.The pairwise rationale judge adds approximately 160 GPT-5 calls.
  • Computational budget: Approximately 60,000–70,000 LLM calls were used across all experiments, with end-to-end metered cost of about $2,500 including failed runs and early sweeps.Final reportable runs cost under $1,000.
  • Local GPU: Qwen2.5-7B-Instruct inference and distillation use single NVIDIA RTX A6000 GPUs, with 89 single-GPU jobs and no distributed training.Each job had a wall-clock limit between 2 and 10 hours.
  • Infrastructure and reproducibility: Z3 returns in single-digit milliseconds per pair, below per-pair LLM latency, and non-LLM computation runs on one workstation without GPU or distributed compute.Pinned dependencies, prompts, sampling parameters, and seeds are documented for reimplementation.
  • Scope: Both benchmarks contain English synthetic patient cases paired with ClinicalTrials.gov criteria, limiting evaluation to English clinical trial matching.The paper documents prompts, matcher configurations, solver outputs, and related artifacts.
Loading 2609.03366v1…