Source-linked AI summary
Maximum Resilience of Artificial Neural Networks
Chih-Hong Cheng, Georg Nührenberg, Harald Ruess
TL;DR
The paper addresses how to verify ANN resilience to noisy or malicious input in safety-critical applications. It defines maximal tolerated perturbation bounds and computes them through mixed-integer optimization with encoding heuristics and parallelization. The approach is demonstrated on image-recognition and autonomous-robot benchmarks, with substantial solver speed-ups and scalable verification.
Problem
Safety-critical ANN applications require verified properties describing how much noisy or malicious sensory input the networks tolerate.
Method
The paper defines resilience over all inputs using softmax-based perturbation bounds and reduces their computation to MIP, with specialized encodings and parallel branch-and-bound.
Results
The approach computes maximum perturbation bounds across image-recognition and autonomous-control benchmarks and demonstrates effectiveness and scalability.
Takeaways & Limitations
Perturbation bounds provide a formal sensor-to-classifier assume-guarantee interface and enable quantitative comparison of ANN resilience.
Takeaways & Limitations
For tan^-1 activations, approximation error propagates through the network, so the method computes an approximation of the resilience measure.
Abstract
from arXiv · showhide
The deployment of Artificial Neural Networks (ANNs) in safety-critical applications poses a number of new verification and certification challenges. In particular, for ANN-enabled self-driving vehicles it is important to establish properties about the resilience of ANNs to noisy or even maliciously manipulated sensory input. We are addressing these challenges by defining resilience properties of ANN-based classifiers as the maximal amount of input or sensor perturbation which is still tolerated. This problem of computing maximal perturbation bounds for ANNs is then reduced to solving mixed integer optimization problems (MIP). A number of MIP encoding heuristics are developed for drastically reducing MIP-solver runtimes, and using parallelization of MIP-solvers results in an almost linear speed-up in the number (up to a certain limit) of computing cores in our experiments. We demonstrate the effectiveness and scalability of our approach by means of computing maximal resilience bounds for a number of ANN benchmark sets ranging from typical image recognition scenarios to the autonomous maneuvering of robots.
1 Introduction
The paper targets verified resilience bounds for ANNs exposed to noisy or malicious sensory inputs in safety-critical applications. It formulates perturbation-bound computation as MIP solving and develops heuristics and parallelization to improve scalability.
- Motivation: Safety-critical ANN deployment creates verification and certification challenges, including determining tolerated noisy or malicious sensory input.The motivation includes medical image processing and semi-autonomous vehicles.
- Motivation: The approach defines maximum and verified resilience bounds for ANN classifiers under input disturbances.These bounds quantify the maximum tolerated perturbation for the network.
- Approach: Computing minimal perturbation bounds is reduced to mixed-integer programming, with integer variables required for nonlinear nodes such as ReLU and max-pooling.The formulation targets multi-class classifiers and uses softmax output ratio ordering.
- Approach: Encoding heuristics use dataflow analysis for smaller big-M values and simpler intermediate MIP problems, while parallel branch-and-bound improves solver performance.The heuristics are designed to speed up generation of satisfying solver instances.
- Results: About two orders of magnitude speed-up over vanilla MIP encodings was observed on MNIST and agent-game benchmarks, with near-linear parallel speed-ups up to a threshold.The benchmarks cover image recognition and autonomous robot maneuver decisions.
- Implications: Perturbation bounds provide a formal assume-guarantee interface for sensor errors and support comparing ANN resilience and generating minimally perturbed inputs.The paper also relates large perturbation bounds inversely to overfitting.
2 Preliminaries
Feed-forward ANNs are layered networks whose nodes transform inputs successively toward an output layer. The preliminaries describe fixed weighted connections, common node functions, and softmax outputs interpreted as class probabilities.
- Network structure: A feed-forward ANN contains input, hidden, and output layers, with layers indexed from l = 0 to L and bounded-domain inputs.Layer 0 is the input layer and layer L is the output layer.
- Network structure: Layers contain neurons connected by directed weighted edges, while index-0 bias nodes provide constant output 1 for activation thresholds.Network weights are fixed because the paper does not consider re-learning.
- Node computation: ReLU nodes output the maximum of 0 and a weighted linear sum, whereas max-pooling nodes output the maximum of their inputs for down-sampling.The illustrated network uses a fully connected ReLU hidden layer followed by max-pooling.
- Node computation: Node functions are applied successively from layer 0 through layer L − 1 to compute the network output.The notation x^(l)_i denotes node output values at layer l.
- Output interpretation: Softmax transforms output-layer values into a probability distribution whose entries represent class probabilities and sum to 1.The example distribution is (0.0132, 0.2654, 0.7214).
3 Arithmetic Encoding of Artificial Neural Networks
The paper encodes ANN behavior as arithmetic constraints for MIP solving, including nonlinear activations, max-pooling, and softmax-related properties. Dataflow-derived bounds tighten these encodings, while tan^-1 approximations introduce a stated approximation scope.
- Neuron and network encodings: ANN node behavior is encoded with linear arithmetic constraints, including ReLU, tan^-1, max-pooling, and softmax nodes.The nonlinearities and pooling operations require specialized encodings within the MIP formulation.
- Neuron and network encodings: ReLU and max-pooling nonlinearities are represented using big-M constraints and binary variables.Max-pooling over two inputs uses three binary integer variables, while ReLU encoding introduces a binary variable and a positive M constant.
- Dataflow-based preprocessing: Interval arithmetic propagates bounded input values through the network to generate relatively small big-M constants and strengthen the MIP relaxation.When interval bounds determine a ReLU branch, the formulation can drop case constraints and reduce binary variables.
- Property-directed softmax encoding: Softmax output layers are handled property-directly by replacing probability comparisons with ratio-ordering constraints rather than encoding exponentials.The approach can omit explicit softmax output construction when only output-neuron ratio ordering matters.
- Nonlinear approximation: tan^-1 nodes use piecewise quadratic approximations with error bounds, requiring mixed-integer quadratic constraint solving and yielding approximate resilience measures.Approximation errors propagate through the network, and interval bounds relax the problem rather than enforcing exact tan^-1 equalities.
4 Perturbation Bounds
The paper defines maximum perturbation bounds for multi-class ANN classifiers and computes them by reducing the search for confidence-degrading perturbations to mixed-integer optimization. The bound captures the smallest total input disturbance that can move a strongly classified input out of the top-k classes, with exactness for ReLU networks and under-approximation for tan^-1 networks.
- Resilience measure: Maximum resilience is defined over all inputs for multi-class ANN classifiers with softmax outputs, without relying on training or test-data distributions.The ANN-level bound is Ξ := min(Φ1, ..., Φd(L)) across classifier-specific bounds.
- Resilience measure: For class m, Φm is the smallest total input perturbation that can make at least k other classes at least as likely as m after perturbation.The perturbation magnitude is the sum of absolute component disturbances, |ϵ1| + ... + |ϵd|.
- Resilience measure: The confidence condition uses α to select inputs strongly classified as m and k to determine when m is no longer among the k highest-probability classes.The experiments use k = 2; increasing k can avoid zero bounds caused by equal class probabilities when α = 1.
- MIP formulation: The optimization minimizes absolute perturbations while enforcing the original-class condition and a post-perturbation violation in which at least k alternatives match or exceed class m.Absolute-value variables linearize the objective, binary variables encode the disjunction, and big-M constraints enforce selected class comparisons.
- MIP formulation: Softmax output layers are omitted from the MIP because ratio ordering can be checked using preceding-layer values instead of the exponential function.This property-directed encoding applies when the analyzed property depends on output ordering rather than concrete softmax probabilities.
- Correctness: For ReLU ANNs, the MIP optimum equals Φm, whereas for tan^-1 networks it provides an under-approximation because of the activation-function approximation.The transformed problem is therefore exact for ReLU networks under the stated α and k conditions.
5 Heuristic Problem Encodings
The paper develops solver heuristics for reducing the cost of MIP-based ANN verification. These include tighter bounds, structure-aware branching, simpler subproblems, and solver initialization.
- MIP-solving heuristics are presented as broadly applicable to ANN verification beyond resilience computation.
- Smaller big-Ms by looking back at multiple layers: A finer-grained dataflow analysis considers multiple predecessor layers to derive smaller big-M values.Independent node-level subproblems can be solved in parallel.
- Branching priorities: Branching priorities favor binary variables from lower ANN layers because they influence variables in deeper layers.
- Constraint generation from samples and solver initialization: Constraint generation first finds a high-confidence input assignment using a simpler MIP without perturbation variables.The subsequent single-input problem computes an initial minimum perturbation bound.
- Constraint generation from samples and solver initialization: The computed initial values are used to initialize the solver with a feasible solution and restrict its search space.
6 Implementation and Evaluation
The evaluation measures MIP verification efficiency and maximum resilience across image-recognition, agent-game, and traffic-control benchmarks. Heuristics and parallelization improve difficult instances, while resilience depends on the confidence parameter α.
- The evaluation uses IMNIST, IAgent, and Ideeptraffic benchmarks spanning digit recognition, agent games, and highway overtaking decisions.The experiments use neural networks with varying hidden-layer sizes.
- Table 1 reports execution times for single-input perturbation verification with a one-hour timeout; agent-game instances require no heuristics.
- The experiments focus on MIP-encoding efficiency, parallelization, and computing perturbation bounds through the stated optimization problem.
- Evaluation of MIP Encodings: More difficult MNIST instances could only be solved using the first preprocessing heuristic, while dataflow analysis benefits longer-running instances.The heuristics can also lengthen solution times for simpler instances.
- Effects of Parallelization: 32 cores improve execution time for IMNIST local-robustness instances, whereas increasing from 32 to 64 threads does not improve this particular 200-neuron case.Other, more complex problems may continue benefiting from additional threads.
- Computing Φm: For simpler problems, computed maximum resilience Φm increases with α; values above the maximum feasible α make the problem infeasible.Higher-confidence inputs allow more perturbation before ambiguity, while high α can shrink the input space for complex problems.
7 Concluding Remarks
The paper presents MIP-based maximum perturbation bounds and heuristics as a scalable basis for ANN verification. It also frames these bounds as assume-guarantee interfaces while acknowledging important scope limitations.
- MIP-based optimization provides a novel way to define and compute maximum perturbation bounds for ANNs.
- Specialized encodings and parallelization demonstrate scalability and possible applicability to neural-network verification in real-world applications.
- Perturbation bounds formally connect sensor error assumptions with classifier resilience, supporting decoupled sensor and network design.The paper suggests these contract-based interfaces may support more modular safety cases.
- The work is characterized as an early step toward the broader potential of formal ANN verification in safety-critical systems.
Appendix
The appendix establishes formal relationships used in the ANN-to-MIP encoding. Its proof steps reason through binary activation cases and verify that the resulting constraints represent the intended conditions.
- The appendix argues that sufficiently large big-M values make the constraints hold in the relevant activation cases.
- A lemma is established before the proposition’s proof to support the subsequent derivation.
- The proof handles binary integer variables by considering both possible cases and checking the associated constraints.
- The appendix introduces a proposition for feed-forward ANNs with softmax output layers and a positive confidence parameter α.