Stanford CS224V Lecture 11: Translate Trial Criteria into SMT Instead of Asking an LLM to Decide
The lecture parses patient records and trial criteria into SMT, retrieves candidates through a weaker propositional projection, and runs a solver on the reduced set. Reasoning is inspectable, but NL-to-SMT remains the main error boundary.