Solvers

PropMethod

Algorithm to propagate the bounds through the computational graph. This is the super-type for all the "solvers" used in the verification process, and is different from the functions defined in propagate folder. In other words, the PropMethod should be understood as the "solver" used in the verification process, while the functions in propagate folder are the "propagation" functions used in the verification process. The solvers include methods such as Ai2 and Crown. For an example, see the documentation on Ai2.

ForwardProp <: PropMethod

Abstract type representing solvers that use forward propagation.

BackwardProp <: PropMethod

Abstract type representing solvers that use backward propagation.

SequentialForwardProp <: ForwardProp

SequentialBackwardProp <: ForwardProp

BatchForwardProp <: ForwardProp

BatchBackwardProp <: BackwardProp

Bound

Abstract type representing bounds.

prepare_method(prop_method::PropMethod, batch_input::AbstractVector, batch_output::AbstractVector, batch_inheritance::AbstractVector, model_info)

Initialize the bound of the start node of the computational graph based on the solver (prop_method).

Agruments

• prop_method (PropMethod): Propagation method, i.e., the solver.
• batch_input (AbstractVector): Batch of inputs.
• batch_output (AbstractVector): Batch of outputs.
• batch_inheritance (AbstractVector): Batch of inheritance, can be used to inheritate pre-act-bound from the parent branch
• model_info: Structure containing the information of the neural network to be verified.

Returns

• batch_output: Batch of outputs.
• batch_info: Dictionary containing information of each node in the model.

init_propagation(prop_method::ForwardProp, batch_input, batch_output, model_info)

Returns a dictionary containing the information of each node in the model. This function is for ForwardProp solvers, and is mainly concerned with initializing the dictionary, batch_info, and populating it with the initial bounds for the starting node. For the starting node of the model, the :bound key is mapped to the list of input specifications.

Arguments

• prop_method (ForwardProp): Solver that uses forward propagation.
• batch_input: List of inputs.
• batch_output: List of outputs.
• model_info: Structure containing the information of the neural network to be verified.

Returns

• batch_info: Dictionary containing information of each node in the model.

init_propagation(prop_method::BackwardProp, batch_input, batch_output, model_info)

Returns a dictionary containing the information of each node in the model. This function is for BackwardProp solvers, and is mainly concerned with initializing the dictionary, batch_info, and populating it with the initial bounds for the starting node. For the starting node of the model, the :bound key is mapped to the list of input specifications.

Arguments

• prop_method (BackwardProp): Solver that uses backward propagation.
• batch_input: List of inputs.
• batch_output: List of outputs.
• model_info: Structure containing the information of the neural network to be verified.

Returns

• batch_info: Dictionary containing information of each node in the model.

init_batch_bound(prop_method::ForwardProp, batch_input, batch_output)

Returns a list of the input specifications (geometries) for the given batch of inputs. This is for ForwardProp solvers. Each input specification is processed to fit the geometric representation used by the solver.

Arguments

• prop_method (ForwardProp): Solver that uses forward propagation method.
• batch_input: Array of inputs.
• batch_output: Array of outputs.

Returns

• List of the input specifications for the given batch of inputs.

init_batch_bound(prop_method::BackwardProp, batch_input, batch_output)

Returns a list of the output specifications (geometries) for the given batch of outputs. This is for BackwardProp solvers. Each input specification is processed to fit the geometric representation used by the solver.

Arguments

• prop_method (BackwardProp): Solver that uses backward propagation method.
• batch_input: Array of inputs.
• batch_output: Array of outputs.

Returns

• List of the output specifications for the given batch of outputs.

init_bound(prop_method::ForwardProp, input)

Returns the geometry representation used to encode the input specification. This is for ForwardProp solvers.

Arguments

• prop_method (ForwardProp): Solver that uses forward propagation method.
• input: Geometry representation used to encode the input specification.

Returns

• input: Geometry representation used to encode the input specification.

init_bound(prop_method::BackwardProp, output)

Returns the geometry representation used to encode the output specification. This is for BackwardProp solvers.

Arguments

• prop_method (BackwardProp): Solver that uses backward propagation method.
• output: Geometry representation used to encode the output specification.

Returns

• output: Geometry representation used to encode the output specification.

process_bound(prop_method::PropMethod, batch_bound, batch_out_spec, model_info, batch_info)

