Quadratic Characterizations for Reachability Analysis of Neural Networks

TL;DR

This paper introduces a framework for verified quadratic characterizations of scalar relations, enhancing reachability analysis of neural networks by reducing conservatism and improving accuracy over existing methods.

Contribution

It develops a method to generate and verify quadratic inequalities for scalar relations, applicable to neural network analysis and other nonlinear systems, using convex quadratic programming and sum-of-squares certificates.

Findings

Improved reachability results for smooth activations like tanh.

Reduced conservatism in QC-based analysis of ReLU networks.

Applicable to systems beyond neural networks, such as saturation examples.

Abstract

Quadratic constraints (QCs) are widely used to characterize nonlinearities and uncertainties, but generic analytical characterizations can be conservative on bounded domains. This paper develops a framework for constructing verified quadratic characterizations of scalar relations in the two-dimensional real plane. Candidate quadratic inequalities are locally generated by solving convex quadratic programs using samples from the relation and exterior sample points. They are then verified globally using sum-of-squares certificates over an exact semialgebraic description or, in the case of nonpolynomial relations, over relaxed polynomial descriptions. The resulting verified constraints define a sound overapproximation of the scalar relations over the considered domains. These constraints are directly compatible with existing analysis frameworks based on QCs and pointwise integral quadratic constraints (IQCs) for static nonlinearities and uncertainties, and they can also be embedded in QC-based semidefinite programs for reachability and safety analysis of feedforward neural networks. For smooth activations such as $\tanh$, the method yields domain-dependent quadratic characterizations that constitute an alternative to generic sector- or slope-based descriptions. For ReLU networks, we give methods to reduce conservatism in QC-based reachability analysis of feedforward networks by exploiting dependencies between neurons and tighter local bounds. Numerical examples demonstrate improved reachability results for smooth activations, reduced conservatism for ReLU networks, and applicability beyond neural networks through an example involving saturation.