Zikai Zhou, Yufei Jin, Yilin Xu, Yu-Chiang Wang, Chieh-Ju Chao, Monica S. Lam
6 min
Clinical trial matching is a high-stakes task where LLMs often produce fluent but ungrounded or inconsistent decisions. This paper investigates how to make AI-driven clinical trial matching accountable, ensuring that decisions are not just accurate, but also inspectable, consistent, and actionable for clinicians.
To address the limitations of monolithic LLM matchers, the authors introduce VERDICT, a neuro-symbolic framework. VERDICT decomposes the matching process into two distinct stages:
By using solvers, the system guarantees that policies are applied consistently. Furthermore, the solver trace provides a formal derivation, explicit assumptions about missing data, and pivotal conditions—the minimal changes required to reverse an eligibility decision.
Across two benchmarks (SIGIR 2016-derived and TREC 2021), VERDICT achieves the highest decision accuracy among both LLM-only and neuro-symbolic baselines. Beyond accuracy, the system demonstrates perfect policy consistency and produces clinician-preferred rationales. Crucially, VERDICT exhibits significantly higher counterfactual self-faithfulness: when the system identifies a condition as pivotal, changing that condition reliably flips the eligibility decision, a property that natural-language models often fail to satisfy.
Accountability is a prerequisite for deploying AI in high-stakes medical settings. By separating language parsing from decision logic, VERDICT provides a framework where clinicians can verify the reasoning behind a decision, override specific assumptions, and understand exactly what information is needed to change an outcome. This approach moves AI matching from a black-box process to an auditable decision-support tool.
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.
Sam: [measured] That's the critical vulnerability, and the framework addresses it through a two-stage parsing process. First, a projection rewriter maps trial criteria into typed signatures with self-contained definitions. The parser isn't guessing what "stable medical history" means — it's given a strict, chart-checkable definition for every predicate.
Alex: [processing] So it's not just asking the model to interpret the criteria — it's providing a controlled vocabulary that constrains how the model interacts with the chart.
Sam: [nodding] Exactly. The parser, which the authors call PPARSE, only extracts facts relevant to those specific defined predicates. Anything unsupported by the record is left unbound rather than inferred. For numerical data, missing evidence is handled by applying institutional policies rather than letting the model fill in gaps. And if the parser finds an inconsistency — say, a conflict between a patient's current and historical states — an arbiter re-reads the chart to resolve it.
Alex: [probing] What if the arbiter still can't resolve the conflict?
Sam: [calm] It defaults to a safe state. If the arbiter can't determine a faithful correction, it returns no override, and the solver proceeds with the raw extraction. The system prioritizes exposing the conflict over forcing a decision. You get a transparent failure rather than a masked one.
Alex: [thoughtful] That's a sensible fail-safe. But how do we know the solver's output is actually reproducible? If it's running an optimization, couldn't it return different solutions for the same input? [[RP_SECTION:solver-logic-and-reproducibility|Solver Logic and Reproducibility]]
Sam: [measured] That's a subtle point worth unpacking. The solver uses Z3 to find an optimum, and yes, different solutions can satisfy the same constraints. But the eligibility verdict itself is invariant — it depends on satisfiability, not on which specific solution the solver happens to return. The authors distinguish between forced entries, which are canonical, and alternative or inert entries, which reflect the search process. The decision is logically robust even if the rationale's internal trace varies slightly.
Alex: [realizing] So the variability is in the "how" of the rationale, not the "what" of the decision.
Sam: [quiet confidence] Precisely. The language model handles the semantic mapping; the solver enforces the logical truth. It's a clean separation of concerns, and it's what makes the verdict auditable in a way that a model's internal activations never could be.
Alex: [leaning in] So how much of the performance gain is actually attributable to the solver's logic versus the more constrained input representation? Could you get most of the benefit just from better-structured prompting? [[RP_SECTION:clinical-utility-and-auditability|Clinical Utility and Auditability]]
Sam: [measured] The solver is the load-bearing component, but the two are tightly coupled. PPARSE is essential because it anchors the model's extraction to a strict vocabulary — without that, the solver is just executing well-formatted garbage. But the real value the solver adds is making the decision boundary *explicit*. It doesn't just produce a verdict; it produces a formal trace of which constraints were satisfied or violated. That's what turns an opaque prediction into an actionable checklist.
Alex: [deliberate] Right — the difference between a model saying "I think this patient is ineligible" and a system showing you the exact criterion, a specific lab value threshold, that triggered the rejection.
Sam: [grounded] And that auditability is what makes it clinically useful rather than just technically interesting. The authors suggest that integrating this framework directly with structured electronic health records could eventually bypass the LLM parsing step entirely — if you have structured data, you don't need to extract it from free text. But for now, the system is designed to expose its own extraction failures rather than mask them behind a confident binary verdict.
Alex: [reflective] That's an honest trade-off. The framework doesn't eliminate the LLM's role as a potential point of failure — it just makes that failure visible. Which, in a high-stakes clinical context, might be exactly the right design priority.
Sam: [measured, closing] That's the argument the paper makes. Verifiability doesn't mean perfection. It means that when the system is wrong, you can find out *why* — and that's a meaningful step forward for deploying AI in settings where the cost of an opaque error is high. Thanks for listening to ResearchPod.