A Sequential Framework Towards an Exact SDP Verification of Neural Networks
This work provides an incremental improvement for safety-critical applications by enhancing exact verification methods for neural networks.
The paper tackles the problem of certifying neural network robustness for safety-critical systems by addressing the large relaxation gap in semidefinite programming (SDP) approaches, and shows that their sequential framework with non-convex cuts shrinks this gap to zero as cuts increase.
Although neural networks have been applied to several systems in recent years, they still cannot be used in safety-critical systems due to the lack of efficient techniques to certify their robustness. A number of techniques based on convex optimization have been proposed in the literature to study the robustness of neural networks, and the semidefinite programming (SDP) approach has emerged as a leading contender for the robust certification of neural networks. The major challenge to the SDP approach is that it is prone to a large relaxation gap. In this work, we address this issue by developing a sequential framework to shrink this gap to zero by adding non-convex cuts to the optimization problem via disjunctive programming. We analyze the performance of this sequential SDP method both theoretically and empirically, and show that it bridges the gap as the number of cuts increases.