Safeguarding Neural Network-Controlled Systems via Formal Methods: From Safety-by-Design to Runtime Assurance (Invited Talk)

Neural networks (NNs) exhibit remarkable potential in decision-making and control systems. While neural networks can be trained by sophisticated Deep Reinforcement Learning (DRL) techniques to achieve optimal system performance under various constraints, a significant concern persists: the lack of provable safety guarantees for the trained decision-making models. The intrinsic complexity and opacity of these models make it profoundly challenging to rigorously guarantee their safety under various hosting environments, including the systems they control. Drawing on our experiences, we contend that formal methods are crucial for developing neural network controllers that are not only robust but also certifiable, thereby ensuring system safety from training through deployment. We demonstrate that integrating formal methods into learning process is essential to provide a comprehensive safety guarantee for the controlled systems across their entire design, training, and execution lifecycle.