Algebraic Robustness Verification of Neural Networks
This work provides a new theoretical framework for understanding the complexity of robustness verification for neural networks, which could benefit researchers working on formal verification methods.
This paper formulates neural network robustness verification as an algebraic optimization problem, introducing the Euclidean Distance (ED) degree as a measure of intrinsic verification complexity. It provides an algorithm to compute the ED discriminant, which distinguishes easier from harder test instances, and derives closed-form expressions for the ED degree for various architectures.
We formulate formal robustness verification of neural networks as an algebraic optimization problem. We leverage the Euclidean Distance (ED) degree, which is the generic number of complex critical points of the distance minimization problem to a classifier's decision boundary, as an architecture-dependent measure of the intrinsic complexity of robustness verification. To make this notion operational, we define the associated ED discriminant, which characterizes input points at which the number of real critical points changes, distinguishing test instances that are easier or harder to verify. We provide an explicit algorithm for computing this discriminant. We further introduce the parameter discriminant of a neural network, identifying parameters where the ED degree drops and the decision boundary exhibits reduced algebraic complexity. We derive closed-form expressions for the ED degree for several classes of neural architectures, as well as formulas for the expected number of real critical points in the infinite-width limit. Finally, we present an exact robustness certification algorithm based on numerical homotopy continuation, establishing a concrete link between metric algebraic geometry and neural network verification.