Formal Verification of Probabilistic Deep Reinforcement Learning Policies with Abstract Training

This conference talk presents a novel approach for quantitatively verifying probabilistic Deep Reinforcement Learning (DRL) policies through abstract training. Learn how researchers from Shanghai Key Laboratory of Trustworthy Computing and University of New Mexico tackle the challenges of formally verifying probabilistic DRL policies in safety-critical domains. The presentation addresses two major verification obstacles: reasoning about neural network probabilistic outputs for infinite state sets and the state explosion problem during model construction. Discover their innovative solution that abstracts continuous state spaces into finite discrete decision units, trains DNN policies on these units, and represents policy execution as a Markov decision model for probabilistic model checking. The approach yields tighter upper bounds on unsafe probabilities over longer time horizons more efficiently than current state-of-the-art methods. This 33-minute video was presented at the VMCAI conference (January 20-21, 2025) and sponsored by ACM SIGPLAN.