Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning
This addresses safety verification for critical systems using deep reinforcement learning, offering a scalable solution for high-dimensional domains, though it is incremental by building on existing shielding methods.
The paper tackles the scalability limitations of verifying safety in learning-enabled controllers for high-dimensional and complex systems, achieving effective synthesis of safe controllers in benchmarks with hundreds of dimensions and stochastic properties.
There has been significant recent interest in devising verification techniques for learning-enabled controllers (LECs) that manage safety-critical systems. Given the opacity and lack of interpretability of the neural policies that govern the behavior of such controllers, many existing approaches enforce safety properties through shield, a dynamic monitoring-and-repairing mechanism that ensures a LEC does not emit actions that would violate desired safety conditions. These methods, however, have been shown to have significant scalability limitations because verification costs grow as problem dimensionality and objective complexity increase. In this paper, we propose a new automated verification pipeline capable of synthesizing high-quality safe controllers even when the problem domain involves hundreds of dimensions, or when the desired objective involves stochastic perturbations, liveness considerations, and other complex non-functional properties. Our key insight involves separating safety verification from neural controller training, and using pre-computed verified safety shields to constrain the training process. Experimental results over a range of high-dimensional benchmarks demonstrate the effectiveness of our approach in a range of stochastic linear time-invariant and time-variant systems.