Efficient Neural Network Analysis with Sum-of-Infeasibilities

TL;DR

This paper introduces DeepSoI, a novel stochastic method leveraging sum-of-infeasibilities to analyze neural network verification queries more efficiently, outperforming existing verifiers and aiding adversarial robustness assessments.

Contribution

It proposes the Sum-of-Infeasibilities (SoI) framework and DeepSoI algorithm, enhancing neural network verification by guiding search and improving bounds with convex relaxations.

Findings

DeepSoI improves verification performance over existing methods.

SoI-based techniques outperform state-of-the-art verifiers.

The approach efficiently enhances adversarial perturbation bounds.

Abstract

Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex relaxation which over-approximates the non-convex activation functions, we encode the violations of activation functions as a cost function and optimize it with respect to the convex relaxation. The cost function, referred to as the Sum-of-Infeasibilities (SoI), is designed so that its minimum is zero and achieved only if all the activation functions are satisfied. We propose a stochastic procedure, DeepSoI, to efficiently minimize the SoI. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with DeepSoI. Extending the complete search with DeepSoI achieves multiple simultaneous goals: 1) it guides the search towards a counter-example; 2) it enables more informed branching decisions; and 3) it creates additional opportunities for bound derivation. An extensive evaluation across different benchmarks and solvers demonstrates the benefit of the proposed techniques. In particular, we demonstrate that SoI significantly improves the performance of an existing complete search procedure. Moreover, the SoI-based implementation outperforms other state-of-the-art complete verifiers. We also show that our technique can efficiently improve upon the perturbation bound derived by a recent adversarial attack algorithm.