GitHub

Branching

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 — Type
SearchMethod

Algorithm for iterating through the branches, such as BFS (breadth-first search) and DFS (depth-first search). For an example, see the documentation on BFS.

source
ModelVerification.BFS — Type
BFS <: SearchMethod

Breadth-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.
source

Split

ModelVerification.SplitMethod — Type
SplitMethod

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

source

Bisection

ModelVerification.Bisect — Type
Bisect <: SplitMethod

Bisection method for splitting branches.

Fields

  • num_split (Int64): Number of splits to be called.
source
ModelVerification.split_branch — Function

splitbranch(splitmethod::Bisect, model::Chain, input::Hyperrectangle, output, inheritance, modelinfo, batchinfo, 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

  • List of subtrees split from the input.
source
ModelVerification.split_branch — Function
split_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

  • List of subtrees split from the input.
source
ModelVerification.split_branch — Method
split_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.
source
ModelVerification.split_branch — Function
split_branch(split_method::Bisect, model::Chain, 
             input::ImageStarBound, output, inheritance, model_info, batch_info, ratio=nothing)

TO-BE-IMPLEMENTED

source
ModelVerification.split_branch — Function
split_branch(split_method::Bisect, model::Chain, input::ImageZonoBound, 
             output, inheritance, model_info, batch_info, ratio=nothing)
source
ModelVerification.split_interval — Method
split_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.
source

Branch-and-bound

ModelVerification.BaBSR — Type
BaBSR <: SplitMethod

Branch-and-Bound method for splitting branches.

Fields

  • num_split (Int64): Number of splits to be called.
source
ModelVerification.split_branch — Function
split_branch(split_method::BaBSR, model::Chain, 
             input::ReLUConstrainedDomain, output, inheritance, model_info, batch_info, ratio=nothing)

Split a set by adding ReLU activation status constraints. BaBSR analyzes which ReLU to split.

Arguments

  • split_method (BaBSR): a split algorithm
  • model (Chain): Model to be verified.
  • input (ReLUConstrainedDomain): Input specification with ReLU activation status constraints
  • 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

  • List of subtrees split from the input.
source

Input Gradient Split