VERDICT makes LLM clinical trial matching auditable via SMT

Clinical trial matching systems built on large language models produce rationales that don't actually track how they decided, and they apply the same eligibility rule inconsistently across cases. A team writing on arxiv proposes fixing that with VERDICT, an LLM agent that translates the decision task, its constraints and its policy into satisfiability modulo theories, then hands the call to SMT and MaxSMT solvers.

The authors introduce 'self-faithfulness' as an automatic accountability test: 'changing the pivotal conditions should change the decision.' On that measure, ordinary LLM matchers 'apply decision policies inconsistently and produce rationales that are unfaithful to their own decisions,' the paper reports. VERDICT, by contrast, is 'accountable by construction' because the solver enforces the policy.

Across a SIGIR 2016-derived dataset and TREC 2021, the paper reports 'the strongest decision accuracy among LLM-only and neurosymbolic baselines,' with policies applied at 'perfect consistency' and rationales clinicians preferred. No per-benchmark accuracy figures appear in the abstract. Two of the researchers on our Who's Who radar circulated it.