Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming

Certifying the safety or robustness of neural networks against input\nuncertainties and adversarial attacks is an emerging challenge in the area of\nsafe machine learning and control. To provide such a guarantee, one must be\nable to bound the output of neural networks when their input changes within a\nbounded set. In this paper, we propose a semidefinite programming (SDP)\nframework to address this problem for feed-forward neural networks with general\nactivation functions and input uncertainty sets. Our main idea is to abstract\nvarious properties of activation functions (e.g., monotonicity, bounded slope,\nbounded values, and repetition across layers) with the formalism of quadratic\nconstraints. We then analyze the safety properties of the abstracted network\nvia the S-procedure and semidefinite programming. Our framework spans the\ntrade-off between conservatism and computational efficiency and applies to\nproblems beyond safety verification. We evaluate the performance of our\napproach via numerical problem instances of various sizes.\n