Scalable High-Recall Constraint-Satisfaction-Based Information Retrieval for Clinical Trials Matching
A constraint-based matching system finds 32–72% more eligible clinical trial candidates per patient than leading AI baselines, with full reasoning transparency.
The Thesis
Recruiting enough patients for clinical trials is one of the most expensive and persistent bottlenecks in drug development — roughly 80% of trials miss their enrollment deadlines. SatIR proposes a new approach: instead of fuzzy keyword or embedding similarity search, it translates eligibility criteria into formal logical constraints and solves them mathematically against patient records. The method uses Satisfiability Modulo Theories (SMT) — a branch of automated reasoning that checks whether a set of conditions can all be satisfied simultaneously — combined with Large Language Models (LLMs) to handle the messy, ambiguous language in real trial protocols. On a benchmark of 59 patients and 3,621 trials, SatIR outperforms TrialGPT (a leading LLM-based baseline) on every retrieval metric. The catch: the benchmark is small, and translating from informal trial language to formal constraints at scale is an unsolved engineering challenge.
Catalyst
LLMs have recently become capable enough to reliably convert loosely written clinical eligibility criteria — full of implicit assumptions and hedged medical language — into structured logical expressions. Without that translation layer, formal constraint solvers had no scalable way to ingest real-world trial protocols. The proliferation of electronic health records (EHRs) and standardized medical ontologies like SNOMED-CT and ICD-10 also provides the structured patient-side data that makes constraint matching tractable.
What's New
Earlier systems like TrialGPT and embedding-based retrieval approaches treat trial matching as a semantic similarity problem: they encode both patient profiles and eligibility criteria as vectors and find approximate matches. These methods struggle when criteria involve precise numerical thresholds, logical negations, or multi-step clinical reasoning — a patient with a prior stroke may be eligible for one trial but not another based on timing, not just diagnosis. SatIR replaces similarity scoring with formal constraint solving, which produces exact matches, can explain exactly why a patient was included or excluded, and can be audited by a clinician without reverse-engineering a neural network.
The Counter
The benchmark is tiny: 59 patients is not enough to draw confident conclusions about real-world performance across diverse disease areas, institution types, or EHR formats. Converting messy clinical prose into clean formal constraints is the hardest part of this pipeline, and the paper relies on LLMs to do it — which means the system inherits all the failure modes (hallucination, inconsistency) it was designed to escape. Formal constraint satisfaction is brittle: a single incorrectly parsed threshold or missing concept in the ontology mapping produces a wrong answer with false confidence, whereas embedding similarity degrades gracefully. The 2.95-second-per-patient speed benchmark is measured over 3,621 trials; the largest trial databases have hundreds of thousands of entries, and the paper does not demonstrate scaling behavior. Finally, regulated clinical settings have strict requirements around auditability and liability for patient selection — formal methods help in principle but have not been validated by any IRB or FDA pathway.
Longs
- IQVIA (IQV) — trial recruitment operations and data services
- Veeva Systems (VEEV) — clinical data management infrastructure
- Oracle Health (ORCL) — EHR data and trial management platforms
- ICON plc (ICLR) — contract research organization directly exposed to enrollment efficiency gains
- Syneos Health (SYNH) — CRO with direct patient recruitment business
Shorts
- TrialGPT and similar LLM-only retrieval vendors — directly benchmarked and outperformed on recall and precision
- Keyword-search-based trial matching incumbents embedded in EHR platforms — their precision limitation is the paper's core motivation
- CROs relying on manual chart review for eligibility screening — automation of the constraint-checking step reduces the labor they bill for
Enablers (Picks & Shovels)
- Z3 and cvc5 — open-source SMT solver libraries the constraint engine likely depends on
- SNOMED-CT and ICD-10 ontologies — standardized medical vocabularies enabling structured patient-side matching
- ClinicalTrials.gov API — the source of trial protocol text for large-scale ingestion
- OpenAI or Anthropic LLM APIs — used to convert informal eligibility language into formal constraints
- HL7 FHIR standard — the interoperability format enabling EHR data extraction at scale
Private Watchlist
- Mendel.ai — clinical trial matching platform using structured patient data
- Trials.ai — AI-driven patient recruitment for sponsor companies
- Deep 6 AI — real-time patient identification for clinical trials
- Unlearn.ai — AI for clinical trial design and patient matching
Resources
The Paper
Clinical trials are central to evidence-based medicine, yet many struggle to meet enrollment targets, despite the availability of over half a million trials listed on ClinicalTrials.gov, which attracts approximately two million users monthly. Existing retrieval techniques, largely based on keyword and embedding-similarity matching between patient profiles and eligibility criteria, often struggle with low recall, low precision, and limited interpretability due to complex constraints. We propose SatIR, a scalable clinical trial retrieval method based on constraint satisfaction, enabling high-precision and interpretable matching of patients to relevant trials. Our approach uses formal methods -- Satisfiability Modulo Theories (SMT) and relational algebra -- to efficiently represent and match key constraints from clinical trials and patient records. Beyond leveraging established medical ontologies and conceptual models, we use Large Language Models (LLMs) to convert informal reasoning regarding ambiguity, implicit clinical assumptions, and incomplete patient records into explicit, precise, controllable, and interpretable formal constraints. Evaluated on 59 patients and 3,621 trials, SatIR outperforms TrialGPT on all three evaluated retrieval objectives. It retrieves 32%-72% more relevant-and-eligible trials per patient, improves recall over the union of useful trials by 22-38 points, and serves more patients with at least one useful trial. Retrieval is fast, requiring 2.95 seconds per patient over 3,621 trials. These results show that SatIR is scalable, effective, and interpretable.