Returns the list of bounds resulting from the propagation and the information of the batch.

Arguments

• prop_method (PropMethod): Solver.
• batch_bound: List of the bounds for the given batch.
• batch_out_spec: List of the output specifications for the given batch of outputs.
• 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: List of the bounds for the given batch.
• batch_info: Dictionary containing information of each node in the model.

check_inclusion(prop_method::ForwardProp, model, batch_input::AbstractArray, batch_reach::AbstractArray, batch_output::AbstractArray)

Determines whether the reachable sets, batch_reach, are within the respective valid output sets, batch_output.

Arguments

• prop_method (ForwardProp): Solver being used.
• model: Neural network model that is to be verified.
• input (AbstractArray): List of input specifications.
• reach (AbstractArray): List of reachable sets.
• output (AbstractArray) : List of sets of valid outputs.

Returns

List of a combination of the following components:

• ReachabilityResult(:holds, [reach]) if reach is a subset of output.
• CounterExampleResult(:unknown) if reach is not a subset of output, but cannot find a counterexample.
• CounterExampleResult(:violated, x) if reach is not a subset of output, and there is a counterexample.

ExactReach <: SequentialForwardProp

ExactReach performs exact reachability analysis to compute the exact reachable set for a network. It works for piecewise linear networks with either linear or ReLU activations. It computes the reachable set for every linear segment of the network and keeps track of all sets. The final reachable set is the union of all sets. Since the number of linear segments is exponential in the number of nodes in one layer, this method is not scalable.

Problem Requirement

1. Network: any depth, ReLU activation (more activations to be supported in the future)
2. Input: Array of AbstractPolytope, i.e., union of polytopes.
3. Output: Array of AbstractPolytope, i.e., union of polytopes.

Returns

BasicResult(:holds), BasicResult(:violated)

Method

Reachability analysis using split and join.

Property

Sound and complete.

Reference

[1] C. Liu, T. Arnon, C. Lazarus, C. Strong, C. Barret, and M. J. Kochenderfer, "Algorithms for Verifying Deep Neural Networks," in Foundations and Trends in Optimization, 2021.

[2] W. Xiang, H.-D. Tran, and T. T. Johnson, "Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations," ArXiv Preprint ArXiv:1712.08163, 2017.

ExactReachBound <: Bound

Bound for ExactReach solver. It is a union of polytopes, represented with an array of LazySet.

Fields

• polys (AbstractArray{LazySet}): Array of polytopes.

get_center(bound::ExactReachBound)

Returns a randomly sampled point from the first polytope in the array of polytopes, bound.polys.

Arguments

• bound (ExactReachBound): The ExactReachBound to sample from.

Returns

• A randomly sampled point from the first polytope in the array of polytopes.

prepare_problem(search_method::SearchMethod, split_method::SplitMethod, 
                prop_method::ExactReach, problem::Problem)

Preprocessing of the Problem to be solved. This method converts the model to a bounded computational graph, makes the input specification compatible with the solver, and returns the model information and preprocessed Problem. This in turn also initializes the branch bank.

Arguments

• search_method (SearchMethod): Method to search the branches.
• split_method (SplitMethod): Method to split the branches.
• prop_method (ExactReach): Solver to be used, specifically the ExactReach.
• problem (Problem): Problem to be preprocessed to better fit the solver.

Returns

• model_info, a structure containing the information of the neural network to be verified.
• Problem after processing the initial input specification and model.

init_bound(prop_method::ExactReach, bound::LazySet)

For the ExactReach solver, this function converts the input set, represented with a LazySet, to an ExactReachBound representation. This serves as a preprocessing step for the ExactReach solver.

Arguments

• prop_method (ExactReach): ExactReach solver.
• bound (LazySet): Input set, represented with a LazySet.

Returns

• ExactReachBound representation of the input set.

check_inclusion(prop_method::ExactReach, model, input::ExactReachBound, 
                reach::ExactReachBound, output::LazySet)

Determines whether the reachable set, reach, is within the valid output specified by a LazySet. This function achieves this by directly checking if all the reachable sets in reach are subsets of the set of valid outputs output. If not, it returns BasicResult(:violated). Otherwise, it returns BasicResult(:holds).

Arguments

• prop_method (ExactReach): Solver being used.
• model: Neural network model that is to be verified.
• input (ExactReachBound): Input specification represented with an ExactReachBound.
• reach (ExactReachBound): Reachable set resulting from the propagation of input through the model, represented with an ExactReachBound.
• output (LazySet): Set of valid outputs represented with a LazySet.

Returns

• BasicResult(:holds) if all reachable sets in reach are subsets of output.
• BasicResult(:violated) if any reachable set in reach is not a subset of output.

Ai2{T<:Union{Hyperrectangle, Zonotope, HPolytope, Star}} 
                                <: SequentialForwardProp

Ai2 performs over-approximated reachability analysis to compute the over- approximated output reachable set for a network. T can be Hyperrectangle, Zonotope, Star, or HPolytope. Different geometric representations impact the verification performance due to different over-approximation sizes. We use Zonotope as "benchmark" geometry, as in the original implementation[1], due to improved scalability and precision (similar results can be achieved using Star). On the other hand, using a HPolytope representation potentially leads to a more precise but less scalable result, and the opposite holds for Hyperrectangle.

Note that initializing Ai2() defaults to Ai2{Zonotope}. The following aliases also exist for convenience:

Problem Requirement

1. Network: any depth, ReLU activation (more activations to be supported in the future)
2. Input: AbstractPolytope

const Ai2h = Ai2{HPolytope}
const Ai2z = Ai2{Zonotope}
const Ai2s = Ai2{Star}
const Box = Ai2{Hyperrectangle}

1. Output: AbstractPolytope

Returns

ReachabilityResult, CounterExampleResult

Method

Reachability analysis using split and join.

Property

Sound but not complete.

Reference

[1] T. Gehr, M. Mirman, D. Drashsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, "Ai2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation," in 2018 IEEE Symposium on Security and Privacy (SP),

compute_bound(bound::Zonotope)

Computes the lower- and upper-bounds of a zonotope. This function is used when propagating through the layers of the model. Radius is the sum of the absolute value of the generators of the given zonotope.

Arguments

• bound (Zonotope) : zonotope of which the bounds need to be computed

Returns

• Lower- and upper-bounds of the Zonotope.

StarSet

Covers supported Ai2 variations: Ai2h, Ai2z, Ai2s, Box.

Fields

• pre_bound_method (Union{SequentialForwardProp, Nothing}): The geometric representation used to compute the over-approximation of the input bounds.

compute_bound(bound::Star)

Computes the lower- and upper-bounds of a star set. This function is used when propagating through the layers of the model. It overapproximates the given star set with a hyperrectangle.

Arguments

• bound (Star): Star set of which the bounds need to be computed.

Returns

• Lower- and upper-bounds of the overapproximated hyperrectangle.

init_bound(prop_method::StarSet, input::Hyperrectangle)

Given a hyperrectangle as input, this function returns a star set that encompasses the hyperrectangle. This helps a more precise computation of bounds.

Arguments

• prop_method (StarSet): StarSet-type solver; includes Ai2h, Ai2z, Ai2s, Box.
• input (Hyperrectangle): Hyperrectangle to be converted into a star set

Returns

• Star set that encompasses the given hyperrectangle.

prepare_method(prop_method::StarSet, batch_input::AbstractVector, 
batch_output::AbstractVector, model_info)

Initialize the bound of the start node of the computational graph for the StarSet solvers.

Arguments

• prop_method (StarSet) : Propagation method of type StarSet.
• batch_input (AbstractVector) : Batch of inputs.
• batch_output (AbstractVector) : Batch of outputs.
• model_info: Structure containing the information of the neural network to be verified.

Returns

• batch_output: batch of outputs.
• batch_info: Dictionary containing information of each node in the model.

check_inclusion(prop_method::ForwardProp, model, input::LazySet, 
reach::LazySet, output::LazySet)

Determines whether the reachable set, reach, is within the valid output specified by a LazySet. This function achieves this by directly checking if the reachable set reach is a subset of the set of valid outputs output. If not, it attempts to find a counterexample and returns the appropriate Result.

Arguments

• prop_method (ForwardProp): Solver being used.
• model: Neural network model that is to be verified.
• input (LazySet): Input specification supported by LazySet.
• reach (LazySet): Reachable set resulting from the propagation of input through the model.
• output (LazySet) : Set of valid outputs represented with a LazySet.

Returns

• ReachabilityResult(:holds, [reach]) if reach is a subset of output.
• CounterExampleResult(:unknown) if reach is not a subset of output, but cannot find a counterexample.
• CounterExampleResult(:violated, x) if reach is not a subset of output, and there is a counterexample.

check_inclusion(prop_method::ForwardProp, model, input::LazySet, 
reach::LazySet, output::Complement)

Determines whether the reachable set, R(input, model), is within the valid output specified by a LazySet. This function achieves this by checking if the box approximation (overapproximation with hyperrectangle) of the reach set is disjoint with the unsafe_output. If the box approximation is a subset of the unsafe_output, then the safety property is violated.

Arguments

• prop_method (ForwardProp): Solver being used.
• model: Neural network model that is to be verified.
• input (LazySet): Input specification supported by Lazyset.
• reach (LazySet): Reachable set resulting from the propagation of input through the model.
• output (Complement): Set of valid outputs represented with a complement set. For problems using this check_inclusion method, the unsafe region is specified. Then, the complement of the unsafe region is given as the desired output specification.

Returns

• ReachabilityResult(:holds, [reach]) if box_reach is disjoint with the complement of the output.
• CounterExampleResult(:violated, x) if the center of the input set results in a state that belongs to the unsafe_output.
• CounterExampleResult(:unknown) if either the two cases above are true.

ImageStar <: SequentialForwardProp

ImageStar is a verification approach that can verify the robustness of Convolutional Neural Network (CNN). This toolbox uses the term, ImageStar, as the verification method itself that uses the ImageStar set. In terms of geometric representation, an ImageStar is an extension of the generalized star set such that the center and generators are images with multiple channels.

$Θ = \{ x : x = c + ∑_{i=1}^{m} (α_i v_i), \; Cα ≤ d \}$

where $c$ is the center image, $V = \{ v_1, …, v_m \}$ is the set of generator images, and $Cα ≤ d$ represent the predicate with α's as the free parameters. This set representation enables efficient over-approximative analysis of CNNs. ImageStar is less conservative and faster than ImageZono [1].

Note that initializing ImageStar() defaults to ImageStar(nothing).

Fields

• pre_bound_method (Union{SequentialForwardProp, Nothing}): The geometric representation used to compute the over-approximation of the input bounds.

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.

ImageStarBound{T<:Real} <: Bound

ImageStarBound is used to represent the bounded set for ImageStar. It is an extension of the geometric representation, StarSet.

Fields

• center (AbstractArray{T, 4}): center image ("anchor" image in literature), of size heigth x width x number of channels x 1.
• generators (AbstractArray{T, 4}): matrix of generator images, of size height x width x number of channels x number of generators.
• A (AbstractArray{T, 2}): normal direction of the predicate, of size number of constraints x number of generators.
• b (AbstractArray{T, 1}): constraints of the predicate, of size number of constraints x number of generators.

prepare_problem(search_method::SearchMethod, split_method::SplitMethod, 
                prop_method::ImageStar, problem::Problem)

Preprocessing of the Problem to be solved. This method converts the model to a bounded computational graph, makes the input specification compatible with the solver, and returns the model information and preprocessed Problem. This in turn also initializes the branch bank.

Arguments

• search_method (SearchMethod): Method to search the branches.
• split_method (SplitMethod): Method to split the branches.
• prop_method (ImageStar): Solver to be used, specifically the ImageStar.
• problem (Problem): Problem to be preprocessed to better fit the solver.

Returns

• model_info, a structure containing the information of the neural network to be verified.
• Problem after processing the initial input specification and model.

prepare_method(prop_method::ImageStar, batch_input::AbstractVector, 
                batch_output::AbstractVector, batch_inheritance::AbstractVector, model_info)

Initialize the bound of the start node of the computational graph based on the pre_bound_method specified in the given ImageStar solver.

Agruments

• prop_method (ImageStar): ImageStar solver.
• batch_input (AbstractVector): Batch of inputs.
• batch_output (AbstractVector): Batch of outputs.
• batch_inheritance (AbstractVector): Batch of inheritance, can be used to inheritate pre-act-bound from the parent branch
• model_info: Structure containing the information of the neural network to be verified.

Returns

• batch_output: Batch of outputs.
• batch_info: Dictionary containing information of each node in the model.

init_bound(prop_method::ImageStar, ch::ImageConvexHull)

For the ImageStar solver, this function converts the input set, represented with an ImageConvexHull, to an ImageStarBound representation. This serves as a preprocessing step for the ImageStar solver.

Arguments

• prop_method (ImageStar): ImageStar solver.
• ch (ImageConvexHull): Convex hull, type ImageConvexHull, is used for the input specification.

Returns

• ImageStarBound set that encompasses the given ImageConvexHull.

assert_zono_star(bound::ImageStarBound)

Asserts whether the given ImageStarBound set is a Zonotope. This is done by checking whether the free parameter belongs to a unit hypercube.

compute_bound(bound::ImageStarBound)

Computes the lower- and upper-bounds of an image star set. This function is used when propagating through the layers of the model. It converts the image star set to a star set. Then, it overapproximates this star set with a hyperrectangle.

Arguments

• bound (ImageStarBound): Image star set of which the bounds need to be computed.

Returns

• Lower- and upper-bounds of the overapproximated hyperrectangle.

get_center(bound::ImageStarBound)

Returns the center image of the ImageStarBound bound.

Arguments

• bound (ImageStarBound): Geometric representation of the specification using ImageStarBound.

Returns

• ImageStarBound.center image of type AbstractArray{T, 4}.

check_inclusion(prop_method::ImageStar, model, input::ImageStarBound, 
                reach::LazySet, output::LazySet)

Determines whether the reachable set, reach, is within the valid output specified by a LazySet.

Agruments

• prop_method (ImageStar): Solver being used.
• model: Neural network model that is to be verified.
• input (ImageStarBound): Input specification supported by ImageStarBound.
• reach (LazySet): Reachable set resulting from the propagation of input through the model.
• output (LazySet): Set of valid outputs represented with a LazySet.

Returns

• ReachabilityResult(:holds, box_reach) if reach is a subset of output, the function returns :holds with the box approximation (overapproximation with hyperrectangle) of the reach set.
• CounterExampleResult(:unknown) if reach is not a subset of output, but cannot find a counterexample.
• CounterExampleResult(:violated, x) if reach is not a subset of output, and there is a counterexample.

ImageZono <: SequentialForwardProp

ImageZono is a verification approach that uses Image Zonotope as the geometric representation. It is an extension of ImageStar where there is no linear constraints on the free parameters, α:

$Θ = \{ x : x = c + ∑_{i=1}^{m} (α_i v_i) \}$

where $c$ is the center image, $V = \{ v_1, …, v_m \}$ is the set of generator images, and α's are the free parameters.

ImageZonoBound{T<:Real} <: Bound

ImageZonoBound is used to represent the bounded set for ImageZono.

Fields

• center (AbstractArray{T, 4}): center image ("anchor" image in literature), of size heigth x width x number of channels x 1.
• generators (AbstractArray{T, 4}): matrix of generator images, of size height x width x number of channels x number of generators.

prepare_problem(search_method::SearchMethod, split_method::SplitMethod, 
                prop_method::ImageZono, problem::Problem)

Converts the model to a bounded computational graph and makes input specification compatible with the solver, prop_method. This in turn also initializes the branch bank.

Arguments

• search_method (SearchMethod): Method to search the branches.
• split_method (SplitMethod): Method to split the branches.
• prop_method (ImageZono): Solver to be used, specifically the ImageZono.
• problem (Problem): Problem to be preprocessed to better fit the solver.

Returns

• model_info, a structure containing the information of the neural network to be verified.
• Problem after processing the initial input specification and model.

init_bound(prop_method::ImageZono, ch::ImageConvexHull)

For the ImageZono solver, this function converts the input set, represented with an ImageConvexHull, to an ImageZonoBound representation. This serves as a preprocessing step for the ImageZono solver.

Arguments

• prop_method (ImageZono): ImageZono solver.
• ch (ImageConvexHull): Convex hull, type ImageConvexHull, is used as the input specification.

Returns

• ImageZonoBound set that encompasses the given ImageConvexHull.

init_bound(prop_method::ImageZono, bound::ImageStarBound)

For the ImageZono solver, if the input set, represented with an ImageStarBound, is a zonotope, this function converts it to an ImageZonoBound representation.

Arguments

• prop_method (ImageZono): ImageZono solver.
• ch (ImageStarBound): ImageStarBound is used for the input specification.

Returns

• ImageZonoBound representation.

compute_bound(bound::ImageZonoBound)

Computes the lower- and upper-bounds of an image zono set. This function is used when propagating through the layers of the model. It converts the image zono set to a zonotope. Then, it computes the bounds using compute_bound(bound::Zonotope).

Arguments

• bound (ImageZonoBound): Image zono set of which the bounds need to be computed.

Returns

• Lower- and upper-bounds of the flattened zonotope.

get_center(bound::ImageZonoBound)

Returns the center image of the ImageZonoBound bound.

Arguments

• bound (ImageZonoBound): Geometric representation of the specification using ImageZonoBound.

Returns

• ImageZonoBound.center image of type AbstractArray{T, 4}.

check_inclusion(prop_method::ImageZono, model, input::ImageZonoBound, 
                reach::LazySet, output::LazySet)

Determines whether the reachable set, reach, is within the valid output specified by a LazySet.

Agruments

• prop_method (ImageZono): Solver being used.
• model: Neural network model that is to be verified.
• input (ImageZonoBound): Input specification supported by ImageZonoBound.
• reach (LazySet): Reachable set resulting from the propagation of input through the model.
• output (LazySet) : Set of valid outputs represented with a LazySet.

Returns

• ReachabilityResult(:holds, box_reach) if reach is a subset of output, the function returns :holds with the box approximation (overapproximation with hyperrectangle) of the reach set.
• CounterExampleResult(:unknown) if reach is not a subset of output, but cannot find a counterexample.
• CounterExampleResult(:violated, x) if reach is not a subset of output, and there is a counterexample.

Crown <: BatchForwardProp

CrownBound <: Bound

ConcretizeCrownBound <: Bound

prepare_problem(search_method::SearchMethod, split_method::SplitMethod, 
                prop_method::Crown, problem::Problem)

prepare_method(prop_method::Crown, batch_input::AbstractVector, 
               out_specs::LinearSpec, batch_inheritance::AbstractVector, model_info)

init_batch_bound(prop_method::Crown, batch_input::AbstractArray, out_specs)

compute_bound(bound::CrownBound)

Compute lower and upper bounds of a relu node in Crown. l, u := ([low]₊*data_min + [low]₋*data_max), ([up]₊*data_max + [up]₋*data_min)

Arguments

• bound (CrownBound): CrownBound object

Outputs:

• (lbound, ubound)

compute_bound(bound::ConcretizeCrownBound)

check_inclusion(prop_method::Crown, model, batch_input::AbstractArray, bound::CrownBound, batch_out_spec::LinearSpec)

BetaCrown <: BatchBackwardProp

BetaCrownBound <: Bound

Compute_bound

prepare_problem(search_method::SearchMethod, split_method::SplitMethod, prop_method::BetaCrown, problem::Problem)

init_batch_bound(prop_method::BetaCrown, batch_input::AbstractArray, batch_output::LinearSpec)

prepare_method(prop_method::BetaCrown, batch_input::AbstractVector, batch_output::AbstractVector, batch_inheritance::AbstractVector, model_info, sub=false)

prepare_method(prop_method::BetaCrown, batch_input::AbstractVector, out_specs::LinearSpec, inheritance_list::AbstractVector, model_info, sub=false)

update_bound_by_relu_con(node, batch_input, relu_input_lower, relu_input_upper)

initbeta(layer::typeof(relu), node, batchinfo, batch_input)

init_A_b(n, batch_size) # A x < b

init_bound(prop_method::BetaCrown, input)

optimize_model(model, input, loss_func, optimizer, max_iter)

process_bound(prop_method::PropMethod, batch_bound, batch_out_spec, model_info, batch_info)

Returns the list of bounds resulting from the propagation and the information of the batch.

Arguments

• prop_method (PropMethod): Solver.
• batch_bound: List of the bounds for the given batch.
• batch_out_spec: List of the output specifications for the given batch of outputs.
• 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: List of the bounds for the given batch.
• batch_info: Dictionary containing information of each node in the model.

get_pre_relu_A(init, use_gpu, lower_or_upper, model_info, batch_info)

get_pre_relu_spec_A(init, use_gpu, lower_or_upper, model_info, batch_info)

check_inclusion(prop_method::BetaCrown, model, batch_input::AbstractArray, bound::ConcretizeCrownBound, batch_out_spec::LinearSpec)