cs.AIFeb 16, 2026

Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC

Authors: Dennis Gross

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Safe and interpretable sequential decision-making is critical in healthcare, yet reinforcement learning (RL) policies for sepsis treatment optimization remain opaque and difficult to verify. Standard probabilistic model checkers operate on the full state space, which becomes infeasible for larger MDPs, and cannot explain why a learned policy makes particular decisions. COOL-MC wraps the model checker Storm but adds three key capabilities: it constructs only the reachable state space induced by a trained policy, yielding a smaller discrete-time Markov chain amenable to verification even when full-MDP analysis is intractable; it automatically labels states with clinically meaningful atomic propositions; and it integrates explainability methods with probabilistic computation tree logic (PCTL) queries to reveal which features drive decisions across treatment trajectories. We demonstrate COOL-MC's capabilities on the ICU-Sepsis MDP, a benchmark derived from approximately 17,000 sepsis patient records, which serves as a case study for applying COOL-MC to the formal analysis of sepsis treatment policies. Our analysis establishes hard bounds via full MDP verification, trains a safe RL policy that achieves optimal survival probability, and analyzes its behavior via PCTL verification and explainability on the induced DTMC. This reveals, for instance, that our trained policy relies predominantly on prior dosing history rather than the patient's evolving condition, a weakness that is invisible to standard evaluation but is exposed by COOL-MC's integration of formal verification and explainability. Our results illustrate how COOL-MC could serve as a tool for clinicians to investigate and debug sepsis treatment policies before deployment.

Figures & tables

Figure 3. State handling example within COOL-MC. Internally, COOL-MC uses PRISM’s integer state encoding for model checking. Whenever a state is passed to the policy, an explainability method, or state labeling, the observation function O\displaystyle\mathbb{O} maps it to its corresponding 47-dimensional observation, enabling decisions, analyses, and annotations based on clinically meaningful patient characteristics.
IDDescriptionPCTL PropertyProb.
2maxBest achievable survivalPmax⁡(◊ survived)\displaystyle P_{\max}(\lozenge\ \texttt{survived})0.8751
2minWorst-case survivalPmin⁡(◊ survived)\displaystyle P_{\min}(\lozenge\ \texttt{survived})0.633
2aBest clean survival (no severe organ failure)Pmax⁡( ¬high_sofa U survived)\displaystyle P_{\max}(\ \neg\texttt{high\_sofa}\ \mathcal{U}\ \texttt{survived})0.4667
2bWorst clean survival (no severe organ failure)Pmin⁡( ¬high_sofa U survived)\displaystyle P_{\min}(\ \neg\texttt{high\_sofa}\ \mathcal{U}\ \texttt{survived})0.2986
2cMin. deaths without organ failurePmin⁡( ¬high_sofa U died)\displaystyle P_{\min}(\ \neg\texttt{high\_sofa}\ \mathcal{U}\ \texttt{died})0.0504
2dUnavoidable low blood pressurePmin⁡(◊ low blood pressure)\displaystyle P_{\min}(\lozenge\ \texttt{low blood pressure})0.5274
Table 1. Full MDP analysis: best-case and worst-case probabilities over all possible treatment policies. Labels, such as high_sofa , are atomic propositions assigned to states.
IDDescriptionPCTL PropertyProb.
5aSurvival probabilityP=?(◊  survived)\displaystyle P_{=?}(\lozenge\;\texttt{survived})0.8751
5bDeath probabilityP=?(◊  died)\displaystyle P_{=?}(\lozenge\;\texttt{died})0.1249
6aSurvive via no-treatment pathP=?(fl0_vp0  U  survived)\displaystyle P_{=?}(\texttt{fl0\_vp0}\;\mathcal{U}\;\texttt{survived})0.2159
6bReach max fluids, no vasopressorsP=?(◊  fl4_vp0)\displaystyle P_{=?}(\lozenge\;\texttt{fl4\_vp0})0.5414
6cReach max fluids + max vasopressorsP=?(◊  fl4_vp4)\displaystyle P_{=?}(\lozenge\;\texttt{fl4\_vp4})0.1029
7aReach state with input_4hourly as most important featureP=?(◊  imp_input_4hourly)\displaystyle P_{=?}(\lozenge\;\texttt{imp\_input\_4hourly})1.0
Table 2. Trained policy (induced DTMC Dπ\displaystyle D^{\pi} ): baseline outcomes and treatment trajectory properties. Action labels flivpj\displaystyle\texttt{fl}_{i}\texttt{vp}_{j} encode IV-fluid level i\displaystyle i and vasopressor level j\displaystyle j ( 0\displaystyle 0 = none, 4\displaystyle 4 = maximum).
Figure 4. Feature importance ranking via feature pruning. Each bar shows the change in survival probability when the corresponding feature fi\displaystyle f_{i} is removed from the policy’s input. The feature input_4hourly dominates, indicating the policy relies heavily on the previous dosing window.
More in this topic

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 323 papers

