Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Algebraic Robustness Verification of Neural Networks

Yulia Alexandr, Hao Duan, Guido Montúfar

TL;DR

The paper reframes robustness verification for neural networks as an algebraic distance-minimization problem onto the classifier's decision boundary and introduces the Euclidean Distance degree ($\mathrm{EDdegree}$) as an architecture-aware measure of verification complexity. It develops discriminants (the ED discriminant and the parameter discriminant) to classify test inputs and network parameters by problem hardness, and derives closed-form ED-degree formulas for shallow and certain deep architectures, along with expected real-ED-degree results (via Kac–Rice and NNGP frameworks). The authors also provide a practical, exact robustness certification pipeline based on numerical homotopy continuation, with an accompanying symbolic algorithm to compute discriminants and a publicly available implementation. This framework connects metric algebraic geometry with verification, enabling complexity-aware model design and principled certification beyond traditional relaxations. The approach has potential to guide architecture selection and regularization to reduce verification burden while offering provable guarantees through exact algebraic certificates.

Abstract

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.

Algebraic Robustness Verification of Neural Networks

TL;DR

The paper reframes robustness verification for neural networks as an algebraic distance-minimization problem onto the classifier's decision boundary and introduces the Euclidean Distance degree () as an architecture-aware measure of verification complexity. It develops discriminants (the ED discriminant and the parameter discriminant) to classify test inputs and network parameters by problem hardness, and derives closed-form ED-degree formulas for shallow and certain deep architectures, along with expected real-ED-degree results (via Kac–Rice and NNGP frameworks). The authors also provide a practical, exact robustness certification pipeline based on numerical homotopy continuation, with an accompanying symbolic algorithm to compute discriminants and a publicly available implementation. This framework connects metric algebraic geometry with verification, enabling complexity-aware model design and principled certification beyond traditional relaxations. The approach has potential to guide architecture selection and regularization to reduce verification burden while offering provable guarantees through exact algebraic certificates.

Abstract

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.
Paper Structure (41 sections, 23 theorems, 152 equations, 5 figures, 2 tables, 2 algorithms)

This paper contains 41 sections, 23 theorems, 152 equations, 5 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related Works
  4. Neural network verification
  5. Distance-based robustness
  6. Algebraic perspectives on neural networks
  7. Verification as an Algebraic Problem
  8. Notation
  9. Robustness Verification via Metric Projection
  10. Geometric interpretation
  11. Algebraic Optimization Formulation
  12. KKT conditions
  13. Relaxation of inequality constraints
  14. ED Degree of a Decision Boundary
  15. ED Degree for Generic Parameters
  16. ...and 26 more sections

Key Result

Proposition 2.0

Let $f_{\boldsymbol{\theta}}: \mathbb{R}^{n}\to \mathbb{R}^{k}$ be a continuous classifier, and let $\hat{c}(\boldsymbol{x}) := \arg\max_{i \in [k]}f_{\boldsymbol{\theta}, i}(\boldsymbol{x})$ denote the predicted class. Fix a test point $\boldsymbol{\xi} \in \mathbb{R}^{n}$ and write $c := \hat{c}(\ Then, for $\gamma$ and $\tilde{\gamma}$ defined in (eq:robustness-margin) and (eq:robustness-margin

Figures (5)

  • Figure 1: The blue hypersurface shows the decision boundary of a polynomial neural network. The black dot is a test input; we compute its projection onto this decision boundary to obtain the robustness margin.
  • Figure 2: Left: An iteration of homotopy continuation, moving from $x_{t}$ to $x_{t+\Delta t}$ via a tangent predictor (orange) and a Newton corrector (blue). Right: Homotopy paths tracking the roots of $x^{3}- 4 x^{2}+ 8x - 8 = 0$ (with $x_{1,2}= 1 \pm \sqrt{3}\, i$ and $x_{3}= 2$) from the start system $x^{3}- 1 = 0$ (with $x_{1,2}= -\frac{1}{2}\pm \frac{\sqrt{3}}{2}\, i$ and $x _{3}= 1$).
  • Figure 3: Left: The decision boundary is shown in blue and the corresponding ED discriminant curve is shown in orange. Right: The number of distinct real critical points of the distance minimization problem on different regions of the data space separated by the discriminant. The shaded region is where $D(u_{1},u_{2})>0$.
  • Figure 4: Schematic illustration of a 2D slice of the conic parameter space. Generic regions (ellipses/hyperbolas) have ED degree 4. The discriminant locus appears as a blue curve for parabolas and a red curve for singular conics, but as a green point for circles.
  • Figure 5: Number of real zeros vs. activation degree. Light points show individual simulations; solid and dashed lines denote empirical and theoretical means ($n=1,000$ samples, $m=20,000$ hidden units).

Theorems & Definitions (48)

  • Proposition 2.0
  • Definition 3.1: Euclidean Distance Degree
  • Proposition 3.1
  • Corollary 3.2
  • Example 3.3
  • Remark 3.4: Deep architectures
  • Proposition 3.4
  • Example 3.5
  • Proposition 3.5
  • Remark 3.6
  • ...and 38 more