Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming
Certifying the safety or robustness of neural networks against input uncertainties and adversarial attacks is an emerging challenge in the area of safe machine learning and control. To provide such a guarantee, one must be able to bound the output of neural networks when their input changes within a bounded set. In this paper, we propose a semidefinite programming (SDP) framework to address this problem for feed-forward neural networks with general activation functions and input uncertainty sets. Our main idea is to abstract various properties of activation functions (e.g., monotonicity, bounded slope, bounded values, and repetition across layers) with the formalism of quadratic constraints. We then analyze the safety properties of the abstracted network via the S-procedure and semidefinite programming. Our framework spans the trade-off between conservatism and computational efficiency and applies to problems beyond safety verification. We evaluate the performance of our approach via numerical problem instances of various sizes.
Code (4)
Tasks
Computational EfficiencySimilar Papers 제목 키워드 기반
Probabilistic Verification and Reachability Analysis of Neural Networks via Semidefinite Programming
Quantifying the robustness of neural networks or verifying their safety properties against input uncertainties or adversarial attacks have become an important research area in learning-enabled systems. Most results conce…
Explicit Solution of Tunable Input-to-State Safe-Based Controller Under High-Relative-Degree Constraints
This paper investigates the safety analysis and verification of nonlinear systems subject to high-relative-degree constraints and unknown disturbance. The closed-form solution of the high-order control barrier functions …
Distributionally Robust Safety Verification of Neural Networks via Worst-Case CVaR
Ensuring the safety of neural networks under input uncertainty is a fundamental challenge in safety-critical applications. This paper builds on and expands Fazlyab's quadratic-constraint (QC) and semidefinite-programming…
RNN Controller for Lane-Keeping Systems with Robustness and Safety Verification
This paper proposes a Recurrent Neural Network (RNN) controller for lane-keeping systems, effectively handling model uncertainties and disturbances. First, quadratic constraints cover the nonlinearities brought by the RN…
Validation of Neural Network Controllers for Uncertain Systems Through Keep-Close Approach: Robustness Analysis and Safety Verification
Among the major challenges in neural control system technology is the validation and certification of the safety and robustness of neural network (NN) controllers against various uncertainties including unmodelled dynami…