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 Singh et al. [SGM+18].

AI2Box <: AI2

AI2 forward algorithm for ReLU activation functions based on abstract interpretation with the interval domain from Gehr et al. [GMD+18].

Notes

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

AI2Zonotope <: AI2

AI2 forward algorithm for ReLU activation functions based on abstract interpretation with the zonotope domain from Gehr et al. [GMD+18].

Fields

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

AI2Polytope <: AI2

AI2 forward algorithm for ReLU activation functions based on abstract interpretation with the polytope domain from Gehr et al. [GMD+18].

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

Forward algorithm based on poynomial zonotopes via polynomial approximation from Kochdumper et al. [KSAB23].

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.

Verisig{R} <: ForwardAlgorithm

Forward algorithm for sigmoid and tanh activation functions from Ivanov et al. [IWA+19].

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.