From f607689fb43bbee5f6cb4746a4456a00b6e67c8b Mon Sep 17 00:00:00 2001 From: tomer arnon Date: Sat, 18 Jul 2020 23:02:39 +0300 Subject: [PATCH 1/7] automate calculating M --- src/optimization/nsVerify.jl | 31 ++++++++++++++++++++++++++----- src/utils/util.jl | 21 ++++++++++++--------- 2 files changed, 38 insertions(+), 14 deletions(-) diff --git a/src/optimization/nsVerify.jl b/src/optimization/nsVerify.jl index 17fb9413..71a748db 100644 --- a/src/optimization/nsVerify.jl +++ b/src/optimization/nsVerify.jl @@ -25,23 +25,44 @@ Sound and complete. """ @with_kw struct NSVerify <: Solver optimizer = GLPK.Optimizer - m::Float64 = 1000.0 # The big M in the linearization + m = nothing end function solve(solver::NSVerify, problem::Problem) + # Set M automatically if not already set. + if isnothing(solver.m) + M = set_automatic_M(problem) + else + @warn "M should be chosen carefully. An M which is too small will cause + the problem to be solved incorrectly. Not setting the `m` keyword, or setting + it equal to `nothing` will cause a safe value to be calculated automatically. + E.g. NSVerify()." maxlog = 1 + M = solver.m + end + + # Set up and solve the problem model = Model(solver) neurons = init_neurons(model, problem.network) deltas = init_deltas(model, problem.network) add_set_constraint!(model, problem.input, first(neurons)) add_complementary_set_constraint!(model, problem.output, last(neurons)) - encode_network!(model, problem.network, neurons, deltas, MixedIntegerLP(solver.m)) + encode_network!(model, problem.network, neurons, deltas, MixedIntegerLP(M)) feasibility_problem!(model) optimize!(model) + + if termination_status(model) == OPTIMAL return CounterExampleResult(:violated, value.(first(neurons))) - end - if termination_status(model) == INFEASIBLE + + elseif termination_status(model) == INFEASIBLE return CounterExampleResult(:holds) + else + return CounterExampleResult(:unknown) end - return CounterExampleResult(:unknown) end + +function set_automatic_M(problem) + # Compute the largest absolute value of + bounds = get_bounds(problem, false) + M = maximum(abs, Iterators.flatten(hr.center + hr.radius for hr in bounds)) +end \ No newline at end of file diff --git a/src/utils/util.jl b/src/utils/util.jl index a025222a..63800053 100644 --- a/src/utils/util.jl +++ b/src/utils/util.jl @@ -339,19 +339,22 @@ Return: - `Vector{Hyperrectangle}`: bounds for all nodes **after** activation. `bounds[1]` is the input set. """ function get_bounds(nnet::Network, input::Hyperrectangle, act::Bool = true) # NOTE there is another function by the same name in convDual. Should reconsider dispatch - if act - solver = MaxSens(0.0, true) - bounds = Vector{Hyperrectangle}(undef, length(nnet.layers) + 1) - bounds[1] = input + solver = MaxSens(0.0, true) + bounds = Vector{Hyperrectangle}(undef, length(nnet.layers) + 1) + bounds[1] = input + for (i, layer) in enumerate(nnet.layers) + bounds[i+1] = forward_layer(solver, layer, bounds[i]) + + end + if !act for (i, layer) in enumerate(nnet.layers) - bounds[i+1] = forward_layer(solver, layer, bounds[i]) + bounds[i+1] = approximate_affine_map(layer, bounds[i]) end - return bounds - else - error("before activation bounds not supported yet.") end + + return bounds end -get_bounds(problem::Problem) = get_bounds(problem.network, problem.input) +get_bounds(problem::Problem, args...) = get_bounds(problem.network, problem.input, args...) """ affine_map(layer, input::AbstractPolytope) From d392f0a8a5b39b4de3d0cf5cf10418ba399f8fc6 Mon Sep 17 00:00:00 2001 From: tomer arnon Date: Sat, 18 Jul 2020 23:04:40 +0300 Subject: [PATCH 2/7] whitespace --- src/utils/util.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/utils/util.jl b/src/utils/util.jl index 63800053..3e376828 100644 --- a/src/utils/util.jl +++ b/src/utils/util.jl @@ -344,8 +344,8 @@ function get_bounds(nnet::Network, input::Hyperrectangle, act::Bool = true) # NO bounds[1] = input for (i, layer) in enumerate(nnet.layers) bounds[i+1] = forward_layer(solver, layer, bounds[i]) - end + if !act for (i, layer) in enumerate(nnet.layers) bounds[i+1] = approximate_affine_map(layer, bounds[i]) From 137c03aef05e1ca191457dfc179e9a2706c130f9 Mon Sep 17 00:00:00 2001 From: tomerarnon Date: Sun, 19 Jul 2020 01:18:18 +0300 Subject: [PATCH 3/7] Update nsVerify.jl finish comment --- src/optimization/nsVerify.jl | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/optimization/nsVerify.jl b/src/optimization/nsVerify.jl index 71a748db..606aa626 100644 --- a/src/optimization/nsVerify.jl +++ b/src/optimization/nsVerify.jl @@ -62,7 +62,9 @@ function solve(solver::NSVerify, problem::Problem) end function set_automatic_M(problem) - # Compute the largest absolute value of + # Compute the largest pre-activation bound absolute value. + # M must be larger than any value a variable in the problem + # can take. bounds = get_bounds(problem, false) M = maximum(abs, Iterators.flatten(hr.center + hr.radius for hr in bounds)) -end \ No newline at end of file +end From fa8ae705afb9b43e8db2cffd4b82fb8e3b59bb1c Mon Sep 17 00:00:00 2001 From: liuchangliu Date: Sun, 19 Jul 2020 15:35:09 -0400 Subject: [PATCH 4/7] update MIP encoding using big M --- src/optimization/utils/constraints.jl | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/optimization/utils/constraints.jl b/src/optimization/utils/constraints.jl index 1fa60f26..8b38d0e0 100644 --- a/src/optimization/utils/constraints.jl +++ b/src/optimization/utils/constraints.jl @@ -184,8 +184,8 @@ function encode_layer!(MIP::MixedIntegerLP, @constraints(model, begin z_next[j] >= ẑ[j] z_next[j] >= 0.0 - z_next[j] <= ẑ[j] + m * δ[j] - z_next[j] <= m - m * δ[j] + z_next[j] <= ẑ[j] + m * (1 - δ[j]) + z_next[j] <= m * δ[j] end) end end From b7cbe6264df431eddcf1a2331d6d8d1f50819168 Mon Sep 17 00:00:00 2001 From: liuchangliu Date: Sun, 19 Jul 2020 16:07:25 -0400 Subject: [PATCH 5/7] modify get_bounds --- src/utils/util.jl | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/src/utils/util.jl b/src/utils/util.jl index 3e376828..fd11c3fe 100644 --- a/src/utils/util.jl +++ b/src/utils/util.jl @@ -339,19 +339,18 @@ Return: - `Vector{Hyperrectangle}`: bounds for all nodes **after** activation. `bounds[1]` is the input set. """ function get_bounds(nnet::Network, input::Hyperrectangle, act::Bool = true) # NOTE there is another function by the same name in convDual. Should reconsider dispatch - solver = MaxSens(0.0, true) bounds = Vector{Hyperrectangle}(undef, length(nnet.layers) + 1) bounds[1] = input + b = input for (i, layer) in enumerate(nnet.layers) - bounds[i+1] = forward_layer(solver, layer, bounds[i]) - end - - if !act - for (i, layer) in enumerate(nnet.layers) - bounds[i+1] = approximate_affine_map(layer, bounds[i]) + if act + b = approximate_affine_map(layer, bounds[i]) + bounds[i+1] = approximate_act_map(layer, b) + else + bounds[i+1] = approximate_affine_map(layer, b) + b = approximate_act_map(layer, bounds[i+1]) end end - return bounds end get_bounds(problem::Problem, args...) = get_bounds(problem.network, problem.input, args...) @@ -393,6 +392,22 @@ function approximate_affine_map(layer::Layer, input::Hyperrectangle) return Hyperrectangle(c, r) end +""" + approximate_act_map(layer, input::Hyperrectangle) + +Returns a Hyperrectangle overapproximation of the activation map of the input. +""" +function approximate_act_map(act::ActivationFunction, input::Hyperrectangle) + β = act.(input.center) + βmax = act.(high(input)) + βmin = act.(low(input)) + c = (βmax + βmin)/2 + r = (βmax - βmin)/2 + return Hyperrectangle(c, r) +end + +approximate_act_map(layer::Layer, input::Hyperrectangle) = approximate_act_map(layer.activation, input) + function translate(v::Vector, H::HPolytope) # translate each halfpsace according to: # a⋅(x-v) ≤ b ⟶ a⋅x ≤ b+a⋅v From 6edcf98bf7a7e711bf6c9c71046a33bd327aee33 Mon Sep 17 00:00:00 2001 From: tomer arnon Date: Mon, 20 Jul 2020 00:45:58 +0300 Subject: [PATCH 6/7] add abs to center since radius will always be positive --- src/optimization/nsVerify.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/optimization/nsVerify.jl b/src/optimization/nsVerify.jl index 606aa626..4ca610f9 100644 --- a/src/optimization/nsVerify.jl +++ b/src/optimization/nsVerify.jl @@ -66,5 +66,5 @@ function set_automatic_M(problem) # M must be larger than any value a variable in the problem # can take. bounds = get_bounds(problem, false) - M = maximum(abs, Iterators.flatten(hr.center + hr.radius for hr in bounds)) + M = maximum(abs, Iterators.flatten(abs.(hr.center) + hr.radius for hr in bounds)) end From 3f80d57f918e1768bdcd620783b42657444efc8f Mon Sep 17 00:00:00 2001 From: tomer arnon Date: Mon, 20 Jul 2020 00:49:13 +0300 Subject: [PATCH 7/7] update comments --- src/utils/util.jl | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/utils/util.jl b/src/utils/util.jl index fd11c3fe..b6e90ed9 100644 --- a/src/utils/util.jl +++ b/src/utils/util.jl @@ -331,12 +331,13 @@ end """ get_bounds(problem::Problem) - get_bounds(nnet::Network, input::Hyperrectangle) + get_bounds(nnet::Network, input::Hyperrectangle, [true]) This function calls maxSens to compute node-wise bounds given a input set. +The optional last argument determines whether the bounds are pre- or post-activation. Return: -- `Vector{Hyperrectangle}`: bounds for all nodes **after** activation. `bounds[1]` is the input set. +- `Vector{Hyperrectangle}`: bounds for all nodes. `bounds[1]` is the input set. """ function get_bounds(nnet::Network, input::Hyperrectangle, act::Bool = true) # NOTE there is another function by the same name in convDual. Should reconsider dispatch bounds = Vector{Hyperrectangle}(undef, length(nnet.layers) + 1) @@ -396,6 +397,7 @@ end approximate_act_map(layer, input::Hyperrectangle) Returns a Hyperrectangle overapproximation of the activation map of the input. +`act`must be monotonic. """ function approximate_act_map(act::ActivationFunction, input::Hyperrectangle) β = act.(input.center)