Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisation

Ben Batten, Yang Zheng, Alessandro De Palma, Panagiotis Kouvaros, Alessio Lomuscio

TL;DR

This work addresses the challenge of formally verifying neural networks against geometric input transformations by introducing a provably sound piecewise linear relaxation of the transformation mapping. The method builds tight convex relaxations for pixel values under rotation, translation, scaling, and shear through sampling, linear bounds, and a Lipschitz-based branch-and-bound procedure, enabling integration with existing verifiers. Empirically, the piecewise linear approach yields tighter bounds, higher certification rates, and competitive runtime on MNIST and CIFAR-10 networks compared to state-of-the-art linear relaxations and prior geometric robustness methods. The results demonstrate practical gains in robust verification without requiring transformation splitting, and the work contributes a scalable framework for exact, geometry-aware neural network verification with open-source code.

Abstract

We address the problem of verifying neural networks against geometric transformations of the input image, including rotation, scaling, shearing, and translation. The proposed method computes provably sound piecewise linear constraints for the pixel values by using sampling and linear approximations in combination with branch-and-bound Lipschitz optimisation. The method obtains provably tighter over-approximations of the perturbation region than the present state-of-the-art. We report results from experiments on a comprehensive set of verification benchmarks on MNIST and CIFAR10. We show that our proposed implementation resolves up to 32% more verification cases than present approaches.

Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisation

TL;DR

This work addresses the challenge of formally verifying neural networks against geometric input transformations by introducing a provably sound piecewise linear relaxation of the transformation mapping. The method builds tight convex relaxations for pixel values under rotation, translation, scaling, and shear through sampling, linear bounds, and a Lipschitz-based branch-and-bound procedure, enabling integration with existing verifiers. Empirically, the piecewise linear approach yields tighter bounds, higher certification rates, and competitive runtime on MNIST and CIFAR-10 networks compared to state-of-the-art linear relaxations and prior geometric robustness methods. The results demonstrate practical gains in robust verification without requiring transformation splitting, and the work contributes a scalable framework for exact, geometry-aware neural network verification with open-source code.

Abstract

We address the problem of verifying neural networks against geometric transformations of the input image, including rotation, scaling, shearing, and translation. The proposed method computes provably sound piecewise linear constraints for the pixel values by using sampling and linear approximations in combination with branch-and-bound Lipschitz optimisation. The method obtains provably tighter over-approximations of the perturbation region than the present state-of-the-art. We report results from experiments on a comprehensive set of verification benchmarks on MNIST and CIFAR10. We show that our proposed implementation resolves up to 32% more verification cases than present approaches.
Paper Structure (23 sections, 3 theorems, 24 equations, 2 figures, 2 tables, 1 algorithm)

This paper contains 23 sections, 3 theorems, 24 equations, 2 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Related Work
  2. $\ell_p$ robustness verification.
  3. Geometric robustness.
  4. Formal verification of geometric robustness.
  5. Geometric robustness verification
  6. Notation.
  7. Neural networks for classification.
  8. Robustness verification.
  9. Attack model via geometric transformation.
  10. Problem statement.
  11. Piecewise linear formulation
  12. Piecewise linear bounds
  13. Linear optimisation based on sampling points
  14. Lipschitz optimisation for obtaining sound piecewise linear bounds
  15. Experimental Evaluation
  16. ...and 8 more sections

Key Result

Proposition 1

Given any subdomains $\mathcal{B}_j$, $j = 1, \ldots, q$, the optimal solutions $\underline{w}_j, \underline{b}_j$, $j = 1, \ldots, q$, to eq:bound_sample_optimisation_individual are suboptimal to eq:bound_sample_optimisation, i.e., $\sum_{j=1}^q \beta^*_j \geq \beta^*$. There exists a set of subdo

Figures (2)

  • Figure 1: Comparison of sound and unsound piecewise (PW) linear domains (our work), sound linear domain (gray area) singh2019abstract, and interval bounds (dashed line) singh2019abstract. The true pixel value function (the green curve) is marked for a rotation of 18$^{\circ}$.
  • Figure 2: A comparison of area captured by piecewise linear and linear bounds as a function of transformation parameter. Relative bound area is defined as $1 - (V_{\text{PWL}} / V_\text{L})$.

Theorems & Definitions (7)

  • Proposition 1
  • proof
  • Remark 1
  • Proposition 2
  • proof
  • Proposition 3
  • proof