Propagation

propagate(prop_method::PropMethod, model_info, batch_info)

Propagates through the model using the specified prop_method. The propagation algorithm is as follows:

1. Add the connecting nodes of the start nodes, i.e., nodes after the start

nodes, into a queue.

1. While the queue is not empty:
   1. Pop a node from the queue.
   2. For each node connected from the current node, i.e., for each output node:
      1. Increment the visit count to the output node.
      2. If the visit count equals the number of nodes connected from the output node, i.e., visit count == previous nodes of the output node, add the output node to the queue.
   3. Propagate through the current node accordingly.
   4. Add information about the bound of the node to batch_info.
2. Return the bound of the output node(s).

In step 2(1)(2), the function adds the output node to the queue since all the previous nodes of the output node have been processed. Thus, the output node is now the node of interest. In step 2(3), the propagation works based on the propagation method (prop_method), which depends on the geometric representation of the safety specifications and the activation function of each layer.

Arguments

• prop_method (PropMethod): Propagation method used for the verification process. This is one of the solvers used to verify the given model.
• model_info: Structure containing the information of the neural network to be verified.
• batch_info: Dictionary containing information of each node in the model.

Returns

• batch_bound: Bound of the output node, i.e., the final bound.
• batch_info: Same as the input batch_info, with additional information on the bound of each node in the model.

propagate(prop_method::ODEProp, model_info, batch_info)

Propagates reachable set with a ODE integrator.

Arguments

• prop_method (ODEProp): ODE integration method used for the verification process.
• model_info: The neural ODE flux model. It is different from model_info in propagate() of other, which is a Model structure containing the general computational graph.
• batch_info: Dictionary containing information of each node in the model.

Returns

• batch_bound: Bound of the output node, i.e., the final bound.
• batch_info: Same as the input batch_info, with additional information on the bound of each node in the model.

propagate_skip_method(prop_method::ForwardProp, model_info, 
                      batch_info, node)

This function propagates the two sets of bounds of the preceding nodes from the provided node using the specified forward propagation method and layer operation. It invokes propagate_skip_batch, which subsequently calls propagate_skip. The function identifies the two previous nodes from the given node in the computational graph, model_info, their bounds, and the layer operation of the node. Then, propagate_skip is invoked.

Arguments

• prop_method (ForwardProp): Forward propagation method used for the verification process. This is one of the solvers used to verify the given model.
• model_info: Structure containing the information of the neural network to be verified.
• batch_info: Dictionary containing information of each node in the model.
• node: The current node to be propagated through.

Returns

• batch_bound: List of reachable bounds after propagating the two sets of bounds in batch_reach through the given node, following the propagation method and the layer operation.

propagate_skip_method(prop_method::BackwardProp, model_info, 
                      batch_info, node)

This function propagates the two sets of bounds of the next nodes from the provided node using the specified backward propagation method and layer operation. It invokes propagate_skip_batch, which subsequently calls propagate_skip. The function identifies the two next nodes from the given node in the computational graph, model_info, their bounds, and the layer operation of the node. Then, propagate_skip is invoked.

Arguments

• prop_method (BackwardProp): Backward propagation method used for the verification process. This is one of the solvers used to verify the given model.
• model_info: Structure containing the information of the neural network to be verified.
• batch_info: Dictionary containing information of each node in the model.
• node: The current node to be propagated through.

Returns

• batch_bound: List of reachable bounds after propagating the two sets of bounds in batch_reach through the given node, following the propagation method and the layer operation.

propagate_layer_method(prop_method::ForwardProp, model_info, batch_info, node)

This function propagates the bounds of the preceding node from the provided node using the specified forward propagation method and layer operation. It invokes propagate_layer_batch, which subsequently calls either propagate_layer_batch or propagate_layer_batch. The function identifies the previous node from the given node in the computational graph, model_info, its bound, and the layer operation of the node. Then, propagate_layer_batch ascertains if the layer operation is linear or includes activation functions like ReLU. Depending on this, propagate_layer_batch or propagate_layer_batch is invoked.

Arguments

• prop_method (ForwardProp): The forward propagation method employed for verification. It is one of the solvers used to validate the specified model.
• model_info: Structure containing the information of the neural network to be verified.
• batch_info: Dictionary containing information of each node in the model.
• node: The current node to be propagated through.

