Geometric Path Enumeration Methods for Verifying ReLU Neural Networks
Presented as part of the 2020 HCSS conference.
|
Neural Networks are universal function approximation tools that learn from examples, and increasingly being used in perception and control applications. For safety and mission-critical needs, one needs assurance that a neural network will produce outputs that satisfy formal properties. Several recent methods have been proposed in this direction, including one class of geometric methods that propages sets of states through a neural network. In this talk, we review neural network execution and discuss methods targeting feedforward neural networks with ReLU activation functions and verification input/output properties. In these methods, it is critical to do range estimation efficiently, in order to determine if sets need to be split or not. These are essentially doing path enumeration for a neural network, where branches occur when the input to a ReLU can be either positive or negative. We explore a series of optimizations to this basic approach, and provide a comparison with several state-of-the-art tools from academia on a version of the ACAS Xu autonomous collision avoidance system that has been compressed using a series of neural networks.
|
Stanley Bak is an assistant professor in the Department of Computer Science at Stony Brook University investigating the verification of autonomy, cyber-physical systems, and neural networks. He strives to develop practical formal methods that are both scalable and useful, which demands developing new theory, programming efficient tools and building experimental systems.
Stanley Bak received a Bachelor's degree in Computer Science from Rensselaer Polytechnic Institute (RPI) in 2007 (summa cum laude), and a Master's degree in Computer Science from the University of Illinois at Urbana-Champaign (UIUC) in 2009. He completed his PhD from the Department of Computer Science at UIUC in 2013. He received the Founders Award of Excellence for his undergraduate research at RPI in 2004, the Debra and Ira Cohen Graduate Fellowship from UIUC twice, in 2008 and 2009, and was awarded the Science, Mathematics and Research for Transformation (SMART) Scholarship from 2009 to 2013. From 2013 to 2018, Stanley was a Research Computer Scientist at the US Air Force Research Lab (AFRL), both in the Information Directorate in Rome, NY, and in the Aerospace Systems Directorate in Dayton, OH. He helped run Safe Sky Analytics, a research consulting company investigating verification and autonomous systems, and performed teaching at Georgetown University before joining Stony Brook University as an assistant professor in Fall 2020.