A Sequential Framework Towards an Exact SDP Verification of Neural Networks

TL;DR

This paper introduces a sequential SDP framework that reduces the relaxation gap in neural network robustness certification by iteratively adding non-convex cuts, enhancing the accuracy of convex optimization methods.

Contribution

It proposes a novel sequential approach with non-convex cuts to achieve exact SDP verification of neural networks, addressing the relaxation gap issue.

Findings

The sequential SDP method effectively shrinks the relaxation gap as more cuts are added.

The approach bridges the gap both theoretically and empirically.

It improves the robustness certification accuracy for neural networks.

Abstract

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.