Explore similar work

CardsList
Mar 2, 2026

COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management

Platelets expire within five days. Blood banks face uncertain daily demand and must balance ordering decisions between costly wastage from overstocking and life-threatening shortages from understocking. Reinforcement learning (RL) can learn effective ordering policies for this Markov decision process (MDP), but the resulting neural policies remain black boxes, hindering trust and adoption in safety-critical domains. We apply COOL-MC, a tool that combines RL with probabilistic model checking and explainable RL, to verify and explain a trained policy for the MDP on platelet inventory management inspired by Haijema et al. By constructing a policy-induced discrete-time Markov chain (which includes only the reachable states under the trained policy to reduce memory usage), we verify PCTL properties and provide feature-level explanations. Results show that the trained policy achieves a 2.9% stockout probability and a 1.1% inventory-full (potential wastage) probability within a 200-step horizon, primarily attends to the age distribution of inventory rather than other features such as day of week or pending orders. Action reachability analysis reveals that the policy employs a diverse replenishment strategy, with most order quantities reached quickly, while several are never selected. Counterfactual analysis shows that replacing medium-large orders with smaller ones leaves both safety probabilities nearly unchanged, indicating that these orders are placed in well-buffered inventory states. This first formal verification and explanation of an RL platelet inventory management policy demonstrates COOL-MC's value for transparent, auditable decision-making in safety-critical healthcare supply chain domains.

Dennis Gross

Inventory ControlReinforcement LearningInterpretability in RLFormal Verification
AskPDF
Jul 7, 2026

EHR-MPC: Inference-Time Control for Sepsis Treatment with Generative Patient Digital Twins

Sepsis is a leading cause of mortality, yet optimal treatment policies remain contested. Existing reinforcement learning (RL) approaches learn fixed strategies for sepsis treatment, limiting adaptability to changing clinical objectives during inference. We propose EHRMPC, a framework that decouples learning patient dynamics from optimizing treatment by training a patient digital twin in the form of a generative electronic health record (EHR) model. The digital twin predicts clinical trajectories under interventions and enables model predictive control (MPC) to optimize treatments via inference-time planning over simulations. We evaluate EHR-MPC on a multicenter ICU sepsis cohort spanning 8 hospitals in the Mass General Brigham health system using both off-policy importance sampling and on-policy simulation-based evaluation. Relative to RL baselines, EHR-MPC achieves comparable off-policy performance and improved simulation performance. Unlike RL, this work frames sepsis treatment optimization as inference-time control over learned patient dynamics, establishing a general framework for decision making with generative clinical models.

Joshua Pickard, Wei Qi, Na Li +4

Broad Institute of MIT and Harvard · Harvard University · Brigham and Women’s Hospital +2

Inference-Time OptimizationModel Predictive Control
AskPDF
Aug 3, 2026

Robust Counterfactual Policy Optimisation via Nondeterministic Causal Models

Counterfactual inference approaches for sequential decision-making typically assume deterministic causal models, where all randomness stems from latent variables. However, Markov Decision Processes (MDPs) are inherently stochastic. We address this by formalising counterfactual policy optimisation under probabilistic nondeterministic causal models, which properly separates latent confounding from irreducible stochasticity, and here propose a first practical optimisation problem for identifying robust counterfactual policies under a sensitivity analysis framework. We validate our approach on a sepsis treatment simulator, where diabetes status acts as a hidden global confounder.

Jessica Lally, Milad Kazemi, Nicola Paoletti +2

1King’s College London · 2Durham University · University College London

Markov Decision ProcessesStructural Causal ModelsPolicy OptimizationCausal Inference
AskPDF