Search papers, labs, and topics across Lattice.
The paper introduces COOL-MC, a tool for formally verifying and explaining reinforcement learning policies for sepsis treatment by constructing a reachable state space induced by the policy, labeling states with clinically meaningful propositions, and integrating explainability methods with PCTL queries. This approach overcomes the limitations of standard model checkers that operate on the full state space, which is infeasible for large MDPs. Applied to the ICU-Sepsis MDP, COOL-MC revealed that a trained RL policy relied heavily on prior dosing history, a previously undetected weakness, demonstrating its potential for debugging treatment policies.
RL policies for sepsis treatment may have hidden flaws undetectable by standard evaluation, like over-reliance on prior dosing, but COOL-MC exposes these weaknesses through formal verification and explainability.
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.
