This toolbox is developed by the Intelligent Control Lab at the Robotics Institute at Carnegie Mellon University. It is an extension of the NeuralVerification.jl.
Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
This toolbox is developed by the Intelligent Control Lab at the Robotics Institute at Carnegie Mellon University. It is an extension of the NeuralVerification.jl.
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
- ${display_result} -
-ModelVerification.APGD — MethodAPGD(model, loss, x, y; ϵ = 10, step_size = 0.1, iters = 100, clamp_range = (0, 1))Auto Projected Gradient Descent (APGD) (https://arxiv.org/pdf/2003.01690.pdf)
Arguments:
model: The model to base teh attack upon.loss: the loss function to use, assuming that it includes the prediction function i.e. loss(x, y) = crossentropy(m(x), y)x: The input to be perturbed.step_size: The ϵ value in the FGSM step.rho: PGD success rate threshold to reduce the step size.a: momentum.iters: The maximum number of iterations to run the algorithm for.ModelVerification.FGSM — MethodFGSM(model, loss, x, y; ϵ = 0.1, clamp_range = (0, 1))Fast Gradient Sign Method (FGSM) is a method of creating adversarial examples by pushing the input in the direction of the gradient and bounded by the ε parameter.
This method was proposed by Goodfellow et al. 2014 (https://arxiv.org/abs/1412.6572)
Arguments:
model: The model to base the attack upon.loss: The loss function to use. This assumes that the loss function includes the predict function, i.e. loss(x, y) = crossentropy(model(x), y).x: The input to be perturbed by the FGSM algorithm.ϵ: The amount of perturbation to apply.ModelVerification.PGD — MethodPGD(model, loss, x, y; ϵ = 10, step_size = 0.1, iters = 100, clamp_range = (0, 1))Projected Gradient Descent (PGD) is an itrative variant of FGSM with a random point. For every step the FGSM algorithm moves the input in the direction of the gradient bounded in the l∞ norm. (https://arxiv.org/pdf/1706.06083.pdf)
Arguments:
model: The model to base teh attack upon.loss: the loss function to use, assuming that it includes the prediction function i.e. loss(x, y) = crossentropy(m(x), y)x: The input to be perturbed.step_size: The ϵ value in the FGSM step.iters: The maximum number of iterations to run the algorithm for.ModelVerification.attack — Methodattack(model, input, output; restart=100)ModelVerification.attack — Methodattack(problem; restart=100)ModelVerification.project — Methodproject(x, dir::AbstractVector, set::Hyperrectangle)ModelVerification.project — Methodproject(x, dir::AbstractVector, set::LazySet)ModelVerification.project — Methodproject(p, rect::Hyperrectangle)ModelVerification.project — Methodproject(p, polytope::LazySet)Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
ModelVerification.APGD — MethodAPGD(model, loss, x, y; ϵ = 10, step_size = 0.1, iters = 100, clamp_range = (0, 1))Auto Projected Gradient Descent (APGD) (https://arxiv.org/pdf/2003.01690.pdf)
Arguments:
model: The model to base teh attack upon.loss: the loss function to use, assuming that it includes the prediction function i.e. loss(x, y) = crossentropy(m(x), y)x: The input to be perturbed.step_size: The ϵ value in the FGSM step.rho: PGD success rate threshold to reduce the step size.a: momentum.iters: The maximum number of iterations to run the algorithm for.ModelVerification.FGSM — MethodFGSM(model, loss, x, y; ϵ = 0.1, clamp_range = (0, 1))Fast Gradient Sign Method (FGSM) is a method of creating adversarial examples by pushing the input in the direction of the gradient and bounded by the ε parameter.
This method was proposed by Goodfellow et al. 2014 (https://arxiv.org/abs/1412.6572)
Arguments:
model: The model to base the attack upon.loss: The loss function to use. This assumes that the loss function includes the predict function, i.e. loss(x, y) = crossentropy(model(x), y).x: The input to be perturbed by the FGSM algorithm.ϵ: The amount of perturbation to apply.ModelVerification.PGD — MethodPGD(model, loss, x, y; ϵ = 10, step_size = 0.1, iters = 100, clamp_range = (0, 1))Projected Gradient Descent (PGD) is an itrative variant of FGSM with a random point. For every step the FGSM algorithm moves the input in the direction of the gradient bounded in the l∞ norm. (https://arxiv.org/pdf/1706.06083.pdf)
Arguments:
model: The model to base teh attack upon.loss: the loss function to use, assuming that it includes the prediction function i.e. loss(x, y) = crossentropy(m(x), y)x: The input to be perturbed.step_size: The ϵ value in the FGSM step.iters: The maximum number of iterations to run the algorithm for.ModelVerification.attack — Methodattack(model, input, output; restart=100)ModelVerification.attack — Methodattack(problem; restart=100)ModelVerification.project — Methodproject(x, dir::AbstractVector, set::Hyperrectangle)ModelVerification.project — Methodproject(x, dir::AbstractVector, set::LazySet)ModelVerification.project — Methodproject(p, rect::Hyperrectangle)ModelVerification.project — Methodproject(p, polytope::LazySet)Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
The "branch" part of the Branch and Bound paradigm for verification algorithms. The branching folder contains algorithms for dividing the input set into searchable smaller sets, which we call "branches."
The search.jl module includes algorithms to iterate over all branches, such as BFS (Breadth-first Search) and DFS (Depth-first Search). The search.jl\search_branches function is of particular importance since it executes the verification procedure.
The split.jl module includes algorithms to split an unknown branch, such as bisect, sensitivity analysis, etc. The split.jl\split_branch function divides the unknown branches into smaller pieces and put them back to the branch bank for future verification. This is done so that we can get a more concrete answer by refining the problem in case the over-approximation introduced in the verification process prevents us from getting a firm result.
ModelVerification.SearchMethod — TypeSearchMethodAlgorithm for iterating through the branches, such as BFS (breadth-first search) and DFS (depth-first search). For an example, see the documentation on BFS.
ModelVerification.BFS — TypeBFS <: SearchMethodBreadth-first Search (BFS) used to iteratively go through the branches in the branch bank.
Fields
max_iter (Int64): Maximum number of iterations to go through the branches in the branch bank.batch_size (Int64): Size of the batch. Defaults to 1. If batch_size is greater than 1, GPU is used for parallel analysis of the nodes in the BaB.ModelVerification.SplitMethod — TypeSplitMethodAlgorithm to split an unknown branch into smaller pieces for further refinement. Includes methods such as Bisect and BaBSR. For an example, see the documentation on Bisect.
ModelVerification.Bisect — TypeBisect <: SplitMethodBisection method for splitting branches.
Fields
num_split (Int64): Number of splits to be called.ModelVerification.split_branch — Methodsplit_branch(split_method::Bisect, model::Chain, input::Hyperrectangle,
- output, model_info, batch_info)Recursively bisects the hyperrectangle input specification at the center for split_method.num_split number of times.
Arguments
split_method (Bisect): Bisection split method.model (Chain): Model to be verified.input (Hyperrectangle): Input specification represented with a Hyperrectangle.output: Output specification.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
input.ModelVerification.split_branch — Methodsplit_branch(split_method::Bisect, model::Chain, input::LazySet,
- output, model_info, batch_info)Given an input specification represented with any geometry, this function converts it to a hyperrectangle. Then, it calls split_branch(..., input::Hyperrectangle, ...) to recursively bisect the input specification for a split_method.num_split number of times.
Arguments
split_method (Bisect): Bisection split method.model (Chain): Model to be verified.input (LazySet): Input specification represented with any LazySet.output: Output specification.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
input.ModelVerification.split_branch — Methodsplit_branch(split_method::Bisect, model::Chain,
- input::ImageStarBound, output)Given an input specification represented with an ImageStarBound, this function converts it
Arguments
split_method (Bisect): Bisection split method.model (Chain): Model to be verified.input (ImageStarBound): Input specification represented with an ImageStarBound.output: Output specification.ModelVerification.split_branch — Methodsplit_branch(split_method::Bisect, model::Chain,
- input::ImageStarBound, output, model_info, batch_info)TO-BE-IMPLEMENTED
ModelVerification.split_branch — Methodsplit_branch(split_method::Bisect, model::Chain, input::ImageZonoBound,
- output, model_info, batch_info)ModelVerification.split_interval — Methodsplit_interval(dom::Hyperrectangle, i::Int64)Split a set into two at the given index.
Arguments
dom (Hyperrectangle): The set in hyperrectangle to be split.i (Int64): The index to split at.Returns
(left, right)::Tuple{Hyperrectangle, Hyperrectangle}: Two sets after split.ModelVerification.BaBSR — TypeBaBSR <: SplitMethodBranch-and-Bound method for splitting branches.
Fields
num_split (Int64): Number of splits to be called.ModelVerification.split_branch — Methodsplit_branch(split_method::BaBSR, model::Chain,
- input::ReLUConstrainedDomain, output, model_info, batch_info)ModelVerification.split_beta — Methodsplit_beta(relu_con_dict, score, split_relu_node, i, split_neurons_index_in_node, j, input, output)ModelVerification.vecsign_convert_to_original_size — Methodvecsign_convert_to_original_size(index, vector, original)Arguments
Returns
ModelVerification.vecmask_convert_to_original_size — Methodvecmask_convert_to_original_size(index, original)Arguments
Returns
ModelVerification.branching_scores_kfsb — Methodbranching_scores_kfsb(model_info, batch_info, input)"Kernel Function Split Branch"
ModelVerification.topk — Methodtopk(score, k, model_info)"Top Kernel"
ModelVerification.InputGradSplit — TypeInputGradSplit <: SplitMethodFields
num_split (Int64): Number of splits to be called.Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
The "branch" part of the Branch and Bound paradigm for verification algorithms. The branching folder contains algorithms for dividing the input set into searchable smaller sets, which we call "branches."
The search.jl module includes algorithms to iterate over all branches, such as BFS (Breadth-first Search) and DFS (Depth-first Search). The search.jl\search_branches function is of particular importance since it executes the verification procedure.
The split.jl module includes algorithms to split an unknown branch, such as bisect, sensitivity analysis, etc. The split.jl\split_branch function divides the unknown branches into smaller pieces and put them back to the branch bank for future verification. This is done so that we can get a more concrete answer by refining the problem in case the over-approximation introduced in the verification process prevents us from getting a firm result.
ModelVerification.SearchMethod — TypeSearchMethodAlgorithm for iterating through the branches, such as BFS (breadth-first search) and DFS (depth-first search). For an example, see the documentation on BFS.
ModelVerification.BFS — TypeBFS <: SearchMethodBreadth-first Search (BFS) used to iteratively go through the branches in the branch bank.
Fields
max_iter (Int64): Maximum number of iterations to go through the branches in the branch bank.batch_size (Int64): Size of the batch. Defaults to 1. If batch_size is greater than 1, GPU is used for parallel analysis of the nodes in the BaB.ModelVerification.SplitMethod — TypeSplitMethodAlgorithm to split an unknown branch into smaller pieces for further refinement. Includes methods such as Bisect and BaBSR. For an example, see the documentation on Bisect.
ModelVerification.Bisect — TypeBisect <: SplitMethodBisection method for splitting branches.
Fields
num_split (Int64): Number of splits to be called.ModelVerification.split_branch — Functionsplit_branch(split_method::Bisect, model::Chain, input::Hyperrectangle,
+ output, inheritance, model_info, batch_info, ratio=nothing)Recursively bisects the hyperrectangle input specification at the center for split_method.num_split number of times.
Arguments
split_method (Bisect): Bisection split method.model (Chain): Model to be verified.input (Hyperrectangle): Input specification represented with a Hyperrectangle.output: Output specification.inheritance: Something from the parent branch that could be reused.model_info: Structure containing the information of the neural network to be verified.batch_info: Dictionary containing information of each node in the model.raio: how much percent this branch is of the whole input set, only works for input set split.Returns
input.ModelVerification.split_branch — Functionsplit_branch(split_method::Bisect, model::Chain, input::LazySet,
+ output, inheritance, model_info, batch_info, ratio=nothing)Given an input specification represented with any geometry, this function converts it to a hyperrectangle. Then, it calls split_branch(..., input::Hyperrectangle, ...) to recursively bisect the input specification for a split_method.num_split number of times.
Arguments
split_method (Bisect): Bisection split method.model (Chain): Model to be verified.input (LazySet): Input specification represented with any LazySet.output: Output specification.inheritance: Something from the parent branch that could be reused to improve efficiency.model_info: Structure containing the information of the neural network to be verified.batch_info: Dictionary containing information of each node in the model.ratio: how much percent the current branch is of the whole input set, only works for input split.Returns
input.ModelVerification.split_branch — Methodsplit_branch(split_method::Bisect, model::Chain,
+ input::ImageStarBound, output)Given an input specification represented with an ImageStarBound, this function converts it
Arguments
split_method (Bisect): Bisection split method.model (Chain): Model to be verified.input (ImageStarBound): Input specification represented with an ImageStarBound.output: Output specification.Missing docstring for split_branch(split_method::Bisect, model::Chain, input::ImageStarBound, output, inheritance, model_info, batch_info, ratio=nothing). Check Documenter's build log for details.
ModelVerification.split_branch — Functionsplit_branch(split_method::Bisect, model::Chain, input::ImageZonoBound,
+ output, inheritance, model_info, batch_info, ratio=nothing)ModelVerification.split_interval — Methodsplit_interval(dom::Hyperrectangle, i::Int64)Split a set into two at the given index.
Arguments
dom (Hyperrectangle): The set in hyperrectangle to be split.i (Int64): The index to split at.Returns
(left, right)::Tuple{Hyperrectangle, Hyperrectangle}: Two sets after split.ModelVerification.BaBSR — TypeBaBSR <: SplitMethodBranch-and-Bound method for splitting branches.
Fields
num_split (Int64): Number of splits to be called.Missing docstring for split_branch(split_method::BaBSR, model::Chain, input::ReLUConstrainedDomain, output, inheritance, model_info, batch_info, ratio=nothing). Check Documenter's build log for details.
Missing docstring for split_beta(S_dict, score, split_relu_node, i, split_neurons_index_in_node, j, input, output). Check Documenter's build log for details.
ModelVerification.vecsign_convert_to_original_size — Methodvecsign_convert_to_original_size(index, vector, original)Arguments
Returns
ModelVerification.vecmask_convert_to_original_size — Methodvecmask_convert_to_original_size(index, original)Arguments
Returns
ModelVerification.branching_scores_kfsb — Methodbranching_scores_kfsb(model_info, batch_info, input)"Kernel Function Split Branch"
ModelVerification.topk — Methodtopk(score, k, model_info)"Top Kernel"
ModelVerification.InputGradSplit — TypeInputGradSplit <: SplitMethodFields
num_split (Int64): Number of splits to be called.Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
Deep Neural Network (DNN) is crucial in approximating nonlinear functions across diverse applications, such as computer vision and control. Verifying specific input-output properties can be a highly challenging task. To this end, we present ModelVerification.jl, the only cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying DNNs. This toolbox significantly extends and improves the previous version (NeuralVerification.jl) and is designed to empower developers and machine learning practioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.
This toolbox requires Julia v1.5 or later. Refer the official Julia documentation to install it for your system.
To download this toolbox, clone it from the Julia package manager like so:
pkg> add https://github.com/intelligent-control-lab/ModelVerification.jl/Deprecated once project is done and should be changed to "Building the package".
Go to the toolbox directory and start the Julia REPL.
julia > ]
+ModelVerification.jl · ModelVerification.jl ModelVerification.jl
Introduction
Deep Neural Network (DNN) is crucial in approximating nonlinear functions across diverse applications, such as computer vision and control. Verifying specific input-output properties can be a highly challenging task. To this end, we present ModelVerification.jl, the only cutting-edge toolbox that contains a suite of state-of-the-art methods for verifying DNNs. This toolbox significantly extends and improves the previous version (NeuralVerification.jl) and is designed to empower developers and machine learning practioners with robust tools for verifying and ensuring the trustworthiness of their DNN models.
Key features:
- Julia and Python integration: Built on Julia programming language, ModelVerification.jl leverages Julia's high-performance capabilities, ensuring efficient and scalable verification processes. Moreover, we provide the user with an easy, ready-to-use Python interface to exploit the full potential of the toolbox even without knowledge of the Julia language (for future versions).
- Different types of verification: ModelVerification.jl enables verification of several input-output specifications, such as reacability analysis, behavioral properties (e.g., to verify Deep Reinforcement Learning policies), or even robustness properties for Convolutional Neural Network (CNN). It also introduces new types of verification, not only for finding individual adversarial input, but for enumerating the entire set of unsafe zones for a given network and safety properties.
- Visualization of intermediate verification results (reachable sets): ModelVerification.jl enables the visualization of intermediate verification results in terms of reachable sets. In particular, our toolbox allows to plot the impactful features for the verification process and the correlated output reachable set (layer by layer) and thus to define new specific input-output specifications based on this information.
- Verification benchmarks: Compare our or your verification toolboxes against state-of-the-art benchmarks and evaluation criteria (VNN-Comp 2023). ModelVerification.jl includes a collection of solvers and standard benchmarks to perform this evaluation efficiently.
Setup
This toolbox requires Julia v1.5 or later. Refer the official Julia documentation to install it for your system.
Installation
To download this toolbox, clone it from the Julia package manager like so:
pkg> add https://github.com/intelligent-control-lab/ModelVerification.jl/
Develop the toolbox (for development)
Deprecated once project is done and should be changed to "Building the package".
Go to the toolbox directory and start the Julia REPL.
julia > ]
(@v1.9) > develop .
(@v1.9) > activate .
-(@v1.9) > instantiate
This will enable development mode for the toolbox. The dependency packages will also be installed. Some of the important ones are listed below.
Overview of the toolbox
ModelVerification.jl receives input as a set consisting of:
- Model to be verified,
- A safety property encoded as input-output specifications for the neural network,
- The solver to be used for the formal verification process.
The toolbox's output varies depending on the type of verification we are performing. Nonetheless, at the end of the verification process, the response of the toolbox potentially allows us to obtain provable guarantees that a given safety property holds (or does not hold) for the model tested.
For more details on how the toolbox works, please refer to the tutorial below.
Quickstart
Here is a simple example for verifying that the user-given safety property holds for a small deep neural network (DNN) with a single input node, two hidden layers with two ReLU nodes, and a single output node. We use the formal verification results obtained through the reachability analysis to get a provable answer whether the safety property holds.
First, we load the relevant libraries and the ModelVerification.jl toolbox.
using ModelVerification
+(@v1.9) > instantiate
This will enable development mode for the toolbox. The dependency packages will also be installed. Some of the important ones are listed below.
Overview of the toolbox
ModelVerification.jl receives input as a set consisting of:
- Model to be verified,
- A safety property encoded as input-output specifications for the neural network,
- The solver to be used for the formal verification process.
The toolbox's output varies depending on the type of verification we are performing. Nonetheless, at the end of the verification process, the response of the toolbox potentially allows us to obtain provable guarantees that a given safety property holds (or does not hold) for the model tested.
For more details on how the toolbox works, please refer to the tutorial below.
Quickstart
Here is a simple example for verifying that the user-given safety property holds for a small deep neural network (DNN) with a single input node, two hidden layers with two ReLU nodes, and a single output node. We use the formal verification results obtained through the reachability analysis to get a provable answer whether the safety property holds.
First, we load the relevant libraries and the ModelVerification.jl toolbox.
using ModelVerification
using Flux
using LazySets
First, load the model.
onnx_path = "models/small_nnet.onnx"
toy_model = ModelVerification.build_flux_model(onnx_path)
Suppose we want to verify that all inputs in $\mathcal{X}=[-2.5, 2.5]$ are mapped into $\mathcal{Y}=[18.5, 114.5]$. We encode this safety property using convex sets, provided by LazySets.
X = Hyperrectangle(low = [-2.5], high = [2.5]) # expected out: [18.5, 114.5]
@@ -14,4 +14,4 @@
upper_bound = true
solver = Crown(use_gpu, lower_bound, upper_bound)
Finally, we can verify that the safety property holds for this simple example!
result = verify(search_method, split_method, solver, problem)
println(result)
-println(result.status)
CROWN verifies that the input-output relationship holds!
Tutorials
- Tutorials
- Example 1: Verifying a toy DNN with reachability analysis
- Example 2: Verifying a CNN for robustness safety property
- Example 3: Verifying a Deep Reinforcement Learning (DRL) policy for collision avoidance safety property
Toolbox Outline
For detailed examples on how to use different functionalities provided by the toolbox, please refer to the Tutorials. The pages below will direct you to the respective documentation for each category.
- Flow
- Problem Outline
- Network
- Input-Output Specification
- Branching
- Propagation
- Solvers
- Attacks
- Helper Functions
Python Interface
[Python Interface](./pythoninterface.md) is currently in development._
ModelVerification.jl provides an interface with Python so that users who are not familiar with Julia can still use the toolbox via Python. Moreover, it provides converters in Python for converting between different neural network file formats, such as .onnx, .pb, .pt, .h5, and .nnet.
Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
CROWN verifies that the input-output relationship holds!
For detailed examples on how to use different functionalities provided by the toolbox, please refer to the Tutorials. The pages below will direct you to the respective documentation for each category.
[Python Interface](./pythoninterface.md) is currently in development._
ModelVerification.jl provides an interface with Python so that users who are not familiar with Julia can still use the toolbox via Python. Moreover, it provides converters in Python for converting between different neural network file formats, such as .onnx, .pb, .pt, .h5, and .nnet.
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
ModelVerification.Model — TypeModelStructure containing the information of the neural network to be verified.
Fields
start_nodes (Array{String, 1}): List of input layer nodes' names.final_nodes (Array{String, 1}): List of output layer nodes' names.all_nodes (Array{String, 1}): List of all the nodes's names.node_layer (Dict): Dictionary of all the nodes. The key is the name of the node and the value is the operation performed at the node.node_prevs (Dict): Dictionary of the nodes connected to the current node. The key is the name of the node and the value is the list of nodes.node_nexts (Dict): Dictionary of the nodes connected from the current node. The key is the name of the node and the value is the list of nodes.activation_nodes (Array{String, 1}): List of all the activation nodes' names.activation_number (Int): Number of activation nodes (deprecated in the future).ModelVerification.Network — TypeNetworkA vector of layers.
Fields
layers (Vector{Layer}): Layers of the network, including the output layer.See also: Layer
ModelVerification.Layer — TypeLayer{F<:ActivationFunction, N<:Number}Consists of weights and bias for linear mapping, and activation for nonlinear mapping.
Fields
weights::Matrix{N}bias::Vector{N}activation::FSee also: Network
ModelVerification.ActivationFunction — TypeActivationFunctionFunction that calculates the output of the node. Supported activation functions are:
ReLU)Max)Id)Sigmoid)Tanh)ModelVerification.GeneralAct — TypeGeneralAct <: ActivationFunctionWrapper type for a general activation function.
Usage
act = GeneralAct(tanh)
+Network · ModelVerification.jl Network
Model
JuMP.Model — TypeModel
A mathematical model of an optimization problem.
Network
ModelVerification.Network — TypeNetwork
A vector of layers.
Fields
layers (Vector{Layer}): Layers of the network, including the output layer.
See also: Layer
sourceModelVerification.Layer — TypeLayer{F<:ActivationFunction, N<:Number}
Consists of weights and bias for linear mapping, and activation for nonlinear mapping.
Fields
weights::Matrix{N}bias::Vector{N}activation::F
See also: Network
sourceActivation Functions
ModelVerification.ActivationFunction — TypeActivationFunction
Function that calculates the output of the node. Supported activation functions are:
- ReLU (
ReLU) - Max (
Max) - Identity (
Id) - Sigmoid (
Sigmoid) - Tanh (
Tanh)
sourceModelVerification.GeneralAct — TypeGeneralAct <: ActivationFunction
Wrapper type for a general activation function.
Usage
act = GeneralAct(tanh)
act(0) == tanh(0) # true
act(10.0) == tanh(10.0) # true
act = GeneralAct(x->tanh.(x))
julia> act(-2:2)
-5-element Array{Float64,1}:
+5-element Array{FloatType[],1}:
-0.9640275800758169
-0.7615941559557649
0.0
0.7615941559557649
- 0.9640275800758169
sourceModelVerification.Id — TypeId <: ActivationFunction
Identity operator
(Id())(x) -> x
sourceModelVerification.Max — TypeMax <: ActivationFunction
(Max())(x) -> max(maximum(x), 0)
sourceModelVerification.PiecewiseLinear — TypePiecewiseLinear <: ActivationFunction
Activation function that uses linear interpolation between supplied knots. An extrapolation condition can be set for values outside the set of knots. Default is Linear.
PiecewiseLinear(knots_x, knots_y, [extrapolation = Line()])
Usage
kx = [0.0, 1.2, 1.7, 3.1]
+ 0.9640275800758169
sourceModelVerification.Id — TypeId <: ActivationFunction
Identity operator
(Id())(x) -> x
sourceModelVerification.Max — TypeMax <: ActivationFunction
(Max())(x) -> max(maximum(x), 0)
sourceModelVerification.PiecewiseLinear — TypePiecewiseLinear <: ActivationFunction
Activation function that uses linear interpolation between supplied knots. An extrapolation condition can be set for values outside the set of knots. Default is Linear.
PiecewiseLinear(knots_x, knots_y, [extrapolation = Line()])
Usage
kx = [0.0, 1.2, 1.7, 3.1]
ky = [0.0, 0.5, 1.0, 1.5]
act = PiecewiseLinear(kx, ky)
@@ -21,5 +21,5 @@
act(-102) # -42.5
act = PiecewiseLinear(kx, ky, Flat())
act(-102) # 0.0
-act(Inf) # 1.5
Extrapolations
- Flat()
- Line()
- constant (supply a number as the argument)
- Throw() (throws bounds error)
PiecewiseLinear uses Interpolations.jl.
sourceModelVerification.ReLU — TypeReLU <: ActivationFunction
(ReLU())(x) -> max.(x, 0)
sourceModelVerification.Sigmoid — TypeSigmoid <: ActivationFunction
(Sigmoid())(x) -> 1 ./ (1 .+ exp.(-x))
sourceModelVerification.Tanh — TypeTanh <: ActivationFunction
(Tanh())(x) -> tanh.(x)
sourceHelper Functions
Below are the helper functions regarding network loading (from file) & dumping (to file), property-related, activation function operations, gradient-related operations, and bound & specification related operations.
Network loading and dumping
ModelVerification.onnx_parse — Methodonnx_parse(onnx_model_path)
Creates the Model from the onnx_model_path. First, the computational graph of the ONNX model is created. Then, the Model is created using the information retrieved from the computational graph.
Arguments
onnx_model_path: String path to the ONNX model.
Returns
model_info (Model): Contains network information retrieved from the computational graph of the ONNX model.
sourceModelVerification.read_nnet — Methodread_nnet(fname::String; last_layer_activation = Id())
Read in neural net from a .nnet file and return Network struct. The .nnet format is borrowed from NNet. The format assumes all hidden layers have ReLU activation. Keyword argument last_layer_activation sets the activation of the last layer, and defaults to Id(), (i.e. a linear output layer).
Arguments
fname (String): String path to the .nnet file.last_layer_activation: Keyword argument that sets the activation of the last layer which defaults to Id().
Returns
- A vector of layers saved as
Network.
sourceModelVerification.read_layer — Functionread_layer(output_dim::Int64, f::IOStream, act = ReLU())
Read in layer from .nnet file and return a Layer containing its weights & biases. Optional argument act sets the activation function for the layer.
Arguments
output_dim (Int64): Output dimension of the layer.f (IOStream): IO stream of the .nnet file.act: Optional argument specifying the activation function of the layer. Defaults to ReLU().
Returns
Layer containing the weights and bias values (and the activation function of the layer).
sourceModelVerification.to_comment — Methodto_comment(txt)
Prepend // to each line of a string.
sourceModelVerification.print_layer — Methodprint_layer(file::IOStream, layer)
Print to file an object implementing weights(layer) and bias(layer).
Arguments
file (IOStream): IO stream of the target .nnet file.layer: Layer to be transcribed to file.
sourceModelVerification.print_header — Methodprint_header(file::IOStream, network; header_text="")
The NNet format has a particular header containing information about the network size and training data. print_header does not take training-related information into account (subject to change).
Arguments
file (IOStream): IO stream of the target .nnet file.network: Network to be transcribed to file.header_text: Optional header text that comes before the network information. Defaults to an empty string.
sourceModelVerification.write_nnet — Methodwrite_nnet(filename, network; header_text)
Write network to filename.nnet. Note: Does not perform safety checks on inputs, so use with caution.
Based on python code at https://github.com/sisl/NNet/blob/master/utils/writeNNet.py and follows .nnet format given here: https://github.com/sisl/NNet.
Arguments
outfile: String name of the .nnet file.network: Network to be transcribed to outfile.nnet.header_text: Optional header text that comes before the network information.
sourceModelVerification.build_flux_model — Methodbuild_flux_model(onnx_model_path)
Builds a Flux.Chain from the given ONNX model path.
Arguments
onnx_model_path: String path to ONNX model in .onnx file.
Returns
model: Flux.Chain constructed from the .onnx file.
sourceModelVerification.get_chain — Methodget_chain(vertex)
Returns a Flux.Chain constructed from the given vertex. This is a helper function for build_flux_model.
Arguments
vertex: Vertex from the NaiveNASflux computation graph.
Returns
model: Flux.Chain constructed from the given vertex.curr_vertex: The last vertex in the chain.
sourceModelVerification.purify_flux_model — Methodpurify_flux_model(model::Chain)
Removes the starting Flatten layer from the model. This is a wrapper function for remove_flux_start_flatten.
Arguments
model (Chain): Flux.Chain model.
Returns
model (Chain): Flux.Chain model with the starting Flatten layer removed.
sourceModelVerification.remove_flux_start_flatten — Methodremove_flux_start_flatten(model::Chain)
Removes the starting Flatten layer from the model.
Arguments
model (Chain): Flux.Chain model.
Returns
model (Chain): Flux.Chain model with the starting Flatten layer removed.
sourceModelVerification.build_onnx_model — Methodbuild_onnx_model(path, model::Chain, input::InputSpec)
Builds an ONNX model from the given Flux.Chain model and input specification. The ONNX model is saved to the given path.
Arguments
path (String): Path to save the ONNX model.model (Chain): Flux.Chain model.input (InputSpec): Input specification.
Returns
path (String): Path to the saved ONNX model.
sourceNetwork properties
ModelVerification.get_act — Methodget_act(l)
Returns the activation function of the node l if it exists.
Arguments
l: node
Returns
- Activation function of the node if it exists.
- Otherwise, return
nothing.
sourceModelVerification.n_nodes — Methodn_nodes(L::Layer)
Returns the number of neurons in a layer.
Arguments
L (Layer): Layer of a network.
Returns
n (Int): Number of nodes in the layer L which is equivalent to the number of biases in the layer.
sourceModelVerification.get_sub_model — Methodget_sub_model(model_info, end_node)
sourceModelVerification.compute_output — Methodcompute_output(nnet::Network, input)
Propagates a given vector through a Network and computes the output.
Arguments
nnet (Network): Network to be propagated.input: Vector to be propagated through nnet.
Returns
Vector of the output of nnet given input.
sourceActivation function operations
ModelVerification.get_activation — Methodget_activation(L::Layer{ReLU}, x::Vector)
Finds the activation pattern of a vector x subject to the activation function given by the layer L. Returns a Vector{Bool} where true denotes the node is "active". In the sense of ReLU, this would be x[i] >= 0.
Arguments
L (Layer{ReLU}): Layer with ReLU activation function.x (Vector): Vector to be propagated through the ReLU activation function.
Returns
Vector{Bool} where true denotes the node is element-wise "active".
sourceModelVerification.get_activation — Methodget_activation(L::Layer{Id}, args...)
Finds the activation pattern of a vector x subject to the activation function given by the layer L. Returns a Vector{Bool} where true denotes the node is "active". In the sense of Identity, this would be a vector of true's for all nodes in the layer L.
Arguments
L (Layer{Id}): Layer with Identity activation function.x (Vector): Vector to be propagated through the Identity activation function.
Returns
Vector{Bool} where true denotes the node is element-wise "active".
sourceModelVerification.get_activation — Methodget_activation(nnet::Network, x::Vector{Float64})
Given a network, find the activation pattern of all neurons at a given point x. Returns Vector{Vector{Bool}}. Each Vector{Bool} refers to the activation pattern of a particular layer.
Arguments
nnet (Network): Network to be propagated.x (Vector{Float64}): Vector to be propagated through nnet.
Returns
Vector{Vector{Bool}} where each Vector{Bool} refers to the activation pattern of a particular layer.
sourceModelVerification.get_activation — Methodget_activation(nnet::Network, input::Hyperrectangle)
Given a network, find the activation pattern of all neurons for a given input set. Assume ReLU activation function for all layers. This function first computes the node-wise bounds of the input set, and then computes the activation pattern using get_activation(nnet, bounds).
Arguments
nnet (Network): Network to be propagated, with the activation function assumed to be ReLU for all layers.input (Hyperrectangle): Input set to be propagated through nnet, represented as a Hyperrectangle.
Returns
Vector{Vector{Bool}} where each Vector{Bool} refers to the activation pattern of a particular layer. Each element in each Vector{Bool} specifies the activation pattern of a particular neuron. 1 means activated, 0 means undetermined, and -1 means not activated.
sourceModelVerification.get_activation — Methodget_activation(nnet::Network, bounds::Vector{Hyperrectangle})
Given a network, find the activation pattern of all neurons given the node-wise bounds. Assume ReLU activation function for all layers. Assume pre-activation bounds where the bounds on the input are given by the first hyperrectangle, the first hidden layer by the second hyperrectangle, and so on.
Arguments
nnet (Network): Network to be propagated, with the activation function assumed to be ReLU for all layers.bounds (Vector{Hyperrectangle}): Vector of node-wise bounds, where the bounds on the input are given by the first hyperrectangle, the first hidden layer by the second hyperrectangle, and so on.
Returns
Vector{Vector{Bool}} where each Vector{Bool} refers to the activation pattern of a particular layer. Each element in each Vector{Bool} specifies the activation pattern of a particular neuron. 1 means activated, 0 means undetermined, and -1 means not activated.
sourceModelVerification.get_activation — Methodget_activation(L::Layer{ReLU}, bounds::Hyperrectangle)
Given a layer, find the activation pattern of all neurons in the layer given the node-wise bounds. Assume ReLU activation function for the given layer. Assume bounds is the pre-activation bounds for each ReLU in the layer.
Arguments
L (Layer{ReLU}): Layer to be propagated, with the activation function assumed to be ReLU.bounds (Hyperrectangle): Node-wise pre-activation bounds for the layer.
Returns
Vector{Bool} where each element refers to the activation pattern of a particular neuron. 1 means activated, 0 means undetermined, and -1 means not activated.
sourceModelVerification.approximate_act_map — Methodapproximate_act_map(act::ActivationFunction, input::Hyperrectangle)
Returns a Hyperrectangle overapproximation of the activation map of the input. act must be monotonic.
Arguments
act (ActivationFunction): Activation function to be propagated.input (Hyperrectangle): Input set to be propagated through act.
Returns
Hyperrectangle overapproximation of the activation map of the input.
sourceModelVerification.approximate_act_map — Methodapproximate_act_map(layer::Layer, input::Hyperrectangle)
Returns a Hyperrectangle overapproximation of the activation map of the input for the given layer. The activation function of the layer must be monotonic.
Arguments
layer (Layer): Layer to be propagated for the activation map.input (Hyperrectangle): Input set to be propagated through layer.
Returns
Hyperrectangle overapproximation of the activation map of the input.
sourceGradient operations
ModelVerification.get_gradient — Methodget_gradient(nnet::Network, x::Vector)
Given a network, find the gradient for the input x. The function propagates through the layers of the network, and computes the gradient at each layer. The gradient at each layer is computed by multiplying the gradient at the previous layer with the gradient of the current layer.
Arguments
nnet (Network): Network to be propagated.x (Vector): Vector to be propagated through nnet.
Returns
Matrix of the gradient for the input x after propagating through nnet.
sourceModelVerification.act_gradient — Methodact_gradient(act::ReLU, z_hat::Vector)
Compute the gradient of an ReLU activation function at point zhat. For each element in `zhat, ifzhat[i] > 0, thenactgradient[i] = 1, elseact_gradient[i] = 0`.
Arguments
act (ReLU): ReLU activation function.z_hat (Vector): Vector to be propagated through act.
Returns
Vector of the gradient of act at z_hat. Each element in the vector corresponds to the gradient of a particular neuron.
sourceModelVerification.act_gradient — Methodact_gradient(act::Id, z_hat::Vector)
Compute the gradient of an Identity activation function at point zhat. For each element in `zhat,act_gradient[i] = 1`.
Arguments
act (Id): Identity activation function.z_hat (Vector): Vector to be propagated through act.
Returns
Vector of the gradient of act at z_hat. Each element in the vector corresponds to the gradient of a particular neuron.
sourceModelVerification.relaxed_relu_gradient — Methodrelaxed_relu_gradient(l::Real, u::Real)
Return the relaxed slope of a ReLU activation based on its lower and upper bounds. The relaxed ReLU function allows for a smooth approximation of the gradient of the ReLU function. The relaxed ReLU function is defined as follows:
f'(x) = 0 if upper-bound < 0, f'(x) = 1 if lower-bound > 0, - and
f'(x) = x/(u-l) if lower-bound < x < upper-bound which is the slope of the line connecting the points (l, ReLU(l)) and (u, ReLU(u)).
This provides a differentiable approximation of the ReLU function within the interval [l, u].
Arguments
l (Real): Lower-bound of the input to the ReLU activation function.u (Real): Upper-bound of the input to the ReLU activation function.
Returns
0.0 if u <= 0.0, 1.0 if l >= 0.0,u/(u-l) otherwise.
sourceModelVerification.act_gradient_bounds — Methodact_gradient_bounds(nnet::Network, input::AbstractPolytope)
Compute the bit-wise bounds on the gradient post activation operation given an input set. Currently only support ReLU activation function. It first calculates the bounds of the input for each layer using get_bounds function (this function propagates through each layer and computes the bounds of each layer). Then, it computes the bit-wise lower and upper gradient for each layer using act_gradient. The final output is a tuple of two vectors, where each vector is a vector of bit-vectors. Each element in the vector corresponds to the gradient of a particular neuron which can be either 0 (not activated) or 1 (activated).
Arguments
nnet (Network): Network to be propagated.input (AbstractPolytope): Input set to be propagated through nnet.
Returns
LΛ, UΛ::NTuple{2, Vector{BitVector}}: lower and upper bit-wsie bounds on the activation gradients for each layer.
sourceModelVerification.get_gradient_bounds — Methodget_gradient_bounds(nnet::Network, input::AbstractPolytope)
Get lower and upper bounds on network gradient for given gradient bounds on activations, or given an input set. It first calculates the bit-wise lower and upper gradient bounds for each layer using act_gradient_bounds. Then, it computes the gradient bounds of the entire network for the weights using get_gradient_bounds.
Arguments
nnet (Network): Network to be propagated.input (AbstractPolytope): Input set to be propagated through nnet.
Returns
(LG, UG): NTuple{2, Matrix{Float64} of the lower and upper bounds of the entire network.
sourceModelVerification.get_gradient_bounds — Methodget_gradient_bounds(nnet::Network, LΛ::Vector{AbstractVector},
- UΛ::Vector{AbstractVector})
Given bit-wise lower and upper gradient bounds for each layer (LΛ and UΛ), compute the lower and upper bounds of the entire network for the weights of the layers.
Arguments
nnet (Network): Network to be propagated.LΛ (Vector{AbstractVector}): Vector of bit-wise lower gradient bounds for each layer. UΛ (Vector{AbstractVector}): Vector of bit-wise upper gradient bounds for each layer.
Returns
(LG, UG): NTuple{2, Matrix{Float64} of the lower and upper bounds of the entire network.
sourceBound & Specification operations
ModelVerification.interval_map — Methodinterval_map(W::Matrix, l::AbstractVecOrMat, u::AbstractVecOrMat)
Simple linear mapping of the weights on intervals. L, U := ([W]₊*l + [W]₋*u), ([W]₊*u + [W]₋*l)
Arguments
W (AbstractMatrix): Matrix of weights.l (AbstractVecOrMat): Vector or matrix of lower bounds.u (AbstractVecOrMat): Vector or matrix of upper bounds.
Returns
(l_new, u_new): New bounds after the linear mapping.
sourceModelVerification.get_bounds — Methodget_bounds(nnet::Network, input; before_act::Bool = false)
Computes node-wise bounds given a input set. The optional last argument determines whether the bounds are pre- or post-activation.
Arguments
nnet (Network): Network to be propagated.input (AbstractPolytope): Input set to be propagated through nnet.before_act: Optional argument that determines whether the bounds are pre- or post-activation. Defaults to false.
Returns
Vector{Hyperrectangle}: bounds for all nodes. bounds[1] is the input set overapproximated with a Hyperrectangle.
sourceModelVerification.get_bounds — Methodget_bounds(problem::Problem; kwargs...)
Compute node-wise bounds for a given Problem using get_bounds(nnet, input).
Arguments
problem (Problem): Problem to be propagated.kwargs: Keyword arguments to be passed to get_bounds(nnet, input) such as the optional boolean argument before_act.
Returns
Vector{Hyperrectangle}: bounds for all nodes. bounds[1] is the input set.
sourceModelVerification.isbounded — Methodisbounded(input)
Check if input set is bounded. If the input is of type HPolytope, then LazySets.isbounded converts the HPolytope to a HPolyhedron and checks if that is bounded. Otherwise, LazySets.isbounded is called directly.
Arguments
input: Input set to be checked for boundedness.
Returns
true if input is bounded, false otherwise.
sourceModelVerification.is_hypercube — Methodis_hypercube(set::Hyperrectangle)
Check if set is a is_hypercube. This is done by checking if all the radii of the Hyperrectangle are equal in all directions.
Arguments
set (Hyperrectangle): Set to be checked for hypercube-ness.
Returns
true if set is a hypercube, false otherwise.
sourceModelVerification.is_halfspace_equivalent — Methodis_halfspace_equivalent(set)
Check if set is halfspace equivalent. This is done by checking if the number of constraints in the set is equal to 1.
Arguments
set: Set to be checked for halfspace equivalence.
Returns
true if set is halfspace equivalent, false otherwise.
sourceModelVerification.UnboundedInputError — TypeUnboundedInputError <: Exception
Exception thrown when an input set is unbounded.
Fields
msg (String): Error message.
sourceSettings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
Extrapolations
PiecewiseLinear uses Interpolations.jl.
ModelVerification.ReLU — TypeReLU <: ActivationFunction(ReLU())(x) -> max.(x, 0)
ModelVerification.Sigmoid — TypeSigmoid <: ActivationFunction(Sigmoid())(x) -> 1 ./ (1 .+ exp.(-x))
ModelVerification.Tanh — TypeTanh <: ActivationFunction(Tanh())(x) -> tanh.(x)
Below are the helper functions regarding network loading (from file) & dumping (to file), property-related, activation function operations, gradient-related operations, and bound & specification related operations.
ModelVerification.onnx_parse — Methodonnx_parse(onnx_model_path)Creates the Model from the onnx_model_path. First, the computational graph of the ONNX model is created. Then, the Model is created using the information retrieved from the computational graph.
Arguments
onnx_model_path: String path to the ONNX model.Returns
model_info (Model): Contains network information retrieved from the computational graph of the ONNX model.ModelVerification.read_nnet — Methodread_nnet(fname::String; last_layer_activation = Id())Read in neural net from a .nnet file and return Network struct. The .nnet format is borrowed from NNet. The format assumes all hidden layers have ReLU activation. Keyword argument last_layer_activation sets the activation of the last layer, and defaults to Id(), (i.e. a linear output layer).
Arguments
fname (String): String path to the .nnet file.last_layer_activation: Keyword argument that sets the activation of the last layer which defaults to Id().Returns
Network.ModelVerification.read_layer — Functionread_layer(output_dim::Int64, f::IOStream, act = ReLU())Read in layer from .nnet file and return a Layer containing its weights & biases. Optional argument act sets the activation function for the layer.
Arguments
output_dim (Int64): Output dimension of the layer.f (IOStream): IO stream of the .nnet file.act: Optional argument specifying the activation function of the layer. Defaults to ReLU().Returns
Layer containing the weights and bias values (and the activation function of the layer).ModelVerification.to_comment — Methodto_comment(txt)Prepend // to each line of a string.
ModelVerification.print_layer — Methodprint_layer(file::IOStream, layer)Print to file an object implementing weights(layer) and bias(layer).
Arguments
file (IOStream): IO stream of the target .nnet file.layer: Layer to be transcribed to file.ModelVerification.print_header — Methodprint_header(file::IOStream, network; header_text="")The NNet format has a particular header containing information about the network size and training data. print_header does not take training-related information into account (subject to change).
Arguments
file (IOStream): IO stream of the target .nnet file.network: Network to be transcribed to file.header_text: Optional header text that comes before the network information. Defaults to an empty string.ModelVerification.write_nnet — Methodwrite_nnet(filename, network; header_text)Write network to filename.nnet. Note: Does not perform safety checks on inputs, so use with caution.
Based on python code at https://github.com/sisl/NNet/blob/master/utils/writeNNet.py and follows .nnet format given here: https://github.com/sisl/NNet.
Arguments
outfile: String name of the .nnet file.network: Network to be transcribed to outfile.nnet.header_text: Optional header text that comes before the network information.ModelVerification.build_flux_model — Methodbuild_flux_model(onnx_model_path)Builds a Flux.Chain from the given ONNX model path.
Arguments
onnx_model_path: String path to ONNX model in .onnx file.Returns
model: Flux.Chain constructed from the .onnx file.ModelVerification.get_chain — Methodget_chain(vertex)Returns a Flux.Chain constructed from the given vertex. This is a helper function for build_flux_model.
Arguments
vertex: Vertex from the NaiveNASflux computation graph.Returns
model: Flux.Chain constructed from the given vertex.curr_vertex: The last vertex in the chain.ModelVerification.purify_flux_model — Methodpurify_flux_model(model::Chain)Removes the starting Flatten layer from the model. This is a wrapper function for remove_flux_start_flatten.
Arguments
model (Chain): Flux.Chain model.Returns
model (Chain): Flux.Chain model with the starting Flatten layer removed.ModelVerification.remove_flux_start_flatten — Methodremove_flux_start_flatten(model::Chain)Removes the starting Flatten layer from the model.
Arguments
model (Chain): Flux.Chain model.Returns
model (Chain): Flux.Chain model with the starting Flatten layer removed.Missing docstring for build_onnx_model(path, model::Chain, input::InputSpec). Check Documenter's build log for details.
ModelVerification.get_act — Methodget_act(l)Returns the activation function of the node l if it exists.
Arguments
l: nodeReturns
nothing.ModelVerification.n_nodes — Methodn_nodes(L::Layer)Returns the number of neurons in a layer.
Arguments
L (Layer): Layer of a network.Returns
n (Int): Number of nodes in the layer L which is equivalent to the number of biases in the layer.ModelVerification.get_sub_model — Methodget_sub_model(model_info, end_node)ModelVerification.compute_output — Methodcompute_output(nnet::Network, input)Propagates a given vector through a Network and computes the output.
Arguments
nnet (Network): Network to be propagated.input: Vector to be propagated through nnet.Returns
Vector of the output of nnet given input.ModelVerification.get_activation — Methodget_activation(L::Layer{ReLU}, x::Vector)Finds the activation pattern of a vector x subject to the activation function given by the layer L. Returns a Vector{Bool} where true denotes the node is "active". In the sense of ReLU, this would be x[i] >= 0.
Arguments
L (Layer{ReLU}): Layer with ReLU activation function.x (Vector): Vector to be propagated through the ReLU activation function.Returns
Vector{Bool} where true denotes the node is element-wise "active".ModelVerification.get_activation — Methodget_activation(L::Layer{Id}, args...)Finds the activation pattern of a vector x subject to the activation function given by the layer L. Returns a Vector{Bool} where true denotes the node is "active". In the sense of Identity, this would be a vector of true's for all nodes in the layer L.
Arguments
L (Layer{Id}): Layer with Identity activation function.x (Vector): Vector to be propagated through the Identity activation function.Returns
Vector{Bool} where true denotes the node is element-wise "active".Missing docstring for get_activation(nnet::Network, x::Vector{Float64}). Check Documenter's build log for details.
ModelVerification.get_activation — Methodget_activation(nnet::Network, input::Hyperrectangle)Given a network, find the activation pattern of all neurons for a given input set. Assume ReLU activation function for all layers. This function first computes the node-wise bounds of the input set, and then computes the activation pattern using get_activation(nnet, bounds).
Arguments
nnet (Network): Network to be propagated, with the activation function assumed to be ReLU for all layers.input (Hyperrectangle): Input set to be propagated through nnet, represented as a Hyperrectangle.Returns
Vector{Vector{Bool}} where each Vector{Bool} refers to the activation pattern of a particular layer. Each element in each Vector{Bool} specifies the activation pattern of a particular neuron. 1 means activated, 0 means undetermined, and -1 means not activated.ModelVerification.get_activation — Methodget_activation(nnet::Network, bounds::Vector{Hyperrectangle})Given a network, find the activation pattern of all neurons given the node-wise bounds. Assume ReLU activation function for all layers. Assume pre-activation bounds where the bounds on the input are given by the first hyperrectangle, the first hidden layer by the second hyperrectangle, and so on.
Arguments
nnet (Network): Network to be propagated, with the activation function assumed to be ReLU for all layers.bounds (Vector{Hyperrectangle}): Vector of node-wise bounds, where the bounds on the input are given by the first hyperrectangle, the first hidden layer by the second hyperrectangle, and so on.Returns
Vector{Vector{Bool}} where each Vector{Bool} refers to the activation pattern of a particular layer. Each element in each Vector{Bool} specifies the activation pattern of a particular neuron. 1 means activated, 0 means undetermined, and -1 means not activated.ModelVerification.get_activation — Methodget_activation(L::Layer{ReLU}, bounds::Hyperrectangle)Given a layer, find the activation pattern of all neurons in the layer given the node-wise bounds. Assume ReLU activation function for the given layer. Assume bounds is the pre-activation bounds for each ReLU in the layer.
Arguments
L (Layer{ReLU}): Layer to be propagated, with the activation function assumed to be ReLU.bounds (Hyperrectangle): Node-wise pre-activation bounds for the layer.Returns
Vector{Bool} where each element refers to the activation pattern of a particular neuron. 1 means activated, 0 means undetermined, and -1 means not activated.ModelVerification.approximate_act_map — Methodapproximate_act_map(act::ActivationFunction, input::Hyperrectangle)Returns a Hyperrectangle overapproximation of the activation map of the input. act must be monotonic.
Arguments
act (ActivationFunction): Activation function to be propagated.input (Hyperrectangle): Input set to be propagated through act.Returns
Hyperrectangle overapproximation of the activation map of the input.ModelVerification.approximate_act_map — Methodapproximate_act_map(layer::Layer, input::Hyperrectangle)Returns a Hyperrectangle overapproximation of the activation map of the input for the given layer. The activation function of the layer must be monotonic.
Arguments
layer (Layer): Layer to be propagated for the activation map.input (Hyperrectangle): Input set to be propagated through layer.Returns
Hyperrectangle overapproximation of the activation map of the input.ModelVerification.get_gradient — Methodget_gradient(nnet::Network, x::Vector)Given a network, find the gradient for the input x. The function propagates through the layers of the network, and computes the gradient at each layer. The gradient at each layer is computed by multiplying the gradient at the previous layer with the gradient of the current layer.
Arguments
nnet (Network): Network to be propagated.x (Vector): Vector to be propagated through nnet.Returns
Matrix of the gradient for the input x after propagating through nnet.ModelVerification.act_gradient — Methodact_gradient(act::ReLU, z_hat::Vector)Compute the gradient of an ReLU activation function at point zhat. For each element in `zhat, ifzhat[i] > 0, thenactgradient[i] = 1, elseact_gradient[i] = 0`.
Arguments
act (ReLU): ReLU activation function.z_hat (Vector): Vector to be propagated through act.Returns
Vector of the gradient of act at z_hat. Each element in the vector corresponds to the gradient of a particular neuron.ModelVerification.act_gradient — Methodact_gradient(act::Id, z_hat::Vector)Compute the gradient of an Identity activation function at point zhat. For each element in `zhat,act_gradient[i] = 1`.
Arguments
act (Id): Identity activation function.z_hat (Vector): Vector to be propagated through act.Returns
Vector of the gradient of act at z_hat. Each element in the vector corresponds to the gradient of a particular neuron. ModelVerification.relaxed_relu_gradient — Methodrelaxed_relu_gradient(l::Real, u::Real)Return the relaxed slope of a ReLU activation based on its lower and upper bounds. The relaxed ReLU function allows for a smooth approximation of the gradient of the ReLU function. The relaxed ReLU function is defined as follows:
f'(x) = 0 if upper-bound < 0, f'(x) = 1 if lower-bound > 0, f'(x) = x/(u-l) if lower-bound < x < upper-bound which is the slope of the line connecting the points (l, ReLU(l)) and (u, ReLU(u)).This provides a differentiable approximation of the ReLU function within the interval [l, u].
Arguments
l (Real): Lower-bound of the input to the ReLU activation function.u (Real): Upper-bound of the input to the ReLU activation function.Returns
0.0 if u <= 0.0, 1.0 if l >= 0.0,u/(u-l) otherwise.ModelVerification.act_gradient_bounds — Methodact_gradient_bounds(nnet::Network, input::AbstractPolytope)Compute the bit-wise bounds on the gradient post activation operation given an input set. Currently only support ReLU activation function. It first calculates the bounds of the input for each layer using get_bounds function (this function propagates through each layer and computes the bounds of each layer). Then, it computes the bit-wise lower and upper gradient for each layer using act_gradient. The final output is a tuple of two vectors, where each vector is a vector of bit-vectors. Each element in the vector corresponds to the gradient of a particular neuron which can be either 0 (not activated) or 1 (activated).
Arguments
nnet (Network): Network to be propagated.input (AbstractPolytope): Input set to be propagated through nnet.Returns
LΛ, UΛ::NTuple{2, Vector{BitVector}}: lower and upper bit-wsie bounds on the activation gradients for each layer.ModelVerification.get_gradient_bounds — Methodget_gradient_bounds(nnet::Network, input::AbstractPolytope)Get lower and upper bounds on network gradient for given gradient bounds on activations, or given an input set. It first calculates the bit-wise lower and upper gradient bounds for each layer using act_gradient_bounds. Then, it computes the gradient bounds of the entire network for the weights using get_gradient_bounds.
Arguments
nnet (Network): Network to be propagated.input (AbstractPolytope): Input set to be propagated through nnet.Returns
(LG, UG): NTuple{2, Matrix{FloatType[]} of the lower and upper bounds of the entire network.ModelVerification.get_gradient_bounds — Methodget_gradient_bounds(nnet::Network, LΛ::Vector{AbstractVector},
+ UΛ::Vector{AbstractVector})Given bit-wise lower and upper gradient bounds for each layer (LΛ and UΛ), compute the lower and upper bounds of the entire network for the weights of the layers.
Arguments
nnet (Network): Network to be propagated.LΛ (Vector{AbstractVector}): Vector of bit-wise lower gradient bounds for each layer. UΛ (Vector{AbstractVector}): Vector of bit-wise upper gradient bounds for each layer. Returns
(LG, UG): NTuple{2, Matrix{FloatType[]} of the lower and upper bounds of the entire network.ModelVerification.interval_map — Methodinterval_map(W::Matrix, l::AbstractVecOrMat, u::AbstractVecOrMat)Simple linear mapping of the weights on intervals. L, U := ([W]₊*l + [W]₋*u), ([W]₊*u + [W]₋*l)
Arguments
W (AbstractMatrix): Matrix of weights.l (AbstractVecOrMat): Vector or matrix of lower bounds.u (AbstractVecOrMat): Vector or matrix of upper bounds.Returns
(l_new, u_new): New bounds after the linear mapping.ModelVerification.get_bounds — Methodget_bounds(nnet::Network, input; before_act::Bool = false)Computes node-wise bounds given a input set. The optional last argument determines whether the bounds are pre- or post-activation.
Arguments
nnet (Network): Network to be propagated.input (AbstractPolytope): Input set to be propagated through nnet.before_act: Optional argument that determines whether the bounds are pre- or post-activation. Defaults to false.Returns
Vector{Hyperrectangle}: bounds for all nodes. bounds[1] is the input set overapproximated with a Hyperrectangle.ModelVerification.get_bounds — Methodget_bounds(problem::Problem; kwargs...)Compute node-wise bounds for a given Problem using get_bounds(nnet, input).
Arguments
problem (Problem): Problem to be propagated.kwargs: Keyword arguments to be passed to get_bounds(nnet, input) such as the optional boolean argument before_act.Returns
Vector{Hyperrectangle}: bounds for all nodes. bounds[1] is the input set.ModelVerification.isbounded — Methodisbounded(input)Check if input set is bounded. If the input is of type HPolytope, then LazySets.isbounded converts the HPolytope to a HPolyhedron and checks if that is bounded. Otherwise, LazySets.isbounded is called directly.
Arguments
input: Input set to be checked for boundedness.Returns
true if input is bounded, false otherwise.ModelVerification.is_hypercube — Methodis_hypercube(set::Hyperrectangle)Check if set is a is_hypercube. This is done by checking if all the radii of the Hyperrectangle are equal in all directions.
Arguments
set (Hyperrectangle): Set to be checked for hypercube-ness.Returns
true if set is a hypercube, false otherwise.ModelVerification.is_halfspace_equivalent — Methodis_halfspace_equivalent(set)Check if set is halfspace equivalent. This is done by checking if the number of constraints in the set is equal to 1.
Arguments
set: Set to be checked for halfspace equivalence.Returns
true if set is halfspace equivalent, false otherwise.ModelVerification.UnboundedInputError — TypeUnboundedInputError <: ExceptionException thrown when an input set is unbounded.
Fields
msg (String): Error message.Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
The following Python scripts are used to convert between different neural network file formats. The supported file formats are as follows:
.onnx (Open Neural Network Exchange): Specification that defines how models should be constructed and the operators in the graph. Open-source project under the Linux Foundation. .pb (protobug): Used by TensorFlow's serving when the model needs to be deployed for production. Open-source project that is currently overviewd by Google..h5 (HDF5 binary data format): Originally used by Keras to save models. This file format is less general and more "data-oriented" and less programmatic than .pb, but simpler to use than .pb. It is easily convertible to .pb..nnet (NNet): Developed by the Stanford Intelligent Systems Laboratory, initially to define aircraft collision avoidance neural networks in human-readable text document. This format is a simple text-based format for feed-forward, fully-connected, ReLU-activate neural networks..pt (PyTorch): Used by PyTorch.Converts a .h5 model to an .onnx model.
~/ModelVerification.jl/NNet/converters$ python h52onnx.py --model_path "[path/to/h5/file]" --name_model "[path/to/converted/onnx/file]" --test_conversion [True/False]Converts a .nnet model to an .onnx model.
~/ModelVerification.jl/NNet/converters$ python nnet2onnx.py [nnetFile] [onnxFile] [outputName] [normalizeNetwork]where
nnetFile: (string) .nnet file to convert to onnx.onnxFile: (string, optional) Optional, name for the created .onnx file.outputName: (string, optional) Optional, name of the output variable in onnx.normalizeNetwork: (bool, optional) If true, adapt the network weights and biases so that networks and inputs do not need to be normalized. Default is False.Converts a .nnet model to a .pb model.
~/ModelVerification.jl/NNet/converters$ python nnet2pb.py [nnetFile] [pbFile] [output_node_names]nnetFile (string): A .nnet file to convert to Tensorflow format.pbFile (string, optional): Name for the created .pb file. Default: "".output_node_names (string, optional): Name of the final operation in the Tensorflow graph. Default: "y_out".Converts an .onnx model to a .nnet model.
~/ModelVerification.jl/NNet/converters$ python onnx2nnet.py [onnxFile] [nnetFile]onnxFile (string): Path to .onnx file.nnetFile (string, optional): Name for the created .nnet file.Converts a .pb model to a .nnet model.
~/ModelVerification.jl/NNet/converters$ python pb2nnet.py [pbFile]pbFile (string): If savedModel is false, it is the path to the frozen graph .pb file. If savedModel is true, it is the path to the savedModel folder, which contains .pb file and variables subdirectory.Converts a .pt model to an .onnx model.
~/ModelVerification.jl/NNet/converters$ python pt2onnx.py --model_path "[path/to/h5/file]" --name_model "[path/to/converted/onnx/file]" --test_conversion [True/False]Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
The following Python scripts are used to convert between different neural network file formats. The supported file formats are as follows:
.onnx (Open Neural Network Exchange): Specification that defines how models should be constructed and the operators in the graph. Open-source project under the Linux Foundation. .pb (protobug): Used by TensorFlow's serving when the model needs to be deployed for production. Open-source project that is currently overviewd by Google..h5 (HDF5 binary data format): Originally used by Keras to save models. This file format is less general and more "data-oriented" and less programmatic than .pb, but simpler to use than .pb. It is easily convertible to .pb..nnet (NNet): Developed by the Stanford Intelligent Systems Laboratory, initially to define aircraft collision avoidance neural networks in human-readable text document. This format is a simple text-based format for feed-forward, fully-connected, ReLU-activate neural networks..pt (PyTorch): Used by PyTorch.Converts a .h5 model to an .onnx model.
~/ModelVerification.jl/NNet/converters$ python h52onnx.py --model_path "[path/to/h5/file]" --name_model "[path/to/converted/onnx/file]" --test_conversion [True/False]Converts a .nnet model to an .onnx model.
~/ModelVerification.jl/NNet/converters$ python nnet2onnx.py [nnetFile] [onnxFile] [outputName] [normalizeNetwork]where
nnetFile: (string) .nnet file to convert to onnx.onnxFile: (string, optional) Optional, name for the created .onnx file.outputName: (string, optional) Optional, name of the output variable in onnx.normalizeNetwork: (bool, optional) If true, adapt the network weights and biases so that networks and inputs do not need to be normalized. Default is False.Converts a .nnet model to a .pb model.
~/ModelVerification.jl/NNet/converters$ python nnet2pb.py [nnetFile] [pbFile] [output_node_names]nnetFile (string): A .nnet file to convert to Tensorflow format.pbFile (string, optional): Name for the created .pb file. Default: "".output_node_names (string, optional): Name of the final operation in the Tensorflow graph. Default: "y_out".Converts an .onnx model to a .nnet model.
~/ModelVerification.jl/NNet/converters$ python onnx2nnet.py [onnxFile] [nnetFile]onnxFile (string): Path to .onnx file.nnetFile (string, optional): Name for the created .nnet file.Converts a .pb model to a .nnet model.
~/ModelVerification.jl/NNet/converters$ python pb2nnet.py [pbFile]pbFile (string): If savedModel is false, it is the path to the frozen graph .pb file. If savedModel is true, it is the path to the savedModel folder, which contains .pb file and variables subdirectory.Converts a .pt model to an .onnx model.
~/ModelVerification.jl/NNet/converters$ python pt2onnx.py --model_path "[path/to/h5/file]" --name_model "[path/to/converted/onnx/file]" --test_conversion [True/False]Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
Verification checks if the input-output relationships of a function, specifically deep neural networks (DNN) $\mathcal{F}$ in this case, hold. For an input specification imposed by a set $\mathcal{X}\subseteq \mathcal{D}_x$, we would like to check if the corresponding output of the function is contained in an output specification imposed by a set $\mathcal{Y}\subseteq \mathcal{D}_y$:
\[x\in\mathcal{X} \Longrightarrow y = \mathcal{F}(x) \in \mathcal{Y}.\]
Thus, a DNN-Verification problem consists of two main components:
Due to the nonlinear and nonconvex nature of DNNs, estimating the exact reachable set is impractical, although there are algorithms that allow us to do this such as ExactReach. Thus, we preform an over-approximation of the reachable set, called $\mathcal{R}$. We check its containment in the desired reachable set $\mathcal{Y}$ which if ture, we can assert that the safety property holds.
Below, we give a brief overview of models (Network), safety property, and outputs (verification results).
Details on Network
Details on Input-Output Specification
The following are the different result types used internally in the toolbox. We outline them here so that the user can have a better idea of what kind of conclusion the toolbox makes.
The user has to only interact with the wrapper ResultInfo, which contains the status and any other additional information needed to help understand the verification result.
| Output result | Explanation |
|---|---|
[BasicResult::holds] | The input-output constraint is always satisfied. |
[BasicResult::violated] | The input-output constraint is violated, i.e., it exists a single point in the input constraint that violates the property. |
[BasicResult::unknown] | Could not be determined if the property holds due to timeout in the computation. |
[CounterExampleResult] | Like BasicResult, but also returns a counterexample if one is found (if status = :violated). The counterexample is a point in the input set that, after the NN, lies outside the output constraint set. |
[AdversarialResult] | Like BasicResult, but also returns the maximum allowable disturbance in the input (if status = :violated). |
[ReachabilityResult] | Like BasicResult, but also returns the output reachable set given the input constraint (if status = :violated). |
[EnumerationResult] | Set of all the (un)safe regions in the safety property's domain. |
ModelVerification.Problem — TypeProblem{P, Q}(network::Network, input::P, output::Q)Problem definition for neural verification. The verification problem consists of: for all points in the input set, the corresponding output of the network must belong to the output set.
There are three ways to construct a Problem:
Problem(path::String, model::Chain, input_data, output_data) if both the .onnx model path and Flux_model are given.Problem(path::String, input_data, output_data) if only the .onnx model path is given.Problem(model::Chain, input_data, output_data) if only the Flux_model is given.Fields
network : Network that can be constructed either using the path to an onnx model or a Flux.Chain structure.input : Input specification defined using a LazySet.output : Output specification defined using a LazySet.ModelVerification.prepare_problem — Methodprepare_problem(search_method::SearchMethod, split_method::SplitMethod,
- prop_method::PropMethod, problem::Problem)Converts the given Problem into a form that is compatible with the verification process of the toolbox. In particular, it retrieves information about the ONNX model to be verified and stores them into a Model. It returns the Problem itself and the Model structure.
Arguments
search_method (SearchMethod): Search method for the verification process.split_method (SplitMethod): Split method for the verification process.prop_method (PropMethod): Propagation method for the verification process.problem (Problem): Problem definition for model verification.Returns
model_info (Model): Information about the model to be verified.problem (Problem): The given problem definition for model verification.ModelVerification.Result — TypeResultSupertype of all result types.
See also:
ModelVerification.ResultInfo — TypeResultInfo(status, info)Like BasicResult, but also returns a info dictionary that contains other informations. This is designed to be the general result type.
Fields
status (Symbol): Status of the result, can be :holds, :violated, or :unknown.info (Dict): A dictionary that contains information related to the result, such as the verified bounds, adversarial input bounds, counter example, etc.ModelVerification.BasicResult — TypeBasicResult(status)Result type that captures whether the input-output constraint is satisfied. Possible status values:
:holds (io constraint is satisfied always)
+Problem Outline · ModelVerification.jl Problem Outline
Verification checks if the input-output relationships of a function, specifically deep neural networks (DNN) $\mathcal{F}$ in this case, hold. For an input specification imposed by a set $\mathcal{X}\subseteq \mathcal{D}_x$, we would like to check if the corresponding output of the function is contained in an output specification imposed by a set $\mathcal{Y}\subseteq \mathcal{D}_y$:
\[x\in\mathcal{X} \Longrightarrow y = \mathcal{F}(x) \in \mathcal{Y}.\]
Thus, a DNN-Verification problem consists of two main components:
- model (DNN) : $\mathcal{F}$
- safety property (input-output specification) : $\mathcal{X}, \mathcal{Y}$.
Due to the nonlinear and nonconvex nature of DNNs, estimating the exact reachable set is impractical, although there are algorithms that allow us to do this such as ExactReach. Thus, we preform an over-approximation of the reachable set, called $\mathcal{R}$. We check its containment in the desired reachable set $\mathcal{Y}$ which if ture, we can assert that the safety property holds.
Below, we give a brief overview of models (Network), safety property, and outputs (verification results).
Network
Details on Network
Safety Property
Details on Input-Output Specification
Output (Verification Results)
The following are the different result types used internally in the toolbox. We outline them here so that the user can have a better idea of what kind of conclusion the toolbox makes.
The user has to only interact with the wrapper ResultInfo, which contains the status and any other additional information needed to help understand the verification result.
Output result Explanation [BasicResult::holds] The input-output constraint is always satisfied. [BasicResult::violated] The input-output constraint is violated, i.e., it exists a single point in the input constraint that violates the property. [BasicResult::unknown] Could not be determined if the property holds due to timeout in the computation. [CounterExampleResult] Like BasicResult, but also returns a counterexample if one is found (if status = :violated). The counterexample is a point in the input set that, after the NN, lies outside the output constraint set. [AdversarialResult] Like BasicResult, but also returns the maximum allowable disturbance in the input (if status = :violated). [ReachabilityResult] Like BasicResult, but also returns the output reachable set given the input constraint (if status = :violated). [EnumerationResult] Set of all the (un)safe regions in the safety property's domain.
Problem
ModelVerification.Problem — TypeProblem{P, Q}(network::Network, input::P, output::Q)
Problem definition for neural verification. The verification problem consists of: for all points in the input set, the corresponding output of the network must belong to the output set.
There are three ways to construct a Problem:
Problem(path::String, model::Chain, input_data, output_data) if both the .onnx model path and Flux_model are given.Problem(path::String, input_data, output_data) if only the .onnx model path is given.Problem(model::Chain, input_data, output_data) if only the Flux_model is given.
Fields
network : Network that can be constructed either using the path to an onnx model or a Flux.Chain structure.input : Input specification defined using a LazySet.output : Output specification defined using a LazySet.
sourceModelVerification.prepare_problem — Methodprepare_problem(search_method::SearchMethod, split_method::SplitMethod,
+ prop_method::PropMethod, problem::Problem)
Converts the given Problem into a form that is compatible with the verification process of the toolbox. In particular, it retrieves information about the ONNX model to be verified and stores them into a Model. It returns the Problem itself and the Model structure.
Arguments
search_method (SearchMethod): Search method for the verification process.split_method (SplitMethod): Split method for the verification process.prop_method (PropMethod): Propagation method for the verification process.problem (Problem): Problem definition for model verification.
Returns
model_info (Model): Information about the model to be verified.problem (Problem): The given problem definition for model verification.
sourceResult
ModelVerification.Result — TypeResult
Supertype of all result types.
See also:
sourceModelVerification.ResultInfo — TypeResultInfo(status, info)
Like BasicResult, but also returns a info dictionary that contains other informations. This is designed to be the general result type.
Fields
status (Symbol): Status of the result, can be :holds, :violated, or :unknown.info (Dict): A dictionary that contains information related to the result, such as the verified bounds, adversarial input bounds, counter example, etc.
sourceModelVerification.BasicResult — TypeBasicResult(status)
Result type that captures whether the input-output constraint is satisfied. Possible status values:
:holds (io constraint is satisfied always)
:violated (io constraint is violated)
-:unknown (could not be determined)
Fields
status (Symbol): Status of the result, can be :holds, :violated, or :unknown.
sourceModelVerification.CounterExampleResult — TypeCounterExampleResult(status, counter_example)
Like BasicResult, but also returns a counter_example if one is found (if status = :violated). The counter_example is a point in the input set that, after the NN, lies outside the output set.
sourceModelVerification.AdversarialResult — TypeAdversarialResult(status, max_disturbance)
Like BasicResult, but also returns the maximum allowable disturbance in the input (if status = :violated).
sourceModelVerification.ReachabilityResult — TypeReachabilityResult(status, reachable)
Like BasicResult, but also returns the output reachable set given the input constraint (if status = :violated).
sourceModelVerification.status — Functionstatus(result::Result)
Returns the status of the result. Only (:holds, :violated, :unknown) are accepted.
sourceModelVerification.validate_status — Functionvalidate_status(st)
Validates the status code. Only (:holds, :violated, :unknown) are accepted.
Arguments
st (Symbol): Status code.
Returns
- Assertion Error if the given
st is not one of (:holds, :violated, :unknown). - Otherwise, returns the given
st.
sourceSettings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
Fields
status (Symbol): Status of the result, can be :holds, :violated, or :unknown.ModelVerification.CounterExampleResult — TypeCounterExampleResult(status, counter_example)Like BasicResult, but also returns a counter_example if one is found (if status = :violated). The counter_example is a point in the input set that, after the NN, lies outside the output set.
ModelVerification.AdversarialResult — TypeAdversarialResult(status, max_disturbance)Like BasicResult, but also returns the maximum allowable disturbance in the input (if status = :violated).
ModelVerification.ReachabilityResult — TypeReachabilityResult(status, reachable)Like BasicResult, but also returns the output reachable set given the input constraint (if status = :violated).
ModelVerification.status — Functionstatus(result::Result)Returns the status of the result. Only (:holds, :violated, :unknown) are accepted.
ModelVerification.validate_status — Functionvalidate_status(st)Validates the status code. Only (:holds, :violated, :unknown) are accepted.
Arguments
st (Symbol): Status code.Returns
st is not one of (:holds, :violated, :unknown).st.Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
Functions for propagating the bound through the model (from start nodes to the end nodes) for a given branch. For a forward propagation method (ForwardProp), the start nodes are the input nodes of the computational graph and the end nodes are the output nodes. For a backward propagation method (BackwardProp), the start nodes are the output nodes and the end nodes are the input nodes. We use BFS (Breadth-first Search) to iterate through the computational graph and propagate the bounds from nodes to nodes.
The propagate\propagate.jl module defines algorithms for propagating bounds from input to output, for both forward propagation and backward propagation.
The propagate\operators folder contains specific propagation algorithms for different operators, such as ReLU, Dense, Identity, Convolution, Bivariate, etc.
ModelVerification.propagate — Functionpropagate(prop_method::PropMethod, model_info, batch_info)Propagates through the model using the specified prop_method. The propagation algorithm is as follows:
nodes, into a queue.
batch_info.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.ModelVerification.propagate_skip_method — Methodpropagate_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.ModelVerification.propagate_skip_method — Methodpropagate_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. ModelVerification.propagate_layer_method — Methodpropagate_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_linear_batch or propagate_act_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_linear_batch or propagate_act_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.ModelVerification.propagate_layer_method — Methodpropagate_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_linear_batch or propagate_act_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_linear_batch or propagate_act_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.ModelVerification.propagate_linear_batch — Methodpropagate_linear_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.ModelVerification.propagate_act_batch — Methodpropagate_act_batch(prop_method::ForwardProp, σ,
- batch_reach::AbstractArray, batch_info)Propagates each of the bound in the batch_reach array with the given forward propagation method, prop_method, through an activation 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.σ: Type of activation function, such as ReLU.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 activation layer operation. ModelVerification.propagate_skip_batch — Methodpropagate_skip_batch(prop_method::ForwardProp, layer,
+Propagation · ModelVerification.jl
Propagation
Functions for propagating the bound through the model (from start nodes to the end nodes) for a given branch. For a forward propagation method (ForwardProp), the start nodes are the input nodes of the computational graph and the end nodes are the output nodes. For a backward propagation method (BackwardProp), the start nodes are the output nodes and the end nodes are the input nodes. We use BFS (Breadth-first Search) to iterate through the computational graph and propagate the bounds from nodes to nodes.
The propagate\propagate.jl module defines algorithms for propagating bounds from input to output, for both forward propagation and backward propagation.
The propagate\operators folder contains specific propagation algorithms for different operators, such as ReLU, Dense, Identity, Convolution, Bivariate, etc.
ModelVerification.propagate — Functionpropagate(prop_method::PropMethod, model_info, batch_info)
Propagates through the model using the specified prop_method. The propagation algorithm is as follows:
- Add the connecting nodes of the start nodes, i.e., nodes after the start
nodes, into a queue.
- While the queue is not empty:
- Pop a node from the queue.
- For each node connected from the current node, i.e., for each output node:
- Increment the visit count to the output node.
- 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.
- Propagate through the current node accordingly.
- Add information about the bound of the node to
batch_info.
- 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.
sourcepropagate(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.
sourceModelVerification.propagate_skip_method — Methodpropagate_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.
sourceModelVerification.propagate_skip_method — Methodpropagate_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.
sourceModelVerification.propagate_layer_method — Methodpropagate_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.
sourceModelVerification.propagate_layer_method — Methodpropagate_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.
sourceMissing docstring. Missing docstring for propagate_linear_batch(prop_method::ForwardProp, layer, batch_reach::AbstractArray, batch_info). Check Documenter's build log for details.
Missing docstring. Missing docstring for propagate_act_batch(prop_method::ForwardProp, σ, batch_reach::AbstractArray, batch_info). Check Documenter's build log for details.
ModelVerification.propagate_skip_batch — Methodpropagate_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.
sourceModelVerification.is_activation — Methodis_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.
sourceModelVerification.propagate_layer_batch — Methodpropagate_layer_batch(prop_method, layer, batch_bound, batch_info)
Propagates through one layer. The given layer identifies what type of operation is performed. Operations such as Dense, BatchNorm, Convolution, and ReLU are supported. The prop_method denotes the solver (and thus the geometric representation for safety specification). The output of the propagation is the bounds of the given batch.
Arguments
prop_method: 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, such as Dense, BatchNorm, Convolution, or ReLU.batch_bound: Bound of the input node (the previous node).batch_info: Dictionary containing information of each node in the model.
Returns
batch_bound: The output bound after applying the operation of the node.
sourceModelVerification.enqueue_nodes! — Methodenqueue_nodes!(prop_method::ForwardProp, queue, model_info)
Inserts the nodes connected from the starting node into the given queue for ForwardProp methods.
sourceModelVerification.enqueue_nodes! — Methodenqueue_nodes!(prop_method::BackwardProp, queue, model_info)
Inserts the final nodes into the given queue for BackwardProp methods.
sourceModelVerification.output_node — Methodoutput_node(prop_method::ForwardProp, model_info)
Returns the final nodes of the model.
sourceModelVerification.next_nodes — Methodnext_nodes(prop_method::ForwardProp, model_info, node)
Returns the next nodes of the node for ForwardProp methods.
sourceModelVerification.next_nodes — Methodnext_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.
sourceModelVerification.prev_nodes — Methodprev_nodes(prop_method::ForwardProp, model_info, node)
Returns the previous nodes of the node for ForwardProp methods.
sourceModelVerification.prev_nodes — Methodprev_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.
sourceModelVerification.all_nexts_in — Methodall_nexts_in(prop_method, model_info, output_node, cnt)
Returns true if all of the next nodes of the output_node have been visited.
sourceModelVerification.all_prevs_in — Methodall_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.
sourceModelVerification.has_two_reach_node — Methodhas_two_reach_node(prop_method, model_info, node)
Checks whether there are two nodes connected to the current node, i.e., there are two previous nodes. This function is used to check if there are skip connections.
sourceBivariate
ModelVerification.propagate_skip — Methodpropagate_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.
sourceModelVerification.propagate_skip — Methodpropagate_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.
sourceConvolution
ModelVerification.bound_layer — Methodbound_layer(layer::Conv{2, 4, typeof(identity),
+ 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.
sourceModelVerification.is_activation — Methodis_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.
sourceMissing docstring. Missing docstring for propagate_layer_batch(prop_method, layer, batch_bound, batch_info). Check Documenter's build log for details.
Missing docstring. Missing docstring for enqueue_nodes!(prop_method::ForwardProp, queue, model_info). Check Documenter's build log for details.
Missing docstring. Missing docstring for enqueue_nodes!(prop_method::BackwardProp, queue, model_info). Check Documenter's build log for details.
ModelVerification.output_node — Methodoutput_node(prop_method::ForwardProp, model_info)
Returns the final nodes of the model.
sourceModelVerification.next_nodes — Methodnext_nodes(prop_method::ForwardProp, model_info, node)
Returns the next nodes of the node for ForwardProp methods.
sourceModelVerification.next_nodes — Methodnext_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.
sourceModelVerification.prev_nodes — Methodprev_nodes(prop_method::ForwardProp, model_info, node)
Returns the previous nodes of the node for ForwardProp methods.
sourceModelVerification.prev_nodes — Methodprev_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.
sourceModelVerification.all_nexts_in — Methodall_nexts_in(prop_method, model_info, output_node, cnt)
Returns true if all of the next nodes of the output_node have been visited.
sourceModelVerification.all_prevs_in — Methodall_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.
sourceMissing docstring. Missing docstring for has_two_reach_node(prop_method, model_info, node). Check Documenter's build log for details.
Bivariate
ModelVerification.propagate_skip — Methodpropagate_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.
sourceModelVerification.propagate_skip — Methodpropagate_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.
sourceConvolution
ModelVerification.bound_layer — Methodbound_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].
sourceModelVerification.bound_onside — Methodbound_onside(layer::Conv{2, 4, typeof(identity),
+ 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].
sourceModelVerification.bound_onside — Methodbound_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.
sourceModelVerification.interval_propagate — Functioninterval_propagate(layer::Conv{2, 4, typeof(identity),
+ 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.
sourceModelVerification.conv_bound_oneside — Methodconv_bound_oneside(weight, bias, stride, pad, dilation, groups, size_before_conv,size_after_conv, batch_size)
sourceModelVerification.convtrans_bound_oneside — Methodconvtrans_bound_oneside(weight, bias, stride, pad, dilation, groups, size_before_conv,size_after_conv, batch_size)
sourceModelVerification.interval_propagate — Functioninterval_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].
sourceModelVerification.propagate_by_small_batch — Methodpropagate_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.
sourceModelVerification.propagate_linear — Methodpropagate_linear(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.
sourceModelVerification.propagate_linear — Methodpropagate_linear(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.
sourceModelVerification.propagate_linear — Methodpropagate_linear(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.
sourceDense
ModelVerification._preprocess — Function_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.
sourceModelVerification.batch_interval_map — Methodbatch_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.
sourceModelVerification.dense_bound_oneside — Methoddense_bound_oneside(last_A, weight, bias, batch_size)
sourceModelVerification.propagate_linear — Methodpropagate_linear(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.
sourceModelVerification.propagate_linear — Methodpropagate_linear(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.
sourceModelVerification.propagate_linear — Methodpropagate_linear(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.
sourceModelVerification.propagate_linear_batch — Methodpropagate_linear_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.
sourceModelVerification.propagate_linear_batch — Methodpropagate_linear_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.
sourceIdentity
ModelVerification.propagate_act — Methodpropagate_act(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.
sourceNormalise
ModelVerification.propagate_linear — Methodpropagate_linear(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.
sourceModelVerification.propagate_linear — Methodpropagate_linear(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.
sourceModelVerification.propagate_linear_batch — Methodpropagate_linear_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.
sourceReLU
ModelVerification.ImageStar_to_Star — MethodImageStar_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.
sourceModelVerification.Star_to_ImageStar — MethodStar_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.
sourceModelVerification.bound_oneside — Methodbound_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.
sourceModelVerification.fast_overapproximate — Methodfast_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.
sourceModelVerification.multiply_by_A_signs — Methodmultiply_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.
sourceModelVerification.partition_relu — Methodpartition_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.
sourceModelVerification.propagate_act — Methodpropagate_act(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.
sourceModelVerification.propagate_act — Methodpropagate_act(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_act 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.
sourceModelVerification.propagate_act — Methodpropagate_act(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.
sourceModelVerification.propagate_act — Methodpropagate_act(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.
sourceModelVerification.propagate_act — Methodpropagate_act(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.
sourceModelVerification.propagate_act — Methodpropagate_act(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.
sourceModelVerification.propagate_act_batch — Methodpropagate_act_batch(prop_method::Crown, layer::typeof(relu),
- bound::CrownBound, batch_info)
Propagate the CrownBound bound through a ReLU layer.
sourceModelVerification.relu_upper_bound — Methodrelu_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.
sourceStateless
ModelVerification.propagate_linear — Methodpropagate_linear(prop_method, layer::MeanPool,
- bound::ImageStarBound, batch_info)
Propagate the ImageStarBound bound through a mean pool layer. I.e., it applies the mean pool operation to the ImageStarBound bound. The resulting bound is also of type ImageStarBound.
Arguments
prop_method: The propagation method used for the verification problem.layer (MeanPool): The mean pool 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 mean pooled bound of the output layer represented in
ImageStarBound type.
sourceModelVerification.propagate_linear — Methodpropagate_linear(prop_method, layer::MeanPool,
- bound::ImageZonoBound, batch_info)
Propagate the ImageZonoBound bound through a mean pool layer. I.e., it applies the mean pool operation to the ImageZonoBound bound. The resulting bound is also of type ImageZonoBound.
Arguments
prop_method: The propagation method used for the verification problem.layer (MeanPool): The mean pool 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 mean pooled bound of the output layer represented in
ImageZonoBound type.
sourceModelVerification.propagate_linear — Methodpropagate_linear(prop_method, layer::typeof(flatten),
- bound::ImageStarBound, batch_info)
Propagate the ImageStarBound bound through a flatten layer. I.e., it flattens the ImageStarBound into a Star type.
Arguments
prop_method: The propagation method used for the verification problem.layer (typeof(flatten)): The layer 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 flattened bound of the output layer represented in
Star type.
sourceModelVerification.propagate_linear — Methodpropagate_linear(prop_method, layer::typeof(flatten),
- bound::ImageZonoBound, batch_info)
Propagate the ImageZonoBound bound through a flatten layer. I.e., it flattens the ImageZonoBound into a Zonotope type.
Arguments
prop_method: The propagation method used for the verification problem.layer (typeof(flatten)): The layer 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 flattened bound of the output layer represented in
Zonotope type.
sourceSettings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
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
ModelVerification.propagate_by_small_batch — Methodpropagate_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
f applied to the input x.ModelVerification.propagate_layer — Methodpropagate_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
ImageStarBound type. ModelVerification.propagate_layer — Methodpropagate_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
ImageStarBound type. ModelVerification.propagate_layer — Methodpropagate_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
ImageZonoBound type. ModelVerification.propagate_layer_batch — Methodpropagate_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.ModelVerification.propagate_layer_batch — Methodpropagatelayerbatch(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.ModelVerification.propagate_layer_batch — Methodforward prop for CNN, Crown, box is not using symbolic boundModelVerification.propagate_layer_batch_box — Methodpropagate_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.ModelVerification.propagate_layer_batch_symbolic — Methodpropagate_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.ModelVerification._preprocess — Function_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.ModelVerification.batch_interval_map — Methodbatch_interval_map(W::AbstractMatrix{N}, l::AbstractArray,
+ u::AbstractArray) where NClamps 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.ModelVerification.dense_bound_oneside — Methoddense_bound_oneside(weight, bias, batch_size)ModelVerification.propagate_layer — Methodpropagate_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.ModelVerification.propagate_layer — Methodpropagate_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.ModelVerification.propagate_layer — Methodpropagate_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.ModelVerification.propagate_layer_batch — Methodpropagate_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.ModelVerification.propagate_layer_batch — Methodpropagate_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.ModelVerification.propagate_layer — Methodpropagate_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.ModelVerification.bn_bound_oneside — Methodbn_bound_oneside(last_A, weight, bias, stride, pad, dilation, groups, size_before_layer,size_after_layer, batch_size)ModelVerification.propagate_layer — Methodpropagate_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
ImageStarBound type.ModelVerification.propagate_layer — Methodpropagate_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
ImageZonoBound type.ModelVerification.propagate_layer_batch — Methodpropagate_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
BetaCrownBound type.ModelVerification.propagate_layer_batch — Methodpropagate_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
CrownBound type.ModelVerification.propagate_layer_batch — Methodpropagate_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
ModelVerification.ImageStar_to_Star — MethodImageStar_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
Star type.ModelVerification.Star_to_ImageStar — MethodStar_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
ImageStarBound type.ModelVerification.bound_oneside — Methodbound_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
ModelVerification.fast_overapproximate — Methodfast_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
r using a Zonotope.ModelVerification.multiply_by_A_signs — Methodmultiply_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.
ModelVerification.partition_relu — Methodpartition_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
VPolytope type.ModelVerification.propagate_layer — Methodpropagate_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
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.
ModelVerification.propagate_layer — Methodpropagate_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
ImageStarBound type.ModelVerification.propagate_layer — Methodpropagate_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
ImageZonoBound type.ModelVerification.propagate_layer — Methodpropagate_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
AbstractPolytope type.ModelVerification.propagate_layer — Methodpropagate_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
ExactReachBound type.ModelVerification.propagate_layer — Methodpropagate_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
Zonotope type.ModelVerification.propagate_layer_batch — Methodpropagate_layer_batch(prop_method::Crown, layer::typeof(relu),
+ bound::CrownBound, batch_info)Propagate the CrownBound bound through a ReLU layer.
ModelVerification.relu_upper_bound — Methodrelu_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
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
TO-BE-DEVELOPED
Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
TO-BE-DEVELOPED
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
A safety property is essentially an input-output relationship for the model we want to verify. In general, the constraints for the input set $\mathcal{X}$ and the output set $\mathcal{Y}$ can have any geometry. For the sake of simplicity, ModelVerification.jl uses convex polytopes and the complement of a polytope to encode the input and output specifications. Specifically, our implementation utilizes the geometric definitions of LazySets, a Julia package for calculus with convex sets. The following section dives into the geometric representations ModelVerification.jl uses and the representations required for each solver.
Different solvers implemented in ModelVerification.jl require the input-output specification formulated with particular geometries. We report here a brief overview of the sets we use. For specifics, please read Algorithms for Verifying Deep Neural Networks by C. Liu, et al. and Sets in LazySets.jl.
HyperrectangleHalfSpaceHPolytopeStarSetImageStarZonotopePolytopeComplementConvexHull| Solver | Input set | Output |
|---|---|---|
| Ai2 | ZT,SS,HP,HR | ReachabilityResult, CounterExampleResult |
| CROWN | ZT,SS,HP,HR,CH | BasicResult |
| $\alpha$-CROWN | ZT,SS,HP,HR,CH | BasicResult |
| $\beta$-CROWN | ZT,SS,HP,HR,CH | BasicResult |
| $\alpha$-$\beta$-CROWN | ZT,SS,HP,HR,CH | BasicResult |
| ImageZono | CH | ReachabilityResult, CounterExampleResult |
| ImageStar | CH | ReachabilityResult, CounterExampleResult |
Hyperrectangle)Corresponds to a high-dimensional rectangle, defined by
\[|x-c| \le r,\]
where $c\in\mathbb{R}^{k_0}$ is the center of the hyperrectangle and $r\in\mathbb{R}^{k_0}$ is the radius of the hyperrectangle.
HalfSpace)Represented by a single linear inequality constraint
\[a^\top x \le b,\]
where $a\in\mathbb{R}^{k_0}$ and $b\in\mathbb{R}$.
HPolytope)HPolytope uses a set of linear inequality constraints to represent a convex polytope, i.e., it is a bounded set defined using an intersection of half-spaces.
\[Ax \le b,\]
where $A\in\mathbb{R}^{k\times k_0}, b\in\mathbb{R}^k$ with $k$ representing the number of inequality constraints.
Star)Only convex star set is considered in this toolbox. A convex star set is an affine transformation of an arbitrary convex polytope,
\[x = c + \begin{bmatrix} r_1 & r_2 & \cdots & r_l \end{bmatrix} \alpha,\; C\alpha \le d,\]
where $c\in\mathbb{R}^{k_0}$ is the center of the star set, $r_i\in\mathbb{R}^{k_0},\; i\in\{1,\dots,l\}$ are generators of the star set, $C\in\mathbb{R}^{k\times l}$, $d\in\mathbb{R}^{k}$, $\alpha\in\mathbb{R}^l$ is the free parameter that belongs to a unit hypercube, and $k$ is the number of inequality constraints on $\alpha$. $l$ is the degree of freedom of the star set.
The general starset, on the left, is not necessarily convex. We only consider convex starsets.
Zonotope)Zonotope is basically as star set in which all predicate variables are in the range of $[-1, 1]$. Zonotope represents polytopes that can be written as affine transformations of a unit hypercube, defined as
\[x = c + \begin{bmatrix} r_1 & r_2 & \cdots & r_l \end{bmatrix} \alpha,\; |\alpha| \le 1,\]
where $c\in\mathbb{R}^{k_0}$ is the center of the zonotope, $r_i\in\mathbb{R}^{k_0},\; i\in\{1,\dots,l\}$ are generators of the zonotope, and $\alpha\in\mathbb{R}^l$ is the free parameter that belongs to a unit hypercube. $l$ is the degree of freedom of the zonotope.
ImageStar is an extension of the star set where the center and generators are images with multiple channels.
\[x = c + \begin{bmatrix} r_1 & r_2 & \cdots & r_l \end{bmatrix} \alpha,\; C\alpha \le d,\]
where $c\in\mathbb{R}^{h\times w \times k_0}$ is the center image, $r_i\in\mathbb{R}^{h \times w \times k_0},\; i\in\{1,\dots,l\}$ are the generator iamges, $C\in\mathbb{R}^{k\times l}$, $d\in\mathbb{R}^{k}$, and $h,w,k$ are the height, width, and number of channels (input dimension) of the images respectively. $\alpha\in\mathbb{R}^l$ is the free parameter that belongs to a unit hypercube, and $k$ is the number of inequality constraints on $\alpha$. $l$ is the degree of freedom of the star set.
ImageZono is an extension of the zonotope where the center and generators are images with multiple channels.
\[x = c + \begin{bmatrix} r_1 & r_2 & \cdots & r_l \end{bmatrix} \alpha\]
where $c\in\mathbb{R}^{h\times w \times k_0}$ is the center image, $r_i\in\mathbb{R}^{h \times w \times k_0},\; i\in\{1,\dots,l\}$ are the generator iamges, and $h,w,k$ are the height, width, and number of channels (input dimension) of the images respectively. $\alpha\in\mathbb{R}^l$ is the free parameter that belongs to a unit hypercube and $l$ is the degree of freedom of the zonotope.
Complement)PolytopeComplement is a type that represents the complement of a polytope, that is the set
\[Y = X^c = \{ y\in\mathbb{R}^n : y \notin X \}.\]
[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] 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), 2018.
[3] M. Forets and C. Schilling, "LazySets.jl: Scalable Symbolic-Numeric Set Computations," in Proceeds of the JuliaCon Conferences, 2021.
[4] HD. Tran, S. Bak, W. Xiang, and T.T. Johnson, "Verification of Deep Convolutional Neural Networks Using ImageStars," in Computer Aided Verification (CAV), 2020.
SpecModelVerification.Spec — TypeSpecAbstract super-type for input-output specifications.
ModelVerification.InputSpec — TypeInputSpecInput specification can be of any type supported by LazySet or ImageConvexHull.
ModelVerification.OutputSpec — TypeOutputSpecOutput specification can be of any type supported by LazySet or LinearSpec.
The following are structures for specifications and construction functions for specifications.
ModelVerification.LinearSpec — TypeLinearSpec <: SpecSafety specification defined as the set $\{ x: x = A x - b ≤ 0 \}$.
Fields
A (AbstractArray{Float64, 3}): Normal dierction of size spec_dim x out_dim x batch_size.b (AbstractArray{Float64, 2}): Constraints of size spec_dim x batch_size.is_complement (Bool): Boolean flag for whether this specification is a complement or not.ModelVerification.get_linear_spec — Methodget_linear_spec(batch_out_set::AbstractVector)Retrieves the linear specifications of the batch of output sets and returns a LinearSpec structure.
Arguments
batch_out_set (AbstractVector): Batch of output sets.Returns
LinearSpec of the batch of output sets.ModelVerification.ReLUConstraints — TypeReLUConstraintsA mutable structure for storing information related to the constraints of a ReLU (Rectified Linear Unit) activation function in a neural network.
Fields
idx_list: A list of indices. val_list: A list of values corresponding to the indices in idx_list. not_splitted_mask: A mask indicating which elements in idx_list and val_list have not been split. This is used in the context of a piecewise linear approximation of the ReLU function, where the input space is split into regions where the function is linear.history_split: A record of the splits that have been performed. ModelVerification.ReLUConstrainedDomain — TypeReLUConstrainedDomain <: SpecA mutable structure for storing specifications related to the ReLU (Rectified Linear Unit) activation function in a neural network.
Fields
domain: A geometric specification representing the domain of the ReLU function.all_relu_cons: A dictionary of ReLU constraints for each node in the network.ModelVerification.ImageConvexHull — TypeImageConvexHull <: SpecConvex hull for images used to specify safety property for images. It is the smallest convex polytope that contains all the images given in the imgs array.
Fields
imgs (AbstractArray): List of images in AbstractArray. Image is represented as a matrix of height x weight x channels.ModelVerification.ImageLinfBall — TypeImageLinfBallA mutable structure for storing information related to the constraints of a L-infinity ball for images.
Fields
lb: Lower bound of the ball.ub: Upper bound of the ball.ModelVerification.get_image_linf_spec — Functionget_image_linf_spec(lb, ub, img_size)Given a lower bound lb, an upper bound ub, and the size of the image, returns a ImageZonoBound structure.
Arguments
lb: Lower bound of the image.ub: Upper bound of the image.img_size: Size of the image.Returns
ImageZonoBound structure.ModelVerification.classification_spec — Methodclassification_spec(n::Int64, target::Int64)Generates an output specification constructed with a convex polyhedron, HPolyhedron, for classification tasks. Given n-number of labels with target as the correct label, the resulting polyhedron is the finite intersection of halfspaces:
$P = \bigcap_{i=1}^n H_i$
where $H_i = \{x : a_i^T x \leq 0 \}, \; i\in\{1:n\}$ is a halfspace, $a_i$ is a row vector where the n-th element is 1.0, the target-th element is -1.0, and the rest are 0's.
Arguments
n (Int64): Number of labels.target (Int64): Target label.Returns
HPolyhedron specified as above such that the output specification captures the target label.The following are helper functions for retrieving information the specification structures.
ModelVerification.get_size — Methodget_size(input_spec::LazySet)Given a LazySet, it determines the size of the set.
ModelVerification.get_size — Methodget_size(input_spec::ImageConvexHull)Given an ImageConvexHull, it determines the size of the image.
ModelVerification.get_shape — Methodget_shape(input::ImageConvexHull)Returns the shape of the given ImageConvexHull input set.
Arguments
input (ImageConvexHull): Input set.Returns
shape (Tuple): Shape of the input set. The last dimension is always the number of the images. The first dimensions are the shape of the image. For example, if the input set is consisted of 10 images of size 128 x 128, then the shape is (128, 128, 10).ModelVerification.get_shape — Methodget_shape(input::Hyperrectangle)Returns the shape of the given Hyperrectangle input set.
Arguments
input (Hyperrectangle): Input set.Returns
shape (Tuple): Shape of the hyperrectangle. The last dimension is always (2, 1).The following are helper functions for modifying (scaling) the specification structures.
ModelVerification.scale_set — Methodscale_set(set::Hyperrectangle, ratio)Scale the hyperrectangle set by the given ratio. The center of the set is not changed, but the radius is scaled by the ratio.
Arguments
set (Hyperrectangle): The set to be scaled.ratio (Real): The ratio to scale the set by.Returns
Hyperrectangle set.ModelVerification.scale_set — Methodscale_set(set::ImageConvexHull, ratio)Scale the image convex hull set by the given ratio. The first image is not changed, but the rest of the images are scaled by the ratio. The first image is not changed because it acts as the "center" of the set.
Arguments
set (ImageConvexHull): The set to be scaled.ratio (Real): The ratio to scale the set by.Returns
ImageConvexHull set.Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
A safety property is essentially an input-output relationship for the model we want to verify. In general, the constraints for the input set $\mathcal{X}$ and the output set $\mathcal{Y}$ can have any geometry. For the sake of simplicity, ModelVerification.jl uses convex polytopes and the complement of a polytope to encode the input and output specifications. Specifically, our implementation utilizes the geometric definitions of LazySets, a Julia package for calculus with convex sets. The following section dives into the geometric representations ModelVerification.jl uses and the representations required for each solver.
Different solvers implemented in ModelVerification.jl require the input-output specification formulated with particular geometries. We report here a brief overview of the sets we use. For specifics, please read Algorithms for Verifying Deep Neural Networks by C. Liu, et al. and Sets in LazySets.jl.
HyperrectangleHalfSpaceHPolytopeStarSetImageStarZonotopePolytopeComplementConvexHull| Solver | Input set | Output |
|---|---|---|
| Ai2 | ZT,SS,HP,HR | ReachabilityResult, CounterExampleResult |
| CROWN | ZT,SS,HP,HR,CH | BasicResult |
| $\alpha$-CROWN | ZT,SS,HP,HR,CH | BasicResult |
| $\beta$-CROWN | ZT,SS,HP,HR,CH | BasicResult |
| $\alpha$-$\beta$-CROWN | ZT,SS,HP,HR,CH | BasicResult |
| ImageZono | CH | ReachabilityResult, CounterExampleResult |
| ImageStar | CH | ReachabilityResult, CounterExampleResult |
Hyperrectangle)Corresponds to a high-dimensional rectangle, defined by
\[|x-c| \le r,\]
where $c\in\mathbb{R}^{k_0}$ is the center of the hyperrectangle and $r\in\mathbb{R}^{k_0}$ is the radius of the hyperrectangle.
HalfSpace)Represented by a single linear inequality constraint
\[a^\top x \le b,\]
where $a\in\mathbb{R}^{k_0}$ and $b\in\mathbb{R}$.
HPolytope)HPolytope uses a set of linear inequality constraints to represent a convex polytope, i.e., it is a bounded set defined using an intersection of half-spaces.
\[Ax \le b,\]
where $A\in\mathbb{R}^{k\times k_0}, b\in\mathbb{R}^k$ with $k$ representing the number of inequality constraints.
Star)Only convex star set is considered in this toolbox. A convex star set is an affine transformation of an arbitrary convex polytope,
\[x = c + \begin{bmatrix} r_1 & r_2 & \cdots & r_l \end{bmatrix} \alpha,\; C\alpha \le d,\]
where $c\in\mathbb{R}^{k_0}$ is the center of the star set, $r_i\in\mathbb{R}^{k_0},\; i\in\{1,\dots,l\}$ are generators of the star set, $C\in\mathbb{R}^{k\times l}$, $d\in\mathbb{R}^{k}$, $\alpha\in\mathbb{R}^l$ is the free parameter that belongs to a unit hypercube, and $k$ is the number of inequality constraints on $\alpha$. $l$ is the degree of freedom of the star set.
The general starset, on the left, is not necessarily convex. We only consider convex starsets.
Zonotope)Zonotope is basically as star set in which all predicate variables are in the range of $[-1, 1]$. Zonotope represents polytopes that can be written as affine transformations of a unit hypercube, defined as
\[x = c + \begin{bmatrix} r_1 & r_2 & \cdots & r_l \end{bmatrix} \alpha,\; |\alpha| \le 1,\]
where $c\in\mathbb{R}^{k_0}$ is the center of the zonotope, $r_i\in\mathbb{R}^{k_0},\; i\in\{1,\dots,l\}$ are generators of the zonotope, and $\alpha\in\mathbb{R}^l$ is the free parameter that belongs to a unit hypercube. $l$ is the degree of freedom of the zonotope.
ImageStar is an extension of the star set where the center and generators are images with multiple channels.
\[x = c + \begin{bmatrix} r_1 & r_2 & \cdots & r_l \end{bmatrix} \alpha,\; C\alpha \le d,\]
where $c\in\mathbb{R}^{h\times w \times k_0}$ is the center image, $r_i\in\mathbb{R}^{h \times w \times k_0},\; i\in\{1,\dots,l\}$ are the generator iamges, $C\in\mathbb{R}^{k\times l}$, $d\in\mathbb{R}^{k}$, and $h,w,k$ are the height, width, and number of channels (input dimension) of the images respectively. $\alpha\in\mathbb{R}^l$ is the free parameter that belongs to a unit hypercube, and $k$ is the number of inequality constraints on $\alpha$. $l$ is the degree of freedom of the star set.
ImageZono is an extension of the zonotope where the center and generators are images with multiple channels.
\[x = c + \begin{bmatrix} r_1 & r_2 & \cdots & r_l \end{bmatrix} \alpha\]
where $c\in\mathbb{R}^{h\times w \times k_0}$ is the center image, $r_i\in\mathbb{R}^{h \times w \times k_0},\; i\in\{1,\dots,l\}$ are the generator iamges, and $h,w,k$ are the height, width, and number of channels (input dimension) of the images respectively. $\alpha\in\mathbb{R}^l$ is the free parameter that belongs to a unit hypercube and $l$ is the degree of freedom of the zonotope.
Complement)PolytopeComplement is a type that represents the complement of a polytope, that is the set
\[Y = X^c = \{ y\in\mathbb{R}^n : y \notin X \}.\]
[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] 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), 2018.
[3] M. Forets and C. Schilling, "LazySets.jl: Scalable Symbolic-Numeric Set Computations," in Proceeds of the JuliaCon Conferences, 2021.
[4] HD. Tran, S. Bak, W. Xiang, and T.T. Johnson, "Verification of Deep Convolutional Neural Networks Using ImageStars," in Computer Aided Verification (CAV), 2020.
SpecModelVerification.Spec — TypeSpecAbstract super-type for input-output specifications.
ModelVerification.InputSpec — TypeInputSpecInput specification can be of any type supported by LazySet or ImageConvexHull.
ModelVerification.OutputSpec — TypeOutputSpecOutput specification can be of any type supported by LazySet or LinearSpec.
The following are structures for specifications and construction functions for specifications.
ModelVerification.LinearSpec — TypeLinearSpec <: SpecSafety specification defined as the set $\{ x: x = A x - b ≤ 0 \}$.
Fields
A (AbstractArray{FloatType[], 3}): Normal dierction of size spec_dim x out_dim x batch_size.b (AbstractArray{FloatType[], 2}): Constraints of size spec_dim x batch_size.is_complement (Bool): Boolean flag for whether this specification is a complement or not.ModelVerification.get_linear_spec — Methodget_linear_spec(batch_out_set::AbstractVector)Retrieves the linear specifications of the batch of output sets and returns a LinearSpec structure.
Arguments
batch_out_set (AbstractVector): Batch of output sets.Returns
LinearSpec of the batch of output sets.ModelVerification.ReLUConstraints — TypeReLUConstraintsA mutable structure for storing information related to the constraints of a ReLU (Rectified Linear Unit) activation function in a neural network.
Fields
idx_list: A list of indices. val_list: A list of values corresponding to the indices in idx_list. not_splitted_mask: A mask indicating which elements in idx_list and val_list have not been split. This is used in the context of a piecewise linear approximation of the ReLU function, where the input space is split into regions where the function is linear.history_split: A record of the splits that have been performed. ModelVerification.ReLUConstrainedDomain — TypeReLUConstrainedDomain <: SpecA mutable structure for storing specifications related to the ReLU (Rectified Linear Unit) activation function in a neural network.
Fields
domain: A geometric specification representing the domain of the ReLU function.all_relu_cons: A dictionary of ReLU constraints for each node in the network.ModelVerification.ImageConvexHull — TypeImageConvexHull <: SpecConvex hull for images used to specify safety property for images. It is the smallest convex polytope that contains all the images given in the imgs array.
Fields
imgs (AbstractArray): List of images in AbstractArray. Image is represented as a matrix of height x weight x channels.ModelVerification.ImageLinfBall — TypeImageLinfBallA mutable structure for storing information related to the constraints of a L-infinity ball for images.
Fields
lb: Lower bound of the ball.ub: Upper bound of the ball.Missing docstring for get_image_linf_spec. Check Documenter's build log for details.
ModelVerification.classification_spec — Methodclassification_spec(n::Int64, target::Int64)Generates an output specification constructed with a convex polyhedron, HPolyhedron, for classification tasks. Given n-number of labels with target as the correct label, the resulting polyhedron is the finite intersection of halfspaces:
$P = \bigcap_{i=1}^n H_i$
where $H_i = \{x : a_i^T x \leq 0 \}, \; i\in\{1:n\}$ is a halfspace, $a_i$ is a row vector where the n-th element is 1.0, the target-th element is -1.0, and the rest are 0's.
Arguments
n (Int64): Number of labels.target (Int64): Target label.Returns
HPolyhedron specified as above such that the output specification captures the target label.The following are helper functions for retrieving information the specification structures.
ModelVerification.get_size — Methodget_size(input_spec::LazySet)Given a LazySet, it determines the size of the set.
ModelVerification.get_size — Methodget_size(input_spec::ImageConvexHull)Given an ImageConvexHull, it determines the size of the image.
ModelVerification.get_shape — Methodget_shape(input::ImageConvexHull)Returns the shape of the given ImageConvexHull input set.
Arguments
input (ImageConvexHull): Input set.Returns
shape (Tuple): Shape of the input set. The last dimension is always the number of the images. The first dimensions are the shape of the image. For example, if the input set is consisted of 10 images of size 128 x 128, then the shape is (128, 128, 10).ModelVerification.get_shape — Methodget_shape(input::Hyperrectangle)Returns the shape of the given Hyperrectangle input set.
Arguments
input (Hyperrectangle): Input set.Returns
shape (Tuple): Shape of the hyperrectangle. The last dimension is always (2, 1).The following are helper functions for modifying (scaling) the specification structures.
ModelVerification.scale_set — Methodscale_set(set::Hyperrectangle, ratio)Scale the hyperrectangle set by the given ratio. The center of the set is not changed, but the radius is scaled by the ratio.
Arguments
set (Hyperrectangle): The set to be scaled.ratio (Real): The ratio to scale the set by.Returns
Hyperrectangle set.ModelVerification.scale_set — Methodscale_set(set::ImageConvexHull, ratio)Scale the image convex hull set by the given ratio. The first image is not changed, but the rest of the images are scaled by the ratio. The first image is not changed because it acts as the "center" of the set.
Arguments
set (ImageConvexHull): The set to be scaled.ratio (Real): The ratio to scale the set by.Returns
ImageConvexHull set.Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
For most of the functions below, each solver has a unique dispatch defined.
All the solvers are based on one of the following propagation methods.
ModelVerification.PropMethod — TypePropMethodAlgorithm 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.
ModelVerification.ForwardProp — TypeForwardProp <: PropMethodAbstract type representing solvers that use forward propagation.
ModelVerification.BackwardProp — TypeBackwardProp <: PropMethodAbstract type representing solvers that use backward propagation.
ModelVerification.SequentialForwardProp — TypeSequentialForwardProp <: ForwardPropModelVerification.SequentialBackwardProp — TypeSequentialBackwardProp <: ForwardPropModelVerification.BatchForwardProp — TypeBatchForwardProp <: ForwardPropModelVerification.BatchBackwardProp — TypeBatchBackwardProp <: BackwardPropThe bounds are based on the following abstract type Bound.
ModelVerification.Bound — TypeBoundAbstract type representing bounds.
prepare_method is the first step called in search_branches. It initializes the bounds of the start node of the computational graph based on the given branch and the geometric representation used by the solver, which is specified with the prop_method. For each solver, there is a unique prepare_method defined. For more information, refer to the documentation for each solver.
ModelVerification.prepare_method — Methodprepare_method(prop_method::PropMethod, batch_input::AbstractVector, batch_output::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.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.The following functions are used to retrieve information regarding each node in the model.
ModelVerification.init_propagation — Methodinit_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.ModelVerification.init_propagation — Methodinit_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.The following functions are used to either retrieve or process the safety specification.
ModelVerification.init_batch_bound — Methodinit_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
ModelVerification.init_batch_bound — Methodinit_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
ModelVerification.init_bound — Methodinit_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.ModelVerification.init_bound — Methodinit_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.ModelVerification.process_bound — Functionprocess_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.process_bound(prop_method::BetaCrown, batch_bound::BetaCrownBound, batch_out_spec, model_info, batch_info)ModelVerification.check_inclusion — Methodcheck_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.ModelVerification.ExactReach — TypeExactReach <: SequentialForwardPropExactReach 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
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.
ModelVerification.ExactReachBound — TypeExactReachBound <: BoundBound for ExactReach solver. It is a union of polytopes, represented with an array of LazySet.
Fields
polys (AbstractArray{LazySet}): Array of polytopes.ModelVerification.center — Methodcenter(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
ModelVerification.prepare_problem — Methodprepare_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.ModelVerification.init_bound — Methodinit_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.ModelVerification.check_inclusion — Methodcheck_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.ModelVerification.Ai2 — TypeAi2{T<:Union{Hyperrectangle, Zonotope, HPolytope, Star}}
+Solvers · ModelVerification.jl Solvers
For most of the functions below, each solver has a unique dispatch defined.
Variations of propagation methods
All the solvers are based on one of the following propagation methods.
ModelVerification.PropMethod — TypePropMethod
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.
sourceModelVerification.ForwardProp — TypeForwardProp <: PropMethod
Abstract type representing solvers that use forward propagation.
sourceModelVerification.BackwardProp — TypeBackwardProp <: PropMethod
Abstract type representing solvers that use backward propagation.
sourceModelVerification.SequentialForwardProp — TypeSequentialForwardProp <: ForwardProp
sourceModelVerification.SequentialBackwardProp — TypeSequentialBackwardProp <: ForwardProp
sourceModelVerification.BatchForwardProp — TypeBatchForwardProp <: ForwardProp
sourceModelVerification.BatchBackwardProp — TypeBatchBackwardProp <: BackwardProp
sourceBound types
The bounds are based on the following abstract type Bound.
ModelVerification.Bound — TypeBound
Abstract type representing bounds.
sourcePreprocessing for the solver
prepare_method is the first step called in search_branches. It initializes the bounds of the start node of the computational graph based on the given branch and the geometric representation used by the solver, which is specified with the prop_method. For each solver, there is a unique prepare_method defined. For more information, refer to the documentation for each solver.
Missing docstring. Missing docstring for prepare_method(prop_method::PropMethod, batch_input::AbstractVector, batch_output::AbstractVector, model_info). Check Documenter's build log for details.
The following functions are used to retrieve information regarding each node in the model.
ModelVerification.init_propagation — Methodinit_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.
sourceModelVerification.init_propagation — Methodinit_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.
sourceThe following functions are used to either retrieve or process the safety specification.
ModelVerification.init_batch_bound — Methodinit_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.
sourceModelVerification.init_batch_bound — Methodinit_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.
sourceModelVerification.init_bound — Methodinit_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.
sourceModelVerification.init_bound — Methodinit_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.
sourceModelVerification.process_bound — Functionprocess_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.
sourceChecking inclusion
ModelVerification.check_inclusion — Methodcheck_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.
sourceExactReach
ModelVerification.ExactReach — TypeExactReach <: 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
- Network: any depth, ReLU activation (more activations to be supported in the future)
- Input: Array of AbstractPolytope, i.e., union of polytopes.
- 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.
sourceModelVerification.ExactReachBound — TypeExactReachBound <: Bound
Bound for ExactReach solver. It is a union of polytopes, represented with an array of LazySet.
Fields
polys (AbstractArray{LazySet}): Array of polytopes.
sourceMissing docstring. Missing docstring for center(bound::ExactReachBound). Check Documenter's build log for details.
ModelVerification.prepare_problem — Methodprepare_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.
sourceModelVerification.init_bound — Methodinit_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.
sourceModelVerification.check_inclusion — Methodcheck_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.
sourceAi2
ModelVerification.Ai2 — TypeAi2{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
- Network: any depth, ReLU activation (more activations to be supported in the future)
- Input: AbstractPolytope
const Ai2h = Ai2{HPolytope}
const Ai2z = Ai2{Zonotope}
const Ai2s = Ai2{Star}
-const Box = Ai2{Hyperrectangle}
- 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),
sourceModelVerification.StarSet — TypeStarSet
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.
sourceModelVerification.prepare_method — Methodprepare_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.
sourceModelVerification.compute_bound — Methodcompute_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.
sourceModelVerification.compute_bound — Methodcompute_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.
sourceModelVerification.init_bound — Methodinit_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.
sourceModelVerification.check_inclusion — Methodcheck_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.
sourceModelVerification.check_inclusion — Methodcheck_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.
sourceImageStar
ModelVerification.ImageStar — TypeImageStar <: 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.
sourceModelVerification.ImageStarBound — TypeImageStarBound{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.
sourceModelVerification.prepare_problem — Methodprepare_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.
sourceModelVerification.prepare_method — Methodprepare_method(prop_method::ImageStar, batch_input::AbstractVector,
- batch_output::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.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.
sourceModelVerification.init_bound — Methodinit_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.
sourceModelVerification.assert_zono_star — Methodassert_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.
sourceModelVerification.compute_bound — Methodcompute_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.
sourceModelVerification.center — Methodcenter(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}.
sourceModelVerification.check_inclusion — Methodcheck_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.
sourceImageZono
ModelVerification.ImageZono — TypeImageZono <: 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.
sourceModelVerification.ImageZonoBound — TypeImageZonoBound{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.
sourceModelVerification.prepare_problem — Methodprepare_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.
sourceModelVerification.init_bound — Methodinit_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.
sourceModelVerification.init_bound — Methodinit_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.
sourceModelVerification.compute_bound — Methodcompute_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.
sourceModelVerification.center — Methodcenter(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}.
sourceModelVerification.check_inclusion — Methodcheck_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.
sourceCrown
ModelVerification.Crown — TypeCrown <: BatchForwardProp
sourceModelVerification.CrownBound — TypeCrownBound <: Bound
sourceModelVerification.ConcretizeCrownBound — TypeConcretizeCrownBound <: Bound
sourceModelVerification.prepare_problem — Methodprepare_problem(search_method::SearchMethod, split_method::SplitMethod,
- prop_method::Crown, problem::Problem)
sourceModelVerification.prepare_method — Methodprepare_method(prop_method::Crown, batch_input::AbstractVector,
- out_specs::LinearSpec, model_info)
sourceModelVerification.init_batch_bound — Methodinit_batch_bound(prop_method::Crown, batch_input::AbstractArray, out_specs)
sourceModelVerification.compute_bound — Methodcompute_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)
sourceModelVerification.compute_bound — Methodcompute_bound(bound::ConcretizeCrownBound)
sourceModelVerification.check_inclusion — Methodcheck_inclusion(prop_method::Crown, model, batch_input::AbstractArray, bound::CrownBound, batch_out_spec::LinearSpec)
source$\alpha$-Crown
$\beta$-Crown
ModelVerification.BetaCrown — TypeBetaCrown <: BatchBackwardProp
sourceModelVerification.BetaCrownBound — TypeBetaCrownBound <: Bound
sourceModelVerification.Compute_bound — TypeCompute_bound
sourceModelVerification.prepare_problem — Methodprepare_problem(search_method::SearchMethod, split_method::SplitMethod, prop_method::BetaCrown, problem::Problem)
sourceModelVerification.init_batch_bound — Methodinit_batch_bound(prop_method::BetaCrown, batch_input::AbstractArray, batch_output::LinearSpec)
sourceModelVerification.prepare_method — Methodprepare_method(prop_method::BetaCrown, batch_input::AbstractVector, batch_output::AbstractVector, model_info)
sourceModelVerification.prepare_method — Methodprepare_method(prop_method::BetaCrown, batch_input::AbstractVector, out_specs::LinearSpec, model_info)
sourceModelVerification.update_bound_by_relu_con — Methodupdate_bound_by_relu_con(node, batch_input, relu_input_lower, relu_input_upper)
sourceModelVerification.init_alpha — Methodinit_alpha(layer::typeof(relu), node, batch_info, batch_input)
sourceModelVerification.init_beta — Methodinitbeta(layer::typeof(relu), node, batchinfo, batch_input)
sourceModelVerification.init_A_b — Methodinit_A_b(n, batch_size) # A x < b
sourceModelVerification.init_bound — Methodinit_bound(prop_method::BetaCrown, input)
sourceModelVerification.optimize_model — Methodoptimize_model(model, input, loss_func, optimizer, max_iter)
sourceModelVerification.process_bound — Methodprocess_bound(prop_method::BetaCrown, batch_bound::BetaCrownBound, batch_out_spec, model_info, batch_info)
sourceModelVerification.get_pre_relu_A — Methodget_pre_relu_A(init, use_gpu, lower_or_upper, model_info, batch_info)
sourceModelVerification.get_pre_relu_spec_A — Methodget_pre_relu_spec_A(init, use_gpu, lower_or_upper, model_info, batch_info)
sourceModelVerification.check_inclusion — Methodcheck_inclusion(prop_method::BetaCrown, model, batch_input::AbstractArray, bound::ConcretizeCrownBound, batch_out_spec::LinearSpec)
sourceSettings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
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),
ModelVerification.StarSet — TypeStarSetCovers 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.Missing docstring for prepare_method(prop_method::StarSet, batch_input::AbstractVector, batch_output::AbstractVector, model_info). Check Documenter's build log for details.
ModelVerification.compute_bound — Methodcompute_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 computedReturns
ModelVerification.compute_bound — Methodcompute_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
ModelVerification.init_bound — Methodinit_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 setReturns
Star set that encompasses the given hyperrectangle.ModelVerification.check_inclusion — Methodcheck_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.ModelVerification.check_inclusion — Methodcheck_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.ModelVerification.ImageStar — TypeImageStar <: SequentialForwardPropImageStar 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.
ModelVerification.ImageStarBound — TypeImageStarBound{T<:Real} <: BoundImageStarBound 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.ModelVerification.prepare_problem — Methodprepare_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.Missing docstring for prepare_method(prop_method::ImageStar, batch_input::AbstractVector, batch_output::AbstractVector, model_info). Check Documenter's build log for details.
ModelVerification.init_bound — Methodinit_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.ModelVerification.assert_zono_star — Methodassert_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.
ModelVerification.compute_bound — Methodcompute_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
Missing docstring for center(bound::ImageStarBound). Check Documenter's build log for details.
ModelVerification.check_inclusion — Methodcheck_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.ModelVerification.ImageZono — TypeImageZono <: SequentialForwardPropImageZono 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.
ModelVerification.ImageZonoBound — TypeImageZonoBound{T<:Real} <: BoundImageZonoBound 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.ModelVerification.prepare_problem — Methodprepare_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.ModelVerification.init_bound — Methodinit_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.ModelVerification.init_bound — Methodinit_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.ModelVerification.compute_bound — Methodcompute_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
Missing docstring for center(bound::ImageZonoBound). Check Documenter's build log for details.
ModelVerification.check_inclusion — Methodcheck_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.ModelVerification.Crown — TypeCrown <: BatchForwardPropModelVerification.CrownBound — TypeCrownBound <: BoundModelVerification.ConcretizeCrownBound — TypeConcretizeCrownBound <: BoundModelVerification.prepare_problem — Methodprepare_problem(search_method::SearchMethod, split_method::SplitMethod,
+ prop_method::Crown, problem::Problem)Missing docstring for prepare_method(prop_method::Crown, batch_input::AbstractVector, out_specs::LinearSpec, model_info). Check Documenter's build log for details.
ModelVerification.init_batch_bound — Methodinit_batch_bound(prop_method::Crown, batch_input::AbstractArray, out_specs)ModelVerification.compute_bound — Methodcompute_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 objectOutputs:
(lbound, ubound)ModelVerification.compute_bound — Methodcompute_bound(bound::ConcretizeCrownBound)ModelVerification.check_inclusion — Methodcheck_inclusion(prop_method::Crown, model, batch_input::AbstractArray, bound::CrownBound, batch_out_spec::LinearSpec)ModelVerification.BetaCrown — TypeBetaCrown <: BatchBackwardPropModelVerification.BetaCrownBound — TypeBetaCrownBound <: BoundModelVerification.Compute_bound — TypeCompute_boundModelVerification.prepare_problem — Methodprepare_problem(search_method::SearchMethod, split_method::SplitMethod, prop_method::BetaCrown, problem::Problem)ModelVerification.init_batch_bound — Methodinit_batch_bound(prop_method::BetaCrown, batch_input::AbstractArray, batch_output::LinearSpec)Missing docstring for prepare_method(prop_method::BetaCrown, batch_input::AbstractVector, batch_output::AbstractVector, model_info). Check Documenter's build log for details.
Missing docstring for prepare_method(prop_method::BetaCrown, batch_input::AbstractVector, out_specs::LinearSpec, model_info). Check Documenter's build log for details.
ModelVerification.update_bound_by_relu_con — Methodupdate_bound_by_relu_con(node, batch_input, relu_input_lower, relu_input_upper)Missing docstring for init_alpha(layer::typeof(relu), node, batch_info, batch_input). Check Documenter's build log for details.
ModelVerification.init_beta — Methodinitbeta(layer::typeof(relu), node, batchinfo, batch_input)
ModelVerification.init_A_b — Methodinit_A_b(n, batch_size) # A x < bModelVerification.init_bound — Methodinit_bound(prop_method::BetaCrown, input)ModelVerification.optimize_model — Methodoptimize_model(model, input, loss_func, optimizer, max_iter)ModelVerification.process_bound — Methodprocess_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.ModelVerification.get_pre_relu_A — Methodget_pre_relu_A(init, use_gpu, lower_or_upper, model_info, batch_info)ModelVerification.get_pre_relu_spec_A — Methodget_pre_relu_spec_A(init, use_gpu, lower_or_upper, model_info, batch_info)ModelVerification.check_inclusion — Methodcheck_inclusion(prop_method::BetaCrown, model, batch_input::AbstractArray, bound::ConcretizeCrownBound, batch_out_spec::LinearSpec)Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
Please note that this page is under construction.
This page serves to explain the overall flow of the toolbox. For examples and explanation on how to use specific verification functions, please refer to the tutorials.
In general, verification algorithms follow the paradigm of Branch and Bound. This process can be summarized into three steps:
Repeat or terminate the process based on the result.
ModelVerification.jl uses a modularized code structure to support various combinations of search methods, split methods, and solvers for a variety of neural network architectures and geometric representations for the safety specifications. After reading through this section, the user should have an overall idea of the flow of the toolbox and the design philosophy behind it. Thanks to the highly modularized structure of the toolbox, the user can add additional functionalities at any layer of the verification process.
Here, we define some terms that are unique to the toolbox or are used differently compared to the typical usage.
propagate.jl. This will be clearer in the following explanations.Let's first create an instance. An instance contains all the information required to run the verify function. This function does the heavy-lifting where the verification problem is solved. As long as the user properly defines the problem and solver methods, this is the only function the user has to call. To run verify, the user has to provide the following arguments. These collectively define an "instance":
SearchMethod: Algorithm for iterating through the branches, such as BFS (breadth-first search) and DFS (depth-first search).SplitMethod: Algorithm for splitting an unknown branch into smaller pieces for further refinement. This is also used in the first step of verify to populate the branches bank. In other words, it splits the input specification into branches to facilitate the propagation process.PropMethod: Solver used to verify the problem, such as Ai2 and Crown.Problem: Problem to be verified. It consists of a Network, and input and output specifications.This toolbox design choice allows for extensive customization of methods and solvers by defining different search or split methods. The user simply needs to add their chosen methods in the specific files (search.jl and split.jl), which the solvers will automatically use for the verification process.
SearchMethodSearchMethod describes the strategy the solver uses when iterating through the branches. Currently, ModelVerification.jl only supports Breath-first Search (BFS). The solver can exploit parallel analysis of the nodes in the BaB by indicating a batch_size is greater than 1.
SplitMethodSplitMethod specifies how many splits and where they are performed on a single node of the BaB. Depending on the SplitMethod, the solver will split either the input space or the ReLU nodes.
The following split methods are supported:
Bisect): splits either the input space or the ReLU nodes.BaBSR): splits the ReLU nodes.PropMethodPropMethod is the solver to be used for the verification.
The following solvers are supported:
ProblemProblem is composed by the model to be verified and the input & output specifications. Specifically, this part of the "instance" encodes what we want to verify rather than how we achieve the formal verification results.
verify is the main function called by ModelVerification.jl to start the verification process of the "instance" provided by the user.
ModelVerification.verify — Functionverify(searchmethod::SearchMethod, splitmethod::SplitMethod, propmethod::PropMethod, problem::Problem; timeout=86400, attackrestart=100, collectbound=false, summary=false, pre_split=nothing)
This is the main function for verification. It takes in a search method, a split method, a propagation method, and a problem, and returns a result. The result is of type ResultInfo, which is a wrapper for the following Result types: BasicResult, CounterExampleResult, AdversarialResult, ReachabilityResult, EnumerationResult, or timeout. For each Result, the status field is either :violated, :verified, or :unknown. Optional arguments can be passed to the function to control the timeout, the number of restarts for the attack, whether to collect the bounds for each branch, whether to print a summary of the verification process, and whether to pre-split the problem.
Arguments
search_method (SearchMethod): The search method, such as BFS, used to search through the branches.split_method (SplitMethod): The split method, such as Bisect, used to split the branches.prop_method (PropMethod): The propagation method, such as Ai2, used to propagate the constraints.problem (Problem): The problem to be verified - consists of a network, input set, and output set.time_out (Int): The timeout in seconds. Defaults to 86400 seconds, or 24 hours. If the timeout is reached, the function returns :timeout.attack_restart (Int): The number of restarts for the attack. Defaults to 100.collect_bound (Bool): Whether to collect the bounds for each branch.summary (Bool): Whether to print a summary of the verification process.pre_split: A function that takes in a Problem and returns a Problem with the input set pre-split. Defaults to nothing.search_adv_bound (Bool): Whether to search the maximal input bound that can pass the verification (get :holds) with the given setting.Returns
ResultInfo, the status field is either :violated, :verified, :unknown, or :timeout. The info is a dictionary that contains other information.prepare_problemThe first step of verify is prepare_problem which preprocesses the Problem into a form that is compatible with the verification solver. Its main two functionalities are:
model_info,init_bound function which returns the geometry representation that matches the solver requirements. For instance, since CROWN is a backward propagation method, the init_bound function returns the geometry used to encode the output specification. The result of prepare_problem are two variables:
model_info: structure that contains information about the Flux model,prepared_problem: Problem with a processed input-output specification.search_branchesModelVerification.search_branches — Methodsearch_branches(search_method::BFS, split_method, prop_method,
- problem, model_info)Searches through the branches in the branch bank, branches, until the branch bank is empty or time out. In each iteration (up to search_method.max_iter), a batch of unverified branches will be extracted from the branch bank. Then, the following is performed to verify the model:
prepare_method initializes the bound of the start node of the computational graph based on the geometric representation and corresponding solver.
propagate propagates the bound from the start node to the end node of the computational graph.
process_bound processes the bounds resulting from the propagation accordingly to the solver, prop_method. For example, for Ai2-based methods, process_bound simply returns the bounds from the propagate step. However, for Crown-based methods, process_bound post-processes the bounds.
check_inclusion decides whether the bound of the end node, the reachable set, satisfies the output specification or not. 1. If not, i.e., :violated, then the counterexample is returned and the verification process terminates. 2. If yes, i.e., :holds, then the current branch is verified and the function starts Step 1 again for the next branch, if any. 3. If unknown, i.e., :unknown, further refinement of the problem is preformed using split_branch, which divides the current branch into smaller pieces and puts them into the branch bank for further verification. Such :unknown status results due to the overapproximation introduced in the verification process.
If the branch bank is empty after going through search_method.max_iter number of verification procedures, the model is verified to be valid and returns :holds. If the branch bank is not empty, the function returns :unknown.
Arguments
search_method (BFS): Breadth-first Search method for iteratively going through the branches.split_method: Method for splitting the branches when further refinement is needed. This inclueds methods such as Bisect and BaBSR.prop_method: Propagation method used for the verification process. This is one of the solvers used to verify the given model.problem: Problem definition for model verification.model_info: Structure containing the information of the neural network to be verified.collect_bound(optional): Default is false, whether return the verified bound.pre_split(optional): nothing, the number of split before any propagation. This is particularly useful for large input set that could lead to memory overflow.Returns
BasicResult(:holds) if all the reachable sets are within the corresponding output specifications in the batch.BasicResult(:unknown) if the function failed to make a firm decision within the given time. This is due to the overapproximation introduced in the verification process.CounterExampleResult(:violated, x) if a reachable set is not within the corresponding output specification and there is a counterexample found.ModelVerification.advance_split — Methodadvancesplit(maxiter::Int, searchmethod::BFS, splitmethod, propmethod, problem, modelinfo)
Performs the splitting of the branches in the branch bank, branches, for a max_iter number of times. This is used in the search_branches function as serves as the first step of the verification process: populating the branches bank with initial branches.
Arguments
max_iter (Int): Maximum number of iterations to split the input specification.search_method (BFS): Breadth-first Search method for iteratively going through the branches.split_method: Method for splitting the branches for the initial population of the branch bank. This inclueds methods such as Bisect.prop_method: Propagation method used for the verification process. This is one of the solvers used to verify the given model.problem: Problem definition for model verification. Include the model and input and output specifications.model_info: Structure containing the information of the neural network to be verified.Returns
branches: Array of branches to be verified, split from the initial input specification.search_branches is the core function used for the verification process. It consists of several subfunctions that we are going to summarize in the following. At first, the function initializes the branch bank for the entire safety property's input-output domain. This can be done by advance_split, which splits the input-output domain using the given split method. Thus, each "branch" is a subpart of the input-output domain. The function seeks to verify all the branches and if it cannot provide a result (i.e., we obtain an :unknown answer), the function proceeds to split branch for a more refined verification process.. If the function verifies all the branches within the given maximum number of iterations, then we obtain a :holds answer. If the function finds any branch that does not satisfy the safety property, then it returns :violated.
For each iteration, i.e., for each branch, the function calls the following subfunctions to verify the branch:
prepare_method: this function retrieves all the information to perform either the forward or backward propagation of the input domain of the branch. The result is stored in two variables called batch_out_spec, batch_info, which contain the batch of the outputs and a dictionary containing all the information of each node in the model. prepare_method calls the following functions in sequence:
init_propagation: Differentiates between ForwardProp and BackwardProp. If the solver being used employs a forward propagation method, then we start propagating from the input nodes. If it employs a backward propagation method, then we start from the output nodes.init_batch_bound: Calls init_bound, which returns either the input or output geometry representation based on the type of propagation to perform.The result of the previous function is then used in the propagate function. This function propagates the starting bounds through the model using the specified propagation method, i.e., the solver. The propagate function acts as the overall logic for propagating the branch through the model and performs the propagation based on the layer operation (linear, ReLU, etc.) and the geometric representation for the bounds. The user can add additional layer operators in the propagate/operators folder. Moreover, the toolbox supports skip connections. The propagate function returns batch_bound, the bound of the output node, and an augmented batch_info dictionary with the output bound information added.
Now, process_bounds returns the reachable bounds obtained from the propagate function. Depending on the solver, the reachable bounds may be post-processed to optimized the verification procedure.
Finally, check_inclusion checks for the overlapping between the reachable bounds obtained from the propagation and the safety property's output bounds. Since we are using overapproximation of the output reachable set, the only case in which we can obtain :holds result is when the output reachable set is fully contained in the user-specified output set. On the other hand, the :violated result is only possible when the sets are completely disjoint. In all other cases, we have an :unknown answer and we proceed with the branch splitting method below to populate the branch bank.
split_branch is used to split the current branch with :unknown answer into two separate branches which are split based on the split_method. The sub-branches are then added to the "branches" bank.
We continue this loop until either get a :violated result, a :hold result for all the branches, or reach the maximum number of iterations.
search_adv_input_boundIf the verification result from verify is not :holds, i.e., either :unknown or :violated, then search_adv_input_bound searches for the maximul input bound that can pass the verification, i.e., retrieves :holds, with the given setting. This information is passed to the ResultInfo as a dictionary field so that the user can check.
ModelVerification.search_adv_input_bound — Functionsearch_adv_input_bound(search_method::SearchMethod,
+Flow · ModelVerification.jl Please note that this page is under construction.
Flow
This page serves to explain the overall flow of the toolbox. For examples and explanation on how to use specific verification functions, please refer to the tutorials.
In general, verification algorithms follow the paradigm of Branch and Bound. This process can be summarized into three steps:
- split the input set into smaller sets, which we call "branches",
- propagate the bound through the model for a given branch,
- check whether the bound of the final layer satisfies the output specificaiton.
Repeat or terminate the process based on the result.
ModelVerification.jl uses a modularized code structure to support various combinations of search methods, split methods, and solvers for a variety of neural network architectures and geometric representations for the safety specifications. After reading through this section, the user should have an overall idea of the flow of the toolbox and the design philosophy behind it. Thanks to the highly modularized structure of the toolbox, the user can add additional functionalities at any layer of the verification process.
Definition of Terms
Here, we define some terms that are unique to the toolbox or are used differently compared to the typical usage.
- Instance: combination of all the necessary information to define an "instance" of neural network verification problem. This is consisted of:
- Propagation Method: this is the bound propagation method used for verifying the problem. In other words, it is the choice of term to represent the "solver": all the solvers in ModelVerification.jl are represented as a propagation method. However, this is different from the methods in
propagate.jl. This will be clearer in the following explanations. - Model / (Deep) Neural Network / Network: these terms are used interchangeably and represent the deep neural network (DNN) to be verified.
- Node: (This is not equivalent to a "neuron" in a traditional deep learning sense.) This refers to a "node" in a computational-graph sense.
- Layer: (This is not equivalent to a "layer" in a traditional deep learning sense.) This refers to an operation at a node, such as ReLU activation function.
- BaB: "Branch-and-Bound" is a method that creates a binary tree for the search space where the verification is employed.
- Set vs Bound: One set is composed of bounds. E.g., for the output reachable set is a union of output bounds. But we use these terms interchangeably throughout the toolbox.
1. Creating an instance: what kind of verification problem do you want to solve?
Let's first create an instance. An instance contains all the information required to run the verify function. This function does the heavy-lifting where the verification problem is solved. As long as the user properly defines the problem and solver methods, this is the only function the user has to call. To run verify, the user has to provide the following arguments. These collectively define an "instance":
SearchMethod: Algorithm for iterating through the branches, such as BFS (breadth-first search) and DFS (depth-first search).SplitMethod: Algorithm for splitting an unknown branch into smaller pieces for further refinement. This is also used in the first step of verify to populate the branches bank. In other words, it splits the input specification into branches to facilitate the propagation process.PropMethod: Solver used to verify the problem, such as Ai2 and Crown.Problem: Problem to be verified. It consists of a Network, and input and output specifications.
This toolbox design choice allows for extensive customization of methods and solvers by defining different search or split methods. The user simply needs to add their chosen methods in the specific files (search.jl and split.jl), which the solvers will automatically use for the verification process.
SearchMethod
SearchMethod describes the strategy the solver uses when iterating through the branches. Currently, ModelVerification.jl only supports Breath-first Search (BFS). The solver can exploit parallel analysis of the nodes in the BaB by indicating a batch_size is greater than 1.
SplitMethod
SplitMethod specifies how many splits and where they are performed on a single node of the BaB. Depending on the SplitMethod, the solver will split either the input space or the ReLU nodes.
The following split methods are supported:
- Bisectection (
Bisect): splits either the input space or the ReLU nodes. - Branch-and-bound (
BaBSR): splits the ReLU nodes.
PropMethod
PropMethod is the solver to be used for the verification.
The following solvers are supported:
- ExactReach
- Ai2
- ImageStar
- ImageZono
- Crown
- Alpha-Crown
- Beta-Crown
Problem
Problem is composed by the model to be verified and the input & output specifications. Specifically, this part of the "instance" encodes what we want to verify rather than how we achieve the formal verification results.
- For information on how to load or convert models and how they are represented in ModelVerification.jl, please refer Network.
- For the different geometric representations for the input and output specifications, please refer Input-Output Specification.
2. Verifying the instance: spinning through the branches - where the magic happens!
verify is the main function called by ModelVerification.jl to start the verification process of the "instance" provided by the user.
ModelVerification.verify — Functionverify(searchmethod::SearchMethod, splitmethod::SplitMethod, propmethod::PropMethod, problem::Problem; timeout=86400, attackrestart=100, collectbound=false, summary=false, pre_split=nothing)
This is the main function for verification. It takes in a search method, a split method, a propagation method, and a problem, and returns a result. The result is of type ResultInfo, which is a wrapper for the following Result types: BasicResult, CounterExampleResult, AdversarialResult, ReachabilityResult, EnumerationResult, or timeout. For each Result, the status field is either :violated, :verified, or :unknown. Optional arguments can be passed to the function to control the timeout, the number of restarts for the attack, whether to collect the bounds for each branch, whether to print a summary of the verification process, and whether to pre-split the problem.
Arguments
search_method (SearchMethod): The search method, such as BFS, used to search through the branches.split_method (SplitMethod): The split method, such as Bisect, used to split the branches.prop_method (PropMethod): The propagation method, such as Ai2, used to propagate the constraints.problem (Problem): The problem to be verified - consists of a network, input set, and output set.time_out (Int): The timeout in seconds. Defaults to 86400 seconds, or 24 hours. If the timeout is reached, the function returns :timeout.attack_restart (Int): The number of restarts for the attack. Defaults to 100.collect_bound (Bool): Whether to collect the bounds for each branch.summary (Bool): Whether to print a summary of the verification process.pre_split: A function that takes in a Problem and returns a Problem with the input set pre-split. Defaults to nothing.search_adv_bound (Bool): Whether to search the maximal input bound that can pass the verification (get :holds) with the given setting.
Returns
- The result is
ResultInfo, the status field is either :violated, :verified, :unknown, or :timeout. The info is a dictionary that contains other information.
sourceprepare_problem
The first step of verify is prepare_problem which preprocesses the Problem into a form that is compatible with the verification solver. Its main two functionalities are:
- Retrieves the model information and stores it inside
model_info, - Exploits the
init_bound function which returns the geometry representation that matches the solver requirements. For instance, since CROWN is a backward propagation method, the init_bound function returns the geometry used to encode the output specification.
The result of prepare_problem are two variables:
model_info: structure that contains information about the Flux model,prepared_problem: Problem with a processed input-output specification.
search_branches
Missing docstring. Missing docstring for search_branches(search_method::BFS, split_method, prop_method, problem, model_info; collect_bound=false, comp_verified_ratio=false, pre_split=nothing, verbose=false, time_out=nothing). Check Documenter's build log for details.
search_branches is the core function used for the verification process. It consists of several subfunctions that we are going to summarize in the following. At first, the function initializes the branch bank for the entire safety property's input-output domain. This can be done by advance_split, which splits the input-output domain using the given split method. Thus, each "branch" is a subpart of the input-output domain. The function seeks to verify all the branches and if it cannot provide a result (i.e., we obtain an :unknown answer), the function proceeds to split branch for a more refined verification process.. If the function verifies all the branches within the given maximum number of iterations, then we obtain a :holds answer. If the function finds any branch that does not satisfy the safety property, then it returns :violated.
For each iteration, i.e., for each branch, the function calls the following subfunctions to verify the branch:
prepare_method: this function retrieves all the information to perform either the forward or backward propagation of the input domain of the branch. The result is stored in two variables called batch_out_spec, batch_info, which contain the batch of the outputs and a dictionary containing all the information of each node in the model. prepare_method calls the following functions in sequence:
init_propagation: Differentiates between ForwardProp and BackwardProp. If the solver being used employs a forward propagation method, then we start propagating from the input nodes. If it employs a backward propagation method, then we start from the output nodes.init_batch_bound: Calls init_bound, which returns either the input or output geometry representation based on the type of propagation to perform.
The result of the previous function is then used in the propagate function. This function propagates the starting bounds through the model using the specified propagation method, i.e., the solver. The propagate function acts as the overall logic for propagating the branch through the model and performs the propagation based on the layer operation (linear, ReLU, etc.) and the geometric representation for the bounds. The user can add additional layer operators in the propagate/operators folder. Moreover, the toolbox supports skip connections. The propagate function returns batch_bound, the bound of the output node, and an augmented batch_info dictionary with the output bound information added.
Now, process_bounds returns the reachable bounds obtained from the propagate function. Depending on the solver, the reachable bounds may be post-processed to optimized the verification procedure.
Finally, check_inclusion checks for the overlapping between the reachable bounds obtained from the propagation and the safety property's output bounds. Since we are using overapproximation of the output reachable set, the only case in which we can obtain :holds result is when the output reachable set is fully contained in the user-specified output set. On the other hand, the :violated result is only possible when the sets are completely disjoint. In all other cases, we have an :unknown answer and we proceed with the branch splitting method below to populate the branch bank.
split_branch is used to split the current branch with :unknown answer into two separate branches which are split based on the split_method. The sub-branches are then added to the "branches" bank.
We continue this loop until either get a :violated result, a :hold result for all the branches, or reach the maximum number of iterations.
search_adv_input_bound
If the verification result from verify is not :holds, i.e., either :unknown or :violated, then search_adv_input_bound searches for the maximul input bound that can pass the verification, i.e., retrieves :holds, with the given setting. This information is passed to the ResultInfo as a dictionary field so that the user can check.
ModelVerification.search_adv_input_bound — Functionsearch_adv_input_bound(search_method::SearchMethod,
split_method::SplitMethod,
prop_method::PropMethod,
problem::Problem;
- eps = 1e-3)
This function is used to search the maximal input bound that can pass the verification (get :holds) with the given setting. The search is done by binary search on the input bound that is scaled by the given ratio. This function is called in verify function when search_adv_bound is set to true and the initial verification result is :unknown or :violated.
Arguments
search_method (SearchMethod): The search method, such as BFS, used to search through the branches. split_method (SplitMethod): The split method, such as Bisect, used to split the branches.prop_method (PropMethod): The propagation method, such as Ai2, used to propagate the constraints.problem (Problem): The problem to be verified - consists of a network, input set, and output set.eps (Real): The precision of the binary search. Defaults to 1e-3.
Returns
- The maximal input bound that can pass the verification (get
:holds) with the given setting.
source3. Results and how to interpret them: so is my model good to go?
Once the verify function is over, it returns a ResultInfo that contains the status (either :hold, :violated, :unknown) and a dictionary that contains any other additional information needed to understand the verification results in detail, such as the verified bounds, adversarial input bounds, etc.
The following are the Result types used interally for the toolbox to differentiate between different verification results. The result is either a BasicResult, CounterExampleResult, AdversarialResult, ReachabilityResult, or EnumerationResult (to-be-supported). The status field is either :violated, :holds, or :unknown.
Output result Explanation [BasicResult::holds] The input-output constraint is always satisfied. [BasicResult::violated] The input-output constraint is violated, i.e., it exists a single point in the input constraint that violates the property. [BasicResult::unknown] Could not be determined if the property holds due to timeout in the computation. [CounterExampleResult] Like BasicResult, but also returns a counterexample if one is found (if status = :violated). The counterexample is a point in the input set that, after the NN, lies outside the output constraint set. [AdversarialResult] Like BasicResult, but also returns the maximum allowable disturbance in the input (if status = :violated). [ReachabilityResult] Like BasicResult, but also returns the output reachable set given the input constraint (if status = :violated). [EnumerationResult] Set of all the (un)safe regions in the safety property's domain.
For more information, please refer to Output (Verification Results).
Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
This function is used to search the maximal input bound that can pass the verification (get :holds) with the given setting. The search is done by binary search on the input bound that is scaled by the given ratio. This function is called in verify function when search_adv_bound is set to true and the initial verification result is :unknown or :violated.
Arguments
search_method (SearchMethod): The search method, such as BFS, used to search through the branches. split_method (SplitMethod): The split method, such as Bisect, used to split the branches.prop_method (PropMethod): The propagation method, such as Ai2, used to propagate the constraints.problem (Problem): The problem to be verified - consists of a network, input set, and output set.eps (Real): The precision of the binary search. Defaults to 1e-3. Returns
:holds) with the given setting.Once the verify function is over, it returns a ResultInfo that contains the status (either :hold, :violated, :unknown) and a dictionary that contains any other additional information needed to understand the verification results in detail, such as the verified bounds, adversarial input bounds, etc.
The following are the Result types used interally for the toolbox to differentiate between different verification results. The result is either a BasicResult, CounterExampleResult, AdversarialResult, ReachabilityResult, or EnumerationResult (to-be-supported). The status field is either :violated, :holds, or :unknown.
| Output result | Explanation |
|---|---|
[BasicResult::holds] | The input-output constraint is always satisfied. |
[BasicResult::violated] | The input-output constraint is violated, i.e., it exists a single point in the input constraint that violates the property. |
[BasicResult::unknown] | Could not be determined if the property holds due to timeout in the computation. |
[CounterExampleResult] | Like BasicResult, but also returns a counterexample if one is found (if status = :violated). The counterexample is a point in the input set that, after the NN, lies outside the output constraint set. |
[AdversarialResult] | Like BasicResult, but also returns the maximum allowable disturbance in the input (if status = :violated). |
[ReachabilityResult] | Like BasicResult, but also returns the output reachable set given the input constraint (if status = :violated). |
[EnumerationResult] | Set of all the (un)safe regions in the safety property's domain. |
For more information, please refer to Output (Verification Results).
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.
ModelVerification.network — Methodnetwork(c::Chain)Converts Flux.Chain to a Network.
Flux.Chain — MethodFlux.Chain(m::Network)Converts Network to a Flux.Chain.
Settings
This document was generated with Documenter.jl version 1.1.0 on Monday 11 December 2023. Using Julia version 1.9.3.
ModelVerification.network — Methodnetwork(c::Chain)Converts Flux.Chain to a Network.
Flux.Chain — MethodFlux.Chain(m::Network)Converts Network to a Flux.Chain.
Settings
This document was generated with Documenter.jl version 0.27.25 on Thursday 11 July 2024. Using Julia version 1.9.3.