-
Notifications
You must be signed in to change notification settings - Fork 50
/
NeuralVerification.jl
98 lines (80 loc) · 2.41 KB
/
NeuralVerification.jl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
module NeuralVerification
using JuMP
using GLPK, SCS # SCS only needed for Certify
using PicoSAT # needed for Planet
using LazySets, LazySets.Approximations
using Polyhedra, CDDLib
using LinearAlgebra
using Parameters
using Interpolations # only for PiecewiseLinear
import LazySets: dim, HalfSpace # necessary to avoid conflict with Polyhedra
using Requires
abstract type Solver end
# For optimization methods:
import JuMP.MOI.OPTIMAL, JuMP.MOI.INFEASIBLE
JuMP.Model(solver::Solver) = Model(solver.optimizer)
JuMP.value(vars::Vector{VariableRef}) = value.(vars)
include("utils/activation.jl")
include("utils/network.jl")
include("utils/problem.jl")
include("utils/util.jl")
function __init__()
@require Flux="587475ba-b771-5e3f-ad9e-33799f191a9c" include("utils/flux.jl")
end
export
Solver,
Network,
AbstractActivation,
PolytopeComplement,
complement,
# NOTE: not sure if exporting these is a good idea as far as namespace conflicts go:
# ReLU,
# Max,
# Id,
GeneralAct,
PiecewiseLinear,
Problem,
Result,
BasicResult,
CounterExampleResult,
AdversarialResult,
ReachabilityResult,
read_nnet,
write_nnet,
solve,
forward_network,
check_inclusion
solve(m::Model; kwargs...) = JuMP.solve(m; kwargs...)
export solve
# TODO: consider creating sub-modules for each of these.
include("optimization/utils/constraints.jl")
include("optimization/utils/objectives.jl")
include("optimization/utils/variables.jl")
include("optimization/nsVerify.jl")
include("optimization/convDual.jl")
include("optimization/duality.jl")
include("optimization/certify.jl")
include("optimization/iLP.jl")
include("optimization/mipVerify.jl")
export NSVerify, ConvDual, Duality, Certify, ILP, MIPVerify
include("reachability/utils/reachability.jl")
include("reachability/exactReach.jl")
include("reachability/maxSens.jl")
include("reachability/ai2.jl")
export ExactReach, MaxSens, Ai2, Ai2h, Ai2z, Box
include("satisfiability/bab.jl")
include("satisfiability/sherlock.jl")
include("satisfiability/reluplex.jl")
export BaB, Sherlock, Reluplex
include("satisfiability/planet.jl")
export Planet
include("adversarial/reluVal.jl")
include("adversarial/neurify.jl")
include("adversarial/fastLin.jl")
include("adversarial/fastLip.jl")
include("adversarial/dlv.jl")
export ReluVal, Neurify, FastLin, FastLip, DLV
const TOL = Ref(sqrt(eps()))
set_tolerance(x::Real) = (TOL[] = x)
export set_tolerance
end