![[2602.14505] Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC](https://arxiv.org/static/browse/0.3.4/images/arxiv-logo-fb.png){kind=logo}
[2602.14505] Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC
Summary
This paper presents COOL-MC, a tool for verifying and explaining sepsis treatment policies using reinforcement learning, enhancing decision-making transparency in healthcare.
Why It Matters
The integration of formal verification and explainability in sepsis treatment policies is crucial for improving patient outcomes. By addressing the opacity of RL models, COOL-MC offers a method to ensure safer and more interpretable healthcare decisions, which is vital in critical care settings.
Key Takeaways
- COOL-MC enhances verification of RL policies by focusing on reachable state spaces.
- It integrates explainability with probabilistic computation tree logic (PCTL) for better decision insights.
- The tool reveals critical weaknesses in treatment policies, such as over-reliance on prior dosing history.
- Demonstrated effectiveness on a benchmark derived from 17,000 sepsis patient records.
- COOL-MC can assist clinicians in debugging and validating treatment policies before implementation.
Computer Science > Artificial Intelligence arXiv:2602.14505 (cs) [Submitted on 16 Feb 2026] Title:Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC Authors:Dennis Gross View a PDF of the paper titled Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC, by Dennis Gross View PDF HTML (experimental) 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 b...
