Compositional Learning and Verification of Neural Network Controllers

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Radoslav Ivanov ◽  
Kishor Jothimurugan ◽  
Steve Hsu ◽  
Shaan Vaidya ◽  
Rajeev Alur ◽  
...  

Recent advances in deep learning have enabled data-driven controller design for autonomous systems. However, verifying safety of such controllers, which are often hard-to-analyze neural networks, remains a challenge. Inspired by compositional strategies for program verification, we propose a framework for compositional learning and verification of neural network controllers. Our approach is to decompose the task (e.g., car navigation) into a sequence of subtasks (e.g., segments of the track), each corresponding to a different mode of the system (e.g., go straight or turn). Then, we learn a separate controller for each mode, and verify correctness by proving that (i) each controller is correct within its mode, and (ii) transitions between modes are correct. This compositional strategy not only improves scalability of both learning and verification, but also enables our approach to verify correctness for arbitrary compositions of the subtasks. To handle partial observability (e.g., LiDAR), we additionally learn and verify a mode predictor that predicts which controller to use. Finally, our framework also incorporates an algorithm that, given a set of controllers, automatically synthesizes the pre- and postconditions required by our verification procedure. We validate our approach in a case study on a simulation model of the F1/10 autonomous car, a system that poses challenges for existing verification tools due to both its reliance on LiDAR observations, as well as the need to prove safety for complex track geometries. We leverage our framework to learn and verify a controller that safely completes any track consisting of an arbitrary sequence of five kinds of track segments.

Author(s):  
Radoslav Ivanov ◽  
Taylor Carpenter ◽  
James Weimer ◽  
Rajeev Alur ◽  
George Pappas ◽  
...  

AbstractThis paper presents Verisig 2.0, a verification tool for closed-loop systems with neural network (NN) controllers. We focus on NNs with tanh/sigmoid activations and develop a Taylor-model-based reachability algorithm through Taylor model preconditioning and shrink wrapping. Furthermore, we provide a parallelized implementation that allows Verisig 2.0 to efficiently handle larger NNs than existing tools can. We provide an extensive evaluation over 10 benchmarks and compare Verisig 2.0 against three state-of-the-art verification tools. We show that Verisig 2.0 is both more accurate and faster, achieving speed-ups of up to 21x and 268x against different tools, respectively.


2021 ◽  
Vol 20 (1) ◽  
pp. 1-26
Author(s):  
Radoslav Ivanov ◽  
Taylor J. Carpenter ◽  
James Weimer ◽  
Rajeev Alur ◽  
George J. Pappas ◽  
...  

Sign in / Sign up

Export Citation Format

Share Document