Returns

• batch_bound: List of reachable bounds after propagating the set of input bounds of the given node, following the propagation method and the linear layer operation.

propagate_layer_method(prop_method::BackwardProp, model_info, batch_info, node)

This function propagates the bounds of the next node from the provided node using the specified forward propagation method and layer operation. It invokes propagate_layer_batch, which subsequently calls either propagate_layer_batch or propagate_layer_batch. The function identifies the next node from the given node in the computational graph, model_info, its bound, and the layer operation of the node. Then, propagate_layer_batch ascertains if the layer operation is linear or includes activation functions like ReLU. Depending on this, propagate_layer_batch or propagate_layer_batch is invoked.

Arguments

• prop_method (BackwardProp): Backward propagation method used for the verification process. This is one of the solvers used to verify the given model.
• model_info: Structure containing the information of the neural network to be verified.
• batch_info: Dictionary containing information of each node in the model.
• node: The current node to be propagated through.

Returns

• batch_bound: List of reachable bounds after propagating the set of bounds in batch_reach through the given node, following the propagation method and the linear layer operation.
• nothing if the given node is a starting node of the model.

propagate_skip_batch(prop_method::ForwardProp, layer, 
                     batch_reach1::AbstractArray, 
                     batch_reach2::AbstractArray, 
                     batch_info)

Propagates each combination of the bounds from the batch_reach1 and batch_reach2 arrays with the given forward propagation method, prop_method, through a skip connection.

Arguments

• prop_method (ForwardProp): Forward propagation method used for the verification process. This is one of the solvers used to verify the given model.
• layer: Identifies what type of operation is done at the layer. Here's a bivariate operation is mainly used.
• batch_reach1 (AbstractArray): First list of input specifications, i.e., bounds, to be propagated through the given layer. This is the list of bounds given by the first of the two previous nodes.
• batch_reach2 (AbstractArray): Second list of input specifications, i.e., bounds, to be propagated through the given layer. This is the list of bounds given by the second of the two previous nodes.
• batch_info: Dictionary containing information of each node in the model.

Returns

• batch_reach_info: List of reachable bounds after propagating the bounds in batch_reach1 and batch_reach2 through the given layer, following the propagation method and the layer operation.

is_activation(l)

Returns true if the given layer l is an activation layer.

Arguments

• l: Layer.

Returns

• True if l is activation layer.
• False otherwise.

propagate_layer_batch(prop_method::ForwardProp, layer, 
                       batch_reach::AbstractArray, batch_info)

Propagates each of the bound in the batch_reach array with the given forward propagation method, prop_method, through a linear layer.

Arguments

• prop_method (ForwardProp): Forward propagation method used for the verification process. This is one of the solvers used to verify the given model.
• layer: Identifies what type of operation is done at the layer. Here, its a linear operation.
• batch_reach (AbstractArray): List of input specifications, i.e., bounds, to be propagated through the given layer.
• batch_info: Dictionary containing information of each node in the model.

Returns

• batch_reach_info: List of reachable bounds after propagating the set of bounds in batch_reach through the given layer, following the propagation method and the linear layer operation.

enqueue_connected!(prop_method::PropMethod, model_info, queue, visit_cnt, node)

Put all the connected node into the queue for propagation.

output_node(prop_method::ForwardProp, model_info)

Returns the final nodes of the model.

next_nodes(prop_method::ForwardProp,  model_info, node)

Returns the next nodes of the node for ForwardProp methods.

next_nodes(prop_method::BackwardProp, model_info, node)

Returns the previous nodes of the node for BackwardProp methods. Since this is for BackwardProp methods, the previous nodes are the "next" nodes.

prev_nodes(prop_method::ForwardProp,  model_info, node)

Returns the previous nodes of the node for ForwardProp methods.

prev_nodes(prop_method::BackwardProp, model_info, node)

Returns the next nodes of the node for BackwardProp methods. Since this is for BackwardProp methods, the next nodes are the "previous" nodes.

all_nexts_in(prop_method, model_info, output_node, cnt)

Returns true if all of the next nodes of the output_node have been visited.

all_prevs_in(prop_method, model_info, output_node, cnt)

