A contrastive decision transformer with TLA⁺ formal verification for sepsis treatment recommendation

Sepsis is a life-threatening disease with a high mortality rate, and its treatment involves multiple interventions, placing stringent demands on the timeliness and safety of clinical decision-making. Decision Transformer (DT) has demonstrated considerable potential in generative sequence modeling and decision recommendation tasks, providing a new paradigm for treatment decision-making in complex clinical settings. However, existing studies have mainly focused on improving long-term policy returns and offline evaluation performance, while lacking safety verification of decision outcomes. In addition, Decision Transformer often struggles to accurately achieve specified target returns because of limitations in target-return alignment. To address these issues, this study proposes a decision verification framework integrated with TLA⁺. An action-contrastive module is introduced into the original Decision Transformer, resulting in the proposed AC-DT model, which explicitly models the matching relationship between state contexts and actions through a contrastive loss, thereby enhancing the model's ability to distinguish among different treatment strategies. Furthermore, SHAP attribution analysis is employed to select key state variables, and the treatment trajectories generated by the model are abstracted into symbolic sequences with explicit clinical semantics to support TLA⁺ specification modeling and TLC model checking. Experimental results show that AC-DT achieves favorable estimated returns on MIMIC-III and in external evaluation on eICU. Moreover, the TLC model checker can effectively identify abnormal decision trajectories that violate predefined clinical safety properties.