Timezone: »

 
Spotlight Poster
Provably Bounding Neural Network Preimages
Suhas Kotha · Christopher Brix · J. Zico Kolter · Krishnamurthy Dvijotham · Huan Zhang

Wed Dec 13 08:45 AM -- 10:45 AM (PST) @ Great Hall & Hall B1+B2 #713
in Poster Session 3 »
Most work on the formal verification of neural networks has focused on bounding the set of outputs that correspond to a given set of inputs (for example, bounded perturbations of a nominal input). However, many use cases of neural network verification require solving the inverse problem, or over-approximating the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set, which can be combined with branch-and-bound to increase precision. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. We demonstrate our algorithm for identifying safe control regions for a dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we find over-approximations over $2500\times$ tighter than prior work while being $2.5\times$ faster. By strengthening robustness verification with output constraints, we consistently verify more properties than the previous state-of-the-art on multiple benchmarks, including a large model with 167k neurons in VNN-COMP 2023. Our algorithm has been incorporated into the $\alpha,\beta$-CROWN verifier, available at https://abcrown.org.

Author Information

Suhas Kotha (Carnegie Mellon University)
Christopher Brix (RWTH Aachen University, Rheinisch Westfälische Technische Hochschule Aachen)
J. Zico Kolter (Carnegie Mellon University / Bosch Center for AI)

Zico Kolter is an Assistant Professor in the School of Computer Science at Carnegie Mellon University, and also serves as Chief Scientist of AI Research for the Bosch Center for Artificial Intelligence. His work focuses on the intersection of machine learning and optimization, with a large focus on developing more robust, explainable, and rigorous methods in deep learning. In addition, he has worked on a number of application areas, highlighted by work on sustainability and smart energy systems. He is the recipient of the DARPA Young Faculty Award, and best paper awards at KDD, IJCAI, and PESGM.

Krishnamurthy Dvijotham (DeepMind)

Krishnamurthy Dvijotham is a research scientist at Google Deepmind. Until recently, he was a research engineer at Pacific Northwest National Laboratory (PNNL) in the optimization and control group. He was previously a postdoctoral fellow at the Center for Mathematics of Information at Caltech. He received his PhD in computer science and engineering from the University of Washington, Seattle in 2014 and a bachelors from IIT Bombay in 2008. His research interests span stochastic control theory, artificial intelligence, machine learning and markets/economics, and his work is motivated primarily by problems arising in large-scale infrastructure systems like the power grid. His research has won awards at several conferences in optimization, AI and machine learning.

Huan Zhang (UIUC)

More from the Same Authors