Search papers, labs, and topics across Lattice.
This paper introduces a novel neural network verification technique called partial multi-neuron relaxation, which selectively applies multi-neuron relaxation to a heuristically chosen subset of neurons to balance tightness and scalability. By focusing multi-neuron relaxation on critical neurons, the method achieves tighter bounds than single-neuron relaxation without the computational cost of full multi-neuron relaxation. Experiments within the Marabou verifier demonstrate improved performance compared to existing bound tightening methods.
Achieve tighter neural network verification bounds without sacrificing scalability by strategically applying multi-neuron relaxation to only the most critical neurons.
The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network's non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.
