• Flow
• • 1. Creating an instance: what kind of verification problem do you want to solve?
  • 2. Verifying the instance: spinning through the branches - where the magic happens!
  • 3. Results and how to interpret them: so is my model good to go?

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:

1. split the input set into smaller sets, which we call "branches",
2. propagate the bound through the model for a given branch,
3. 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:
  • problem
  • solver
  • search methods
  • split methods
• 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.

prepare_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:

1. Retrieves the model information and stores it inside model_info,
2. 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:

1. model_info: structure that contains information about the Flux model,
2. prepared_problem: Problem with a processed input-output specification.

search_branches

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)

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:

1. 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.

2. 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.

3. 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.

4. 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.

5. 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.

search_adv_input_bound(search_method::SearchMethod, 
                       split_method::SplitMethod, 
                       prop_method::PropMethod, 
                       problem::Problem;
                       eps = 1e-3)

3. 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.

For more information, please refer to Output (Verification Results).