Verisig is a tool for verifying safety properties of autonomous systems with neural network (NN) controllers. Verisig supports sigmoid and tanh-based networks and exploits the fact that the sigmoid (and the tanh) is the solution to a quadratic differential equation, which allows us to transform the neural network into an equivalent hybrid system. By composing the network's hybrid system with the plant's, Verisig transforms the problem into a hybrid system verification problem which can be solved using state-of-the-art reachability tools. Specifically, Verisig uses Flow* to solve the resulting hybrid system reachability problem. Verisig is available at verisig.org, and the code can be found at https://github.com/verisig.
This work is supported in part by the DARPA Assured Autonomy program.
ORGANIZATION
The University of Pennsylvania, Philadelphia, Pennsylvania,USA
Radoslav Ivanov
Taylor J. Carpenter
James Weimer
Rajeev Alur
George J. Pappas
Insup Lee