Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming

Convex relaxations have emerged as a promising approach for verifying\ndesirable properties of neural networks like robustness to adversarial\nperturbations. Widely used Linear Programming (LP) relaxations only work well\nwhen networks are trained to facilitate verification. This precludes\napplications that involve verification-agnostic networks, i.e., networks not\nspecially trained for verification. On the other hand, semidefinite programming\n(SDP) relaxations have successfully be applied to verification-agnostic\nnetworks, but do not currently scale beyond small networks due to poor time and\nspace asymptotics. In this work, we propose a first-order dual SDP algorithm\nthat (1) requires memory only linear in the total number of network\nactivations, (2) only requires a fixed number of forward/backward passes\nthrough the network per iteration. By exploiting iterative eigenvector methods,\nwe express all solver operations in terms of forward and backward passes\nthrough the network, enabling efficient use of hardware like GPUs/TPUs. For two\nverification-agnostic networks on MNIST and CIFAR-10, we significantly improve\nL-inf verified robust accuracy from 1% to 88% and 6% to 40% respectively. We\nalso demonstrate tight verification of a quadratic stability specification for\nthe decoder of a variational autoencoder.\n