2020/04/16 by Haimin Hu, Hu, Haimin, Mahyar Fazlyab +5 · 6 citations
Computer Science · Engineering · Mathematics · #Adversarial Robustness in Machine Learning #FOS: Computer and information sciences #FOS: Electrical engineering #FOS: Mathematics #Fault Detection and Control Systems #Formal Methods in Verification #Machine Learning (cs.LG) #Optimization and Control (math.OC) #Systems and Control (eess.SY) #cs.LG #cs.SY #eess.SY #electronic engineering #information engineering #math.OC
paper · pdf · doi:10.48550/arxiv.2004.07876
arxiv created 2020/04/16 · openalex publication_date 2020/04/16 · arxiv updated 2020/04/20 · openalex created_date 2020/04/24 · openalex updated_date 2026/07/28
There has been an increasing interest in using neural networks in closed-loop control systems to improve performance and reduce computational costs for on-line implementation. However, providing safety and stability guarantees for these systems is challenging due to the nonlinear and compositional structure of neural networks. In this paper, we propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback interconnection. Our technical approach relies on abstracting the nonlinear activation functions by quadratic constraints, which leads to an outer-approximation of forward reachable sets of the closed-loop system. We show that we can compute these approximate reachable sets using semidefinite programming. We illustrate our method in a quadrotor example, in which we first approximate a nonlinear model predictive controller via a deep neural network and then apply our analysis tool to certify finite-time reachability and constraint satisfaction of the closed-loop system.