Verifying the Safety of Autonomous Systems with Neural Network Controllers
Radoslav Ivanov, Taylor J. Carpenter, James E. Weimer, Rajeev Alur, George J. Pappas, Insup Lee · ACM Transactions on Embedded Computing Systems · 2020
This article addresses the problem of verifying the safety of autonomous systems with neural network (NN) controllers. We focus on NNs with sigmoid/tanh activations and use the fact that the sigmoid/tanh is the solution to a quadratic differential equation. This allows us to convert the NN into an equivalent hybrid system and cast the problem as a hybrid system verification problem, which can be solved by existing tools. Furthermore, we improve the scalability of the proposed method by approximating the sigmoid with a Taylor series with worst-case error bounds. Finally, we provide an evaluation over four benchmarks, including comparisons with alternative approaches based on mixed integer linear programming as well as on star sets.