ForwardAlgorithms

ForwardAlgorithm

Abstract supertype of forward algorithms.

DefaultForward <: ForwardAlgorithm

Default forward algorithm, which works for vector-like inputs.

ConcreteForward <: ForwardAlgorithm

Forward algorithm that uses concrete set operations.

LazyForward <: ForwardAlgorithm

Forward algorithm that uses lazy set operations.

BoxForward{AMA<:ForwardAlgorithm} <: ForwardAlgorithm

Forward algorithm that uses a box approximation for non-identity activations and applies the affine map according to the specified algorithm.

Fields

• affine_map_algorithm – algorithm to apply for affine maps

SplitForward{S<:ForwardAlgorithm,FS,FM} <: ForwardAlgorithm

Forward algorithm that splits a set, then computes the image under the neural network, and finally merges the resulting sets again, all according to a policy.

Fields

• algo – algorithm to be applied between splitting and merging
• split_function – function for splitting
• merge_function – function for merging

DeepZ <: ForwardAlgorithm

Forward algorithm based on zonotopes for ReLU, sigmoid, and tanh activation functions from [1].

[1]: Singh et al.: Fast and Effective Robustness Certification, NeurIPS 2018.

AI2Box <: AI2

AI2 forward algorithm for ReLU activation functions based on abstract interpretation with the interval domain from [1].

Notes

This algorithm is less precise than BoxForward because it abstracts after every step, including the affine map.

[1]: Gehr et al.: AI²: Safety and robustness certification of neural networks with abstract interpretation, SP 2018.

AI2Zonotope <: AI2

AI2 forward algorithm for ReLU activation functions based on abstract interpretation with the zonotope domain from [1].

Fields

• join_algorithm – (optional; default: "join") algorithm to compute the join of two zonotopes

[1]: Gehr et al.: AI²: Safety and robustness certification of neural networks with abstract interpretation, SP 2018.

AI2Polytope <: AI2

AI2 forward algorithm for ReLU activation functions based on abstract interpretation with the polytope domain from [1].

[1]: Gehr et al.: AI²: Safety and robustness certification of neural networks with abstract interpretation, SP 2018.

PolyZonoForward{A<:PolynomialApproximation,N,R} <: ForwardAlgorithm

Forward algorithm based on poynomial zonotopes via polynomial approximation from [1].

Fields

• polynomial_approximation – method for polynomial approximation
• reduced_order – order to which the result will be reduced after each layer
• compact – predicate for compacting the result after each layer

Notes

The default constructor takes keyword arguments with the following defaults:

• polynomial_approximation: RegressionQuadratic(10), i.e., quadratic regression with 10 samples
• compact: () -> true, i.e., compact after each layer

See the subtypes of PolynomialApproximation for available polynomial approximation methods.

[1]: Kochdumper et al.: Open- and closed-loop neural network verification using polynomial zonotopes, NFM 2023.

Verisig{R} <: ForwardAlgorithm

Forward algorithm for sigmoid and tanh activation functions from [1].

Fields

• algo – reachability algorithm of type TMJets

Notes

The implementation is known to be unsound in some cases.

The implementation currently only supports neural networks with a single hidden layer.

[1] Ivanov et al.: Verisig: verifying safety properties of hybrid systems with neural network controllers, HSCC 2019.