Generating probabilistic safety guarantees for neural network controllers

DOI10.1007/S10994-021-06065-9zbMATH Open1518.68211arXiv2103.01203MaRDI QIDQ6134350FDOQ6134350

Authors: Sydney M. Katz, Kyle D. Julian, Christopher A. Strong, Mykel J. Kochenderfer 

Publication date: 22 August 2023

Published in: Machine Learning (Search for Journal in Brave)

Abstract: Neural networks serve as effective controllers in a variety of complex settings due to their ability to represent expressive policies. The complex nature of neural networks, however, makes their output difficult to verify and predict, which limits their use in safety-critical applications. While simulations provide insight into the performance of neural network controllers, they are not enough to guarantee that the controller will perform safely in all scenarios. To address this problem, recent work has focused on formal methods to verify properties of neural network outputs. For neural network controllers, we can use a dynamics model to determine the output properties that must hold for the controller to operate safely. In this work, we develop a method to use the results from neural network verification tools to provide probabilistic safety guarantees on a neural network controller. We develop an adaptive verification approach to efficiently generate an overapproximation of the neural network policy. Next, we modify the traditional formulation of Markov decision process (MDP) model checking to provide guarantees on the overapproximated policy given a stochastic dynamics model. Finally, we incorporate techniques in state abstraction to reduce overapproximation error during the model checking process. We show that our method is able to generate meaningful probabilistic safety guarantees for aircraft collision avoidance neural networks that are loosely inspired by Airborne Collision Avoidance System X (ACAS X), a family of collision avoidance systems that formulates the problem as a partially observable Markov decision process (POMDP).

Full work available at URL: https://arxiv.org/abs/2103.01203

Recommendations

• Learning safe neural network controllers with barrier certificates
• Learning safe neural network controllers with barrier certificates
• Verisig 2.0: verification of neural network controllers using Taylor model preconditioning
• An abstraction-based framework for neural network verification
• Verifying low-dimensional input neural networks via input quantization

zbMATH Keywords

verificationmodel checkingsafetyneural network controller

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Specification and verification (program logics, model checking, etc.) (68Q60) Adaptive control/observation systems (93C40) Control/observation systems involving computers (process control, etc.) (93C83)

Cites Work

• On the Theory of Dynamic Programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• Variable resolution discretization in optimal control
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Reachability analysis for neural feedback systems using regressive polynomial rule inference
• Verisig
• Decision making under uncertainty. Theory and application. With contributions from Christopher Amato, Girish Chowdhary, Jonathan P. How, Hayley J. Davison Reynolds, Jason R. Thornton, Pedro A. Torres-Carrasquillo, N. Kemal Üre and John Vian

Cited In (5)

• Learning safe neural network controllers with barrier certificates
• Learning safe neural network controllers with barrier certificates
• Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming
• Neural flocking: MPC-based supervised learning of flocking controllers
• Risk verification of stochastic systems with neural network controllers

This page was built for publication: Generating probabilistic safety guarantees for neural network controllers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6134350)