Returns true if the output_node has been visited from all the previous nodes. This function checks if all possible connections to the output_node has been made in the propagation procedure. For example, given a node X, say that there are 5 different nodes that are mapped to X. Then, if the node X has been visited 5 times, i.e., cnt == 5, it means that all the previous nodes of X has been outputted to X.

propagate_skip(prop_method, layer::typeof(+), bound1::ImageStarBound, 
               bound2::ImageStarBound, batch_info)

Propagate the bounds of the two input layers to the output layer for skip connection. The output layer is of type ImageStarBound. The input layers' centers, generators, and constraints are concatenated to form the output layer's center, generators, and constraints.

Arguments

• prop_method (PropMethod): The propagation method used for the verification

problem.

• layer (typeof(+)): The layer operation to be used for propagation.
• bound1 (ImageStarBound): The bound of the first input layer.
• bound2 (ImageStarBound): The bound of the second input layer.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The bound of the output layer represented in ImageStarBound type.

propagate_skip(prop_method, layer::typeof(+), bound1::ImageZonoBound, 
               bound2::ImageZonoBound, batch_info)

Propagate the bounds of the two input layers to the output layer for skip connection. The output layer is of type ImageZonoBound. The input layers' centers and generators are concatenated to form the output layer's center and generators.

Arguments

• prop_method (PropMethod): The propagation method used for the verification problem.
• layer (typeof(+)): The layer operation to be used for propagation.
• bound1 (ImageZonoBound): The bound of the first input layer.
• bound2 (ImageZonoBound): The bound of the second input layer.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The bound of the output layer represented in ImageZonoBound type.

bound_layer(layer::Conv{2, 4, typeof(identity), 
                        Array{Float32, 4}, Vector{Float32}}, 
            lower_weight::AbstractArray, upper_weight::AbstractArray, 
            lower_bias::AbstractArray, upper_bias::AbstractArray)

Propagates the bounds of weight and bias through a convolutional layer. It applies the convolution operation with Conv to the weight and bias bounds: upper_weight, lower_weight, upper_bias, and lower_bias.

Arguments

• layer (Conv): The convolutional layer to be used for propagation.
• lower_weight (AbstractArray): The lower bound of the weight.
• upper_weight (AbstractArray): The upper bound of the weight.
• lower_bias (AbstractArray): The lower bound of the bias.
• upper_bias (AbstractArray): The upper bound of the bias.

Returns

• The bounds of the weight and bias after convolution operation represented in a tuple of [lowerweight, lowerbias, upperweight, upperbias].

bound_onside(layer::Conv{2, 4, typeof(identity), 
                        Array{Float32, 4}, Vector{Float32}}, 
             conv_input_size::AbstractArray, batch_reach::AbstractArray)

Transforms the batch reachable set to the input size of the convolutional layer using a ConvTranspose layer. First, it extracts the layer properties such as weight, bias, and stride. Then, it computes the output bias by summing over the batch reach and multiplying by the bias. Then, it flips the weights horizontally and vertically. Then, it computes the padding needed for the output based on the input size and the convolutional layer properties. Then, it creates a ConvTranspose layer with the calculated parameters and applies it to the batch reach. If additional padding is needed, it pads the output using the PaddedView function.

Arguments

• layer (Conv): The convolutional layer to be used for propagation.
• conv_input_size (AbstractArray): The size of the input to the convolutional layer.
• batch_reach (AbstractArray): The batch reachable set of the input to the convolutional layer.

Returns

• The batch reachable set and batch bias in dimension equal to the input size of the convolutional layer.

conv_bound_oneside(weight, bias, stride, pad, dilation, groups, size_before_conv,size_after_conv, batch_size)

convtrans_bound_oneside(weight, bias, stride, pad, dilation, groups, size_before_conv,size_after_conv, batch_size)

interval_propagate(layer::Conv{2, 4, typeof(identity), 
                               Array{Float32, 4}, Vector{Float32}}, 
                   interval, C = nothing)

Propagates the interval bounds through a convolutional layer. This is used in the interval arithmetic for neural network verification, where the goal is to compute the range of possible output values given a range of input values, represented with interval. It applies the convolution operation with Conv to the center of the interval and the deviation of the interval.

Arguments

• layer (Conv): The convolutional layer to be used for propagation.
• interval (Tuple): The interval bounds of the input to the convolutional layer.
• C (nothing): Optional argument for the center of the interval, default is nothing.

Returns

• The interval bounds after convolution operation represented in an array of [lower, upper, C = nothing].

propagate_by_small_batch(f, x; sm_batch=500)

Propagate the input x through f by small batches. This is useful when the input x is too large to fit into GPU memory.

Arguments

• f (function): Function to be applied to the input x.
• x (AbstractArray): Input to be propagated through f.
• sm_batch (Int): Optional argument for the size of the small batch, default is 500.

Returns

• Output of f applied to the input x.

propagate_layer(prop_method::ImageStar, layer::Conv, 
                 bound::ImageStarBound, batch_info)

Propagate the ImageStarBound bound through a convolution layer. I.e., it applies the convolution operation to the ImageStarBound bound. The convolution operation is applied to both the center and the generators of the ImageStarBound bound. Using the Flux.Conv, a convolutional layer is made in Flux with the given layer properties. While cen_Conv (convolutional layer for the center image) uses the bias, the gen_Conv (convolutional layer for the generators) does not. The resulting bound is also of type ImageStarBound.

Arguments

• prop_method (ImageStar): The ImageStar propagation method used for the verification problem.
• layer (Conv): The convolution operation to be used for propagation.
• bound (ImageStarBound): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The convolved bound of the output layer represented in ImageStarBound type.

propagate_layer(prop_method::ImageStar, layer::ConvTranspose, 
                 bound::ImageStarBound, batch_info)

Propagate the ImageStarBound bound through a convolutional transpose layer. I.e., it applies the convolutional transpose operation to the ImageStarBound bound. While a regular convolution reduces the spatial dimensions of an input, a convolutional transpose expands the spatial dimensions of an input. The convolutional transpose operation is applied to both the center and the generators of the ImageStarBound bound. Using the Flux.ConvTranspose, a convolutional tranpose layer is made in Flux with the given layer properties. While cen_Conv (convolutional transpose layer for the center image) uses the bias, the gen_Conv (convolutional transpose layer for the generators) does not. The resulting bound is also of type ImageStarBound.

Arguments

• prop_method (ImageStar): The ImageStar propagation method used for the verification problem.
• layer (ConvTranspose): The convolutional transpose operation to be used for propagation.
• bound (ImageStarBound): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The convolved bound of the output layer represented in ImageStarBound type.

propagate_layer(prop_method::ImageZono, layer::ConvTranspose, 
                 bound::ImageZonoBound, batch_info)

Propagate the ImageZonoBound bound through a convolutional transpose layer. I.e., it applies the convolutional transpose operation to the ImageZonoBound bound. While a regular convolution reduces the spatial dimensions of an input, a convolutional transpose expands the spatial dimensions of an input. The convolutional transpose operation is applied to both the center and the generators of the ImageZonoBound bound. Using the Flux.ConvTranspose, a convolutional tranpose layer is made in Flux with the given layer properties. While cen_Conv (convolutional transpose layer for the center image) uses the bias, the gen_Conv (convolutional transpose layer for the generators) does not. The resulting bound is also of type ImageZonoBound.

Arguments

• prop_method (ImageZono): The ImageZono propagation method used for the verification problem.
• layer (ConvTranspose): The convolutional transpose operation to be used for propagation.
• bound (ImageZonoBound): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The convolved bound of the output layer represented in ImageZonoBound type.

propagate_layer_batch(prop_method::BetaCrown, layer::Conv, 
                       bound::BetaCrownBound, batch_info)

Propagates the bounds through the Conv layer for BetaCrown solver. It operates an conv transformation on the given input bound and returns the output bound. It first preprocesses the lower- and upper-bounds of the bias of the node using _preprocess. Then, it computes the interval map of the resulting lower- and upper-bounds using conv_bound_oneside function. The resulting bound is represented by BetaCrownBound type.

Arguments

• prop_method (BetaCrown): BetaCrown solver used for the verification process.
• layer (Conv): Conv layer of the model.
• bound (BetaCrownBound): Bound of the input, represented by BetaCrownBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• New_bound (BetaCrownBound): Bound of the output after affine transformation, which is represented by BetaCrownBound type.

propagatelayerbatch(propmethod::BetaCrown, layer::ConvTranspose, bound::BetaCrownBound, batchinfo)

Propagates the bounds through the ConvTranspose layer for BetaCrown solver. It operates an ConvTranspose transformation on the given input bound and returns the output bound. It first preprocesses the lower- and upper-bounds of the bias of the node using _preprocess. Then, it computes the interval map of the resulting lower- and upper-bounds using convtrans_bound_oneside function. The resulting bound is represented by BetaCrownBound type.

Arguments

• prop_method (BetaCrown): BetaCrown solver used for the verification process.
• layer (ConvTranspose): ConvTranspose layer of the model.
• bound (BetaCrownBound): Bound of the input, represented by BetaCrownBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• New_bound (BetaCrownBound): Bound of the output after affine transformation, which is represented by BetaCrownBound type.

forward prop for CNN, Crown, box is not using symbolic bound

propagate_layer_batch_box(prop_method::Crown, layer::Conv, 
                       bound::CrownBound, batch_info)

Propagates the bounds through the convolution layer for Crown solver. It operates an convolutional transformation on the given input bound and returns the output bound. It first concretizes the bounds and forward pro asp using batch_interval_map function. Then the bound is initalized again CrownBound type.

Arguments

• prop_method (Crown): Crown solver used for the verification process.
• layer (Dense): Dense layer of the model.
• bound (CrownBound): Bound of the input, represented by CrownBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• new_bound (CrownBound): Bound of the output after affine transformation, which is represented by CrownBound type.

propagate_layer_batch_symbolic(prop_method::Crown, layer::Conv, 
                       bound::CrownBound, batch_info)

Propagates the bounds through the convolution layer for Crown solver. It operates an convolutional transformation on the given input bound and returns the output bound. It adopt symbolic forward prop using batch_interval_map function. Then the bound is initalized again CrownBound type.

Arguments

• prop_method (Crown): Crown solver used for the verification process.
• layer (Dense): Dense layer of the model.
• bound (CrownBound): Bound of the input, represented by CrownBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• new_bound (CrownBound): Bound of the output after affine transformation, which is represented by CrownBound type.

_preprocess(node, batch_info, bias = nothing)

Preprocesses the bias of the given node for the BetaCrown solver. If the bias is not nothing, it multiplies the bias with the beta value of the node.

Arguments

• node: Node of the model.
• batch_info: Dictionary containing information of each node in the model.
• bias: Bias of the node, default is nothing.

Returns

• bias: Preprocessed bias of the node.

batch_interval_map(W::AbstractMatrix{N}, l::AbstractArray, 
                   u::AbstractArray) where N

Clamps the input to the given bounds and computes the interval map of the resulting bound using the given weight matrix.

Arguments

• W (AbstractMatrix{N}): Weight matrix of the layer.
• l (AbstractArray): Lower bound of the input.
• u (AbstractArray): Upper bound of the input.

Returns

Tuple of:

• l_new (AbstractArray): Lower bound of the output.
• u_new (AbstractArray): Upper bound of the output.

dense_bound_oneside(weight, bias, batch_size)

propagate_layer(prop_method::Box, layer::Dense, reach::LazySet, batch_info)

Propagate the bounds through the dense layer for Ai2 Box solver. It operates an approximate affine transformation (affine transformation using hyperrectangle overapproximation) on the given input bound and returns the output bound.

Arguments

• prop_method (Box): Ai2 Box solver used for the verification process.
• layer (Dense): Dense layer of the model.
• reach (LazySet): Bound of the input.
• batch_info: Dictionary containing information of each node in the model.

Returns

• reach (hyperrectangle): Bound of the output after approximate affine transformation.

propagate_layer(prop_method::ExactReach, layer::Dense, 
                 reach::ExactReachBound, batch_info)

Propagate the bounds through the dense layer. It operates an affine transformation on the given input bound and returns the output bound for ExactReach solver.

Arguments

• prop_method (ExactReach): Exact reachability method used for the verification process. This is one of the solvers used to verify the given model.
• layer (Dense): Dense layer of the model.
• reach (ExactReachBound): Bound of the input, represented by ExactReachBound type, which is a vector of LazySet type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• reach (ExactReachBound): Bound of the output after affine transformation, which is represented by ExactReachBound type.

propagate_layer(prop_method::ForwardProp, layer::Dense, 
                 reach::LazySet, batch_info)

Propagate the bounds through the dense layer. It operates an affine transformation on the given input bound and returns the output bound.

Arguments

• prop_method (ForwardProp): Forward propagation method used for the verification process. This is one of the solvers used to verify the given model.
• layer (Dense): Dense layer of the model.
• reach (LazySet): Bound of the input.
• batch_info: Dictionary containing information of each node in the model.

Returns

• reach (LazySet): Bound of the output after affine transformation.

propagate_layer_batch(prop_method::BetaCrown, layer::Dense, 
                       bound::BetaCrownBound, batch_info)

Propagates the bounds through the dense layer for BetaCrown solver. It operates an affine transformation on the given input bound and returns the output bound. It first preprocesses the lower- and upper-bounds of the bias of the node using _preprocess. Then, it computes the interval map of the resulting lower- and upper-bounds using dense_bound_oneside function. The resulting bound is represented by BetaCrownBound type.

Arguments

• prop_method (BetaCrown): BetaCrown solver used for the verification process.
• layer (Dense): Dense layer of the model.
• bound (BetaCrownBound): Bound of the input, represented by BetaCrownBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• New_bound (BetaCrownBound): Bound of the output after affine transformation, which is represented by BetaCrownBound type.

propagate_layer_batch(prop_method::Crown, layer::Dense, 
                       bound::CrownBound, batch_info)

Propagates the bounds through the dense layer for Crown solver. It operates an affine transformation on the given input bound and returns the output bound. It first clamps the input bound and multiplies with the weight matrix using batch_interval_map function. Then, it adds the bias to the output bound. The resulting bound is represented by CrownBound type.

Arguments

• prop_method (Crown): Crown solver used for the verification process.
• layer (Dense): Dense layer of the model.
• bound (CrownBound): Bound of the input, represented by CrownBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• new_bound (CrownBound): Bound of the output after affine transformation, which is represented by CrownBound type.

propagate_layer(prop_method, σ::typeof(identity), bound, batch_info)

Propagate the bounds through the identity activation layer.

Arguments

• prop_method: Propagation method.
• σ: Identity activation function.
• bound: Bounds of the input.
• batch_info: Dictionary containing information of each node in the model.

Returns

• bound: Bounds of the output, which is equivalent to the bounds of the input.

bn_bound_oneside(last_A, weight, bias, stride, pad, dilation, groups, size_before_layer,size_after_layer, batch_size)

propagate_layer(prop_method::ImageStar, layer::BatchNorm, 
                 bound::ImageStarBound, batch_info)

Propagate the ImageStarBound bound through a batch norm layer. I.e., it applies the batch norm operation to the ImageStarBound bound. The batch norm operation is decomposed into two operations: centering and scaling. The centering operation is applied to the center of the ImageStarBound bound. The scaling operation is applied to the generators of the ImageStarBound bound. The resulting bound is also of type ImageStarBound.

Arguments

• prop_method (ImageStar): The ImageStar propagation method used for the verification problem.
• layer (BatchNorm): The batch norm operation to be used for propagation.
• bound (ImageStarBound): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The batch normed bound of the output layer represented in ImageStarBound type.

propagate_layer(prop_method::ImageZono, layer::BatchNorm, 
                 bound::ImageZonoBound, batch_info)

Propagate the ImageZonoBound bound through a batch norm layer. I.e., it applies the batch norm operation to the ImageZonoBound bound. The batch norm operation is decomposed into two operations: centering and scaling. The centering operation is applied to the center of the ImageZonoBound bound. The scaling operation is applied to the generators of the ImageZonoBound bound. The resulting bound is also of type ImageZonoBound.

Arguments

• prop_method (ImageZono): The ImageZono propagation method used for the verification problem.
• layer (BatchNorm): The batch norm operation to be used for propagation.
• bound (ImageZonoBound): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The batch normed bound of the output layer represented in ImageZonoBound type.

propagate_linear(prop_method::BetaCrown, layer::BatchNorm, 
                 bound::BetaCrownBound, batch_info)

Propagate the BetaCrownBound bound through a batch norm layer. I.e., it applies the "inverse" batch norm operation to the BetaCrownBound bound. The resulting bound is also of type BetaCrownBound.

Arguments

• prop_method (Crown): The Crown propagation method used for the verification problem.
• layer (BetaCrown): The batch norm operation to be used for propagation.
• bound (BetaCrownBound): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The batch normed bound of the output layer represented in BetaCrownBound type.

propagate_layer(prop_method::Crown, layer::BatchNorm, 
                 bound::CrownBound, batch_info)

Propagate the CrownBound bound through a batch norm layer. I.e., it applies the batch norm operation to the CrownBound bound. The resulting bound is also of type CrownBound.

Arguments

• prop_method (Crown): The Crown propagation method used for the verification problem.
• layer (BatchNorm): The batch norm operation to be used for propagation.
• bound (CrownBound): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The batch normed bound of the output layer represented in CrownBound type.

propagate_layer_batch(layer::BatchNorm, batch_reach::AbstractArray, 
                       batch_info)

Propagate the batch_reach through a batch norm layer. I.e., it applies the batch norm operation to the batch_reach. The batch norm operation is decomposed into two operations: centering and scaling. This function supports input batch with channel dimension.

Arguments

• layer (BatchNorm): The batch norm operation to be used for propagation.
• batch_reach (AbstractArray): The batch of input bounds.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The batch normed bound of the output layer.

ImageStar_to_Star(bound::ImageStarBound)

Convert the ImageStarBound bound to Star bound.

Arguments

• bound (ImageStarBound): The bound of the input node, represented using ImageStarBound type.

Returns

• The bound represented using Star type.

Star_to_ImageStar(bound::Star, sz)

Converts the Star bound to ImageStarBound bound.

Arguments

• bound (Star): The bound of the input node, represented using Star type.
• sz: The size of the input image, i.e., the target size.

Returns

• The bound represented using ImageStarBound type.

bound_oneside(last_A, slope_pos, slope_neg)

Bound the ReLU activation function from one side, such as upper or lower.

Arguments

• last_A: The last layer's activation.
• slope_pos: The slope of the ReLU activation function from the positive side.
• slope_neg: The slope of the ReLU activation function from the negative side.

Returns

• The bound of the ReLU activation function from one side.

fast_overapproximate(r::Rectification{N,<:AbstractZonotope}, 
                     ::Type{<:Zonotope}) where {N}

Computes the overapproximation of the rectified set r using a Zonotope.

Arguments

• r (Rectification): The rectified set.
• ::Type{<:Zonotope}: The type of the overapproximation, default is Zonotope.

Returns

• The overapproximation of the rectified set r using a Zonotope.

multiply_by_A_signs(last_A, slope_pos, slope_neg)

Multiply the last layer's activation by the sign of the slope of the ReLU activation function. This is for BetaLayer propagation method.

partition_relu(bound)

Partition the bound into multiple VPolytope objects, each of which is the intersection of the bound and an orthant. The resulting VPolytope objects are stored in an array. This is for ReLU propagations in ExactReach solver. Thus, the resulting VPolytope objects are the outputs of rectifying the input bound. The dimension of the bound must be less than 30, since otherwise the number of output sets will be too large.

Arguments

• bound: The bound of the input node.

Returns

• An array of partitioned bounds represented using VPolytope type.

propagate_layer(prop_method, layer::typeof(relu), bound::Star, batch_info)

Propagate the Star bound through a ReLU layer. I.e., it applies the ReLU operation to the Star bound. The resulting bound is also of type Star. This is for Star propagation methods.

Arguments

• prop_method: The propagation method used for the verification problem.
• layer (typeof(relu)): The ReLU operation to be used for propagation.
• bound (Star): The bound of the input node, represented using Star type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• the relued bound of the output represented in Star type.

Reference

[1] HD. Tran, S. Bak, W. Xiang, and T.T. Johnson, "Verification of Deep Convolutional Neural Networks Using ImageStars," in Computer Aided Verification (CAV), 2020.

propagate_layer(prop_method, layer::typeof(relu), 
              bound::ImageStarBound, batch_info)

Propagate the ImageStarBound bound through a ReLU layer. I.e., it applies the ReLU operation to the ImageStarBound bound. The resulting bound is also of type ImageStarBound. This is for ImageStar propagation method. It converts the input bound to Star type, calls propagate_layer that propagates the Star bound through a ReLU layer, and converts the resulting bound back to ImageStarBound.

Arguments

• prop_method: The propagation method used for the verification problem.
• layer (typeof(relu)): The ReLU operation to be used for propagation.
• bound (ImageStarBound): The bound of the input node, represented using ImageStarBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• The relued bound of the output represented in ImageStarBound type.

propagate_layer(prop_method, layer::typeof(relu), 
              bound::ImageZonoBound, batch_info)

Propagate the ImageZonoBound bound through a ReLU layer. I.e., it applies the ReLU operation to the ImageZonoBound bound. The resulting bound is also of type ImageZonoBound. This is for ImageZono propagation method. It flattens the input bound into a Zonotope and calls fast_overapproximate that computes the overapproximation of the rectified set using a Zonotope. It then converts the resulting Zonotope back to ImageZonoBound.

Arguments

• prop_method: The propagation method used for the verification problem.
• layer (typeof(relu)): The ReLU operation to be used for propagation.
• bound (ImageZonoBound): The bound of the input node, represented using ImageZonoBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• the relued bound of the output represented in ImageZonoBound type.

propagate_layer(prop_method::Box, layer::typeof(relu), 
              reach::AbstractPolytope, batch_info)

Propagate the AbstractPolytope bound through a ReLU layer. I.e., it applies the ReLU operation to the AbstractPolytope bound. The resulting bound is also of type AbstractPolytope. This is for Ai2's Box propagation method. It calls rectify that rectifies the input bound.

Arguments

• prop_method (Box): The propagation method used for the verification problem.
• layer (typeof(relu)): The ReLU operation to be used for propagation.
• reach (AbstractPolytope): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• the relued bound of the output represented in AbstractPolytope type.

propagate_layer(prop_method::ExactReach, layer::typeof(relu), 
              reach::ExactReachBound, batch_info)

Propagate the ExactReachBound bound through a ReLU layer. I.e., it applies the ReLU operation to the ExactReachBound bound. The resulting bound is also of type ExactReachBound. This is for ExactReach propagation method. It calls partition_relu that partitions the resulting rectified bound into multiple VPolytope objects, each of which is the intersection of the resulting bound and an orthant. The resulting VPolytope objects are vertically concatenated and stored in an ExactReachBound object.

Arguments

• prop_method (ExactReach): The propagation method used for the verification problem.
• layer (typeof(relu)): The ReLU operation to be used for propagation.
• reach (ExactReachBound): The bound of the input node, represented using ExactReachBound type.
• batch_info: Dictionary containing information of each node in the model.

Returns

• the relued bound of the output represented in ExactReachBound type.

propagate_layer(prop_method::Union{Ai2z, ImageZono}, layer::typeof(relu), 
              reach::AbstractPolytope, batch_info)

Propagate the AbstractPolytope bound through a ReLU layer. I.e., it applies the ReLU operation to the AbstractPolytope bound. The resulting bound is also of type AbstractPolytope. This is for either Ai2z or ImageZono propagation methods, which both use Zonotope-like representation for the safety specifications. After rectifying the input bound, it overapproximates the resulting bound using a Zonotope.

Arguments

• prop_method (Union{Ai2z, ImageZono}): The propagation method used for the verification problem. It can be either Ai2z or ImageZono, which both use Zonotope-like representation for the safety specifications.
• layer (typeof(relu)): The ReLU operation to be used for propagation.
• reach (AbstractPolytope): The bound of the input node.
• batch_info: Dictionary containing information of each node in the model.

Returns

• the relued bound of the output represented in Zonotope type.

propagate_layer_batch(prop_method::Crown, layer::typeof(relu), 
                    bound::CrownBound, batch_info)

Propagate the CrownBound bound through a ReLU layer.

relu_upper_bound(lower, upper)

Compute the upper bound slope and intercept according to CROWN relaxation.

Arguments

• lower: The lower bound of the input node, pre-ReLU operation.
• upper: The upper bound of the input node, pre-ReLU operation.

Returns

• The upper bound slope and intercept according to CROWN relaxation.