#formal-methods

把臨床試驗條件翻成 SMT，而不是讓 LLM 直接判資格｜Stanford CS224V 第 11 堂

這堂把病人紀錄與試驗條件各自轉成 SMT，先以較弱的命題邏輯投影做大規模候選檢索，再用 solver 檢查候選；推理可解釋，但 NL-to-SMT 仍是主要錯誤入口。