Skip to content

Instantly share code, notes, and snippets.

@mforets

mforets/neuralverif_lazysets.jl

Created February 4, 2020 16:56
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mforets/05d3c27edda7c7cb4f0947e1e0538e0a to your computer and use it in GitHub Desktop.
Save mforets/05d3c27edda7c7cb4f0947e1e0538e0a to your computer and use it in GitHub Desktop.
Download ZIP
Test NeuralVerification on LazySets#master
Raw
neuralverif_lazysets.jl
(v1.2) pkg> test NeuralVerification
Updating registry at `~/.julia/registries/General`
Updating git-repo `https://github.com/JuliaRegistries/General.git`
Testing NeuralVerification
Resolving package versions...
Status `/tmp/jl_Wfxs1N/Manifest.toml`
[621f4979] AbstractFFTs v0.5.0
[1520ce14] AbstractTrees v0.3.1
[79e6a3ab] Adapt v1.0.0
[13072b0f] AxisAlgorithms v1.0.0
[6e4b80f9] BenchmarkTools v0.4.3
[9e28174c] BinDeps v0.8.10
[b99e7846] BinaryProvider v0.5.8
[3391f64e] CDDLib v0.5.3
[fa961155] CEnum v0.2.0
[96374032] CRlibm v0.8.0
[3895d2a7] CUDAapi v1.2.0
[c5f51814] CUDAdrv v3.1.0
[be33ccc6] CUDAnative v2.4.0
[49dc2e85] Calculus v0.5.1
[944b1d66] CodecZlib v0.6.0
[3da002f7] ColorTypes v0.9.1
[5ae59095] Colors v0.11.2
[bbf7d656] CommonSubexpressions v0.2.0
[34da2185] Compat v2.2.0
[8f4d0f93] Conda v1.3.0
[3a865a2d] CuArrays v1.2.1
[9a962f9c] DataAPI v1.1.0
[864edb3b] DataStructures v0.17.9
[163ba53b] DiffResults v1.0.2
[b552c78f] DiffRules v1.0.0
[90fa49ef] ErrorfreeArithmetic v0.4.1
[7a1cc6ca] FFTW v1.1.0
[fa42c844] FastRounding v0.2.0
[1a297f60] FillArrays v0.7.4
[53c48c17] FixedPointNumbers v0.6.1
[587475ba] Flux v0.9.0
[f6369f11] ForwardDiff v0.10.8
[60bf3e95] GLPK v0.12.1
[3c7084bd] GLPKMathProgInterface v0.4.4
[0c68f7d7] GPUArrays v1.0.4
[4d00f742] GeometryTypes v0.7.7
[a98d9a8b] Interpolations v0.12.8
[d1acc4aa] IntervalArithmetic v0.16.3 #v0.16.3 (https://github.com/JuliaIntervals/IntervalArithmetic.jl.git)
[682c06a0] JSON v0.21.0
[4076af6c] JuMP v0.20.1
[e5e0dc1b] Juno v0.7.2
[929cbde3] LLVM v1.3.3
[b4f0291d] LazySets v1.27.0 [`~/.julia/dev/LazySets`]
[1914dd2f] MacroTools v0.5.4
[b8f27783] MathOptInterface v0.9.7
[fdba3010] MathProgBase v0.7.7
[e89f7d12] Media v0.5.0
[e1d29d7a] Missings v0.4.3
[872c559c] NNlib v0.6.4
[77ba4419] NaNMath v0.3.3
[146f25fa] NeuralVerification v0.0.0 #master (https://github.com/sisl/NeuralVerification.jl.git)
[6fe1bfb0] OffsetArrays v1.0.2
[bac558e1] OrderedCollections v1.1.0
[774612a8] ParameterJuMP v0.1.2
[d96e819e] Parameters v0.12.0
[69de0a69] Parsers v0.3.11
[ff2beb65] PicoSAT v0.3.2
[67491407] Polyhedra v0.5.7 [`~/.julia/dev/Polyhedra`]
[c84ed2f1] Ratios v0.3.1
[3cdcf5f2] RecipesBase v0.7.0
[189a3867] Reexport v0.2.0
[ae029012] Requires v0.5.2
[c946c3f1] SCS v0.6.4
[3cc68bcd] SetRounding v0.2.0
[a2af1166] SortingAlgorithms v0.3.1
[276daf66] SpecialFunctions v0.8.0
[90137ffa] StaticArrays v0.12.1
[2913bbd2] StatsBase v0.32.0
[a759f4b9] TimerOutputs v0.5.3
[9f7883ad] Tracker v0.2.6
[3bb67fe8] TranscodingStreams v0.9.5
[30578b45] URIParser v0.4.0
[81def892] VersionParsing v1.2.0
[efce3f68] WoodburyMatrices v0.5.0
[a5390f91] ZipFile v0.8.4
[2a0f44e3] Base64 [`@stdlib/Base64`]
[ade2ca70] Dates [`@stdlib/Dates`]
[8bb1440f] DelimitedFiles [`@stdlib/DelimitedFiles`]
[8ba89e20] Distributed [`@stdlib/Distributed`]
[b77e0a4c] InteractiveUtils [`@stdlib/InteractiveUtils`]
[76f85450] LibGit2 [`@stdlib/LibGit2`]
[8f399da3] Libdl [`@stdlib/Libdl`]
[37e2e46d] LinearAlgebra [`@stdlib/LinearAlgebra`]
[56ddb016] Logging [`@stdlib/Logging`]
[d6f4376e] Markdown [`@stdlib/Markdown`]
[a63ad114] Mmap [`@stdlib/Mmap`]
[44cfe95a] Pkg [`@stdlib/Pkg`]
[de0858da] Printf [`@stdlib/Printf`]
[9abbd945] Profile [`@stdlib/Profile`]
[3fa0cd96] REPL [`@stdlib/REPL`]
[9a3f8284] Random [`@stdlib/Random`]
[ea8e919c] SHA [`@stdlib/SHA`]
[9e88b42a] Serialization [`@stdlib/Serialization`]
[1a1011a3] SharedArrays [`@stdlib/SharedArrays`]
[6462fe0b] Sockets [`@stdlib/Sockets`]
[2f01184e] SparseArrays [`@stdlib/SparseArrays`]
[10745b16] Statistics [`@stdlib/Statistics`]
[8dfed614] Test [`@stdlib/Test`]
[cf7118a7] UUIDs [`@stdlib/UUIDs`]
[4ec0a83e] Unicode [`@stdlib/Unicode`]
[ Info: MaxSens overapproximates HPolytope input sets as Hyperrectangles.
[ Info: MaxSens overapproximates HPolytope input sets as Hyperrectangles.
dGroup 1: Error During Test at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:17
Got exception outside of a @test
AssertionError: a half-space needs a non-zero normal vector
Stacktrace:
[1] macro expansion at /home/mforets/.julia/dev/LazySets/src/Assertions/Assertions.jl:23 [inlined]
[2] HalfSpace{Float64,Array{Float64,1}}(::Array{Float64,1}, ::Float64) at /home/mforets/.julia/dev/LazySets/src/Sets/HalfSpace.jl:36
[3] HalfSpace(::Array{Float64,1}, ::Float64) at /home/mforets/.julia/dev/LazySets/src/Sets/HalfSpace.jl:45
[4] #_linear_map_hrep_helper#32(::Nothing, ::typeof(LazySets._linear_map_hrep_helper), ::Array{Float64,2}, ::HPolytope{Float64}, ::Bool) at /home/mforets/.julia/dev/LazySets/src/Interfaces/AbstractPolyhedron_functions.jl:504
[5] #_linear_map_hrep_helper at ./none:0 [inlined]
[6] #_linear_map_hrep#96 at /home/mforets/.julia/dev/LazySets/src/Sets/HPolytope.jl:136 [inlined]
[7] _linear_map_hrep at /home/mforets/.julia/dev/LazySets/src/Sets/HPolytope.jl:136 [inlined]
[8] #linear_map#29(::Nothing, ::Bool, ::Float64, ::Nothing, ::typeof(linear_map), ::Array{Float64,2}, ::HPolytope{Float64}) at /home/mforets/.julia/dev/LazySets/src/Interfaces/AbstractPolyhedron_functions.jl:435
[9] linear_map at /home/mforets/.julia/dev/LazySets/src/Interfaces/AbstractPolyhedron_functions.jl:400 [inlined]
[10] affine_map(::NeuralVerification.Layer{Id,Float64}, ::HPolytope{Float64}) at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/src/utils/util.jl:309
[11] forward_layer(::ExactReach, ::NeuralVerification.Layer{Id,Float64}, ::Array{HPolytope,1}) at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/src/reachability/exactReach.jl:37
[12] forward_network(::ExactReach, ::Network, ::HPolytope{Float64}) at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/src/reachability/utils/reachability.jl:9
[13] solve(::ExactReach, ::Problem{HPolytope{Float64},HPolytope{Float64}}) at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/src/reachability/exactReach.jl:28
[14] top-level scope at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:22
[15] top-level scope at /buildworker/worker/package_linux64/build/usr/share/julia/stdlib/v1.2/Test/src/Test.jl:1113
[16] top-level scope at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:18
[17] top-level scope at /buildworker/worker/package_linux64/build/usr/share/julia/stdlib/v1.2/Test/src/Test.jl:1113
[18] top-level scope at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:4
[19] include at ./boot.jl:328 [inlined]
[20] include_relative(::Module, ::String) at ./loading.jl:1094
[21] include(::Module, ::String) at ./Base.jl:31
[22] include(::String) at ./client.jl:431
[23] top-level scope at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/runtests.jl:17
[24] include at ./boot.jl:328 [inlined]
[25] include_relative(::Module, ::String) at ./loading.jl:1094
[26] include(::Module, ::String) at ./Base.jl:31
[27] include(::String) at ./client.jl:431
[28] top-level scope at none:5
[29] eval(::Module, ::Any) at ./boot.jl:330
[30] exec_options(::Base.JLOptions) at ./client.jl:271
[31] _start() at ./client.jl:464
Group 2, 3, 4, 6: Error During Test at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:33
Got exception outside of a @test
AssertionError: lower bound must be lower than upper bound
Stacktrace:
[1] macro expansion at /home/mforets/.julia/dev/LazySets/src/Assertions/Assertions.jl:23 [inlined]
[2] #Hyperrectangle#118(::Array{Float64,1}, ::Array{Float64,1}, ::Type{Hyperrectangle}) at /home/mforets/.julia/dev/LazySets/src/Sets/Hyperrectangle.jl:97
[3] Type at ./array.jl:0 [inlined]
[4] tighten_bounds(::Problem{Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}},HPolytope{Float64}}, ::Type) at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/src/satisfiability/planet.jl:149
[5] solve(::Planet, ::Problem{Hyperrectangle{Float64,Array{Float64,1},Array{Float64,1}},HPolytope{Float64}}) at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/src/satisfiability/planet.jl:36
[6] top-level scope at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:45
[7] top-level scope at /buildworker/worker/package_linux64/build/usr/share/julia/stdlib/v1.2/Test/src/Test.jl:1113
[8] top-level scope at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:35
[9] top-level scope at /buildworker/worker/package_linux64/build/usr/share/julia/stdlib/v1.2/Test/src/Test.jl:1113
[10] top-level scope at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:4
[11] include at ./boot.jl:328 [inlined]
[12] include_relative(::Module, ::String) at ./loading.jl:1094
[13] include(::Module, ::String) at ./Base.jl:31
[14] include(::String) at ./client.jl:431
[15] top-level scope at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/runtests.jl:17
[16] include at ./boot.jl:328 [inlined]
[17] include_relative(::Module, ::String) at ./loading.jl:1094
[18] include(::Module, ::String) at ./Base.jl:31
[19] include(::String) at ./client.jl:431
[20] top-level scope at none:5
[21] eval(::Module, ::Any) at ./boot.jl:330
[22] exec_options(::Base.JLOptions) at ./client.jl:271
[23] _start() at ./client.jl:464
bounds: [-69.1, -25.900000000000002]
bounds: [-69.1, -25.900000000000002]
----------------------------------------------------------------------------
SCS v2.1.1 - Splitting Conic Solver
(c) Brendan O'Donoghue, Stanford University, 2012
----------------------------------------------------------------------------
Lin-sys: sparse-indirect, nnz in A = 9, CG tol ~ 1/iter^(2.00)
eps = 1.00e-05, alpha = 1.50, max_iters = 5000, normalize = 1, scale = 1.00
acceleration_lookback = 10, rho_x = 1.00e-03
Variables n = 6, constraints m = 9
Cones: linear vars: 3
sd vars: 6, sd blks: 1
Setup time: 1.35e-04s
----------------------------------------------------------------------------
Iter | pri res | dua res | rel gap | pri obj | dua obj | kap/tau | time (s)
----------------------------------------------------------------------------
0| 1.83e+19 2.64e+18 1.00e+00 -7.69e+18 -0.00e+00 4.01e+18 8.21e-05
29| 1.07e-10 3.80e-11 8.27e-12 -5.00e-01 -5.00e-01 2.08e-17 3.29e-04
----------------------------------------------------------------------------
Status: Solved
Timing: Solve time: 3.34e-04s
Lin-sys: avg # CG iterations: 1.00, avg solve time: 5.46e-07s
Cones: avg projection time: 5.38e-06s
Acceleration: avg step time: 2.85e-06s
----------------------------------------------------------------------------
Error metrics:
dist(s, K) = 2.0460e-09, dist(y, K*) = 1.8357e-09, s'y/|s||y| = 2.8096e-12
primal res: |Ax + s - b|_2 / (1 + |b|_2) = 1.0684e-10
dual res: |A'y + c|_2 / (1 + |c|_2) = 3.8025e-11
rel gap: |c'x + b'y| / (1 + |c'x| + |b'y|) = 8.2678e-12
----------------------------------------------------------------------------
c'x = -0.5000, -b'y = -0.5000
============================================================================
Test Summary: | Pass Error Total
Id Last Layer | 27 2 29
Group 1 | 2 1 3
MaxSens | 2 2
Group 2, 3, 4, 6 | 16 1 17
NSVerify | 2 2
MIPVerify | 2 2
ILP | 2 2
ConvDual | 2 2
Duality | 2 2
FastLin | 2 2
FastLip | 2 2
Reluplex | 2 2
Group 5 | 8 8
Certify | 1 1
ERROR: LoadError: LoadError: Some tests did not pass: 27 passed, 0 failed, 2 errored, 0 broken.
in expression starting at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/identity_network.jl:2
in expression starting at /home/mforets/.julia/packages/NeuralVerification/4qLbJ/test/runtests.jl:17
ERROR: Package NeuralVerification errored during testing
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment