ConvDual and FastLip should take HalfSpace output sets

[castrong]

I would expect from the survey paper that ConvDual and FastLip can handle HalfSpace output sets. However, they each give errors when given a HalfSpace as an output set, although for different reasons. ConvDual expects a HPolytope as input, as seen in the function definition function dual_value(solver::ConvDual, network::Network, input::Hyperrectangle{N}, output::HPolytope{N}) where N . The error is shown below when you try to run it with a HalfSpace.

ERROR: LoadError: MethodError: no method matching dual_value(::ConvDual, ::Network, ::Hyperrectangle{Float64}, ::HalfSpace{Float64})
Closest candidates are:
dual_value(::ConvDual, ::Network, ::Hyperrectangle{N}, ::HPolytope{N}) where N at /Users/cstrong/Desktop/Stanford/Research/NV_Fork/NeuralVerification.jl/src/optimization/convDual.jl:40
Stacktrace:
[1] solve(::ConvDual, ::Problem{Hyperrectangle{Float64},HalfSpace{Float64}}) at /Users/cstrong/Desktop/Stanford/Research/NV_Fork/NeuralVerification.jl/src/optimization/convDual.jl:29
[2] top-level scope at /Users/cstrong/Desktop/Stanford/Research/NV_Fork/NeuralVerification.jl/examples/SimpleProblem.jl:8
[3] include at ./boot.jl:328 [inlined]
[4] include_relative(::Module, ::String) at ./loading.jl:1094
[5] include(::Module, ::String) at ./Base.jl:31
[6] include(::String) at ./client.jl:431
[7] top-level scope at none:0
in expression starting at /Users/cstrong/Desktop/Stanford/Research/NV_Fork/NeuralVerification.jl/examples/SimpleProblem.jl:8

In comparison, FastLip attempts to convert the HalfSpace into a HPolytope, but this conversion is unsuccessful. The line: c, d = tosimplehrep(convert(HPolytope, problem.output)) in fastLip.jl doesn't work to convert a halfspace to a HPolytope - it gives an error when I pass in a HPolytope. In comparison, HPolytope([problem.output]) would convert a halfspace into a polytope.

The error is pasted below:

ERROR: LoadError: MethodError: Cannot convert an object of type HalfSpace{Float64} to an object of type HPolytope
Closest candidates are:
convert(::Type{HPolytope}, ::HPolyhedron{N<:Real}) where N<:Real at /Users/cstrong/.julia/packages/LazySets/vv2cg/src/HPolyhedron.jl:661
convert(::Type{HPolytope}, ::AbstractHPolygon) at /Users/cstrong/.julia/packages/LazySets/vv2cg/src/convert.jl:86
convert(::Type{HPolytope}, ::VPolytope) at /Users/cstrong/.julia/packages/LazySets/vv2cg/src/convert.jl:186
...
Stacktrace:
[1] solve(::FastLip, ::Problem{Hyperrectangle{Float64},HalfSpace{Float64}}) at /Users/cstrong/Desktop/Stanford/Research/NV_Fork/NeuralVerification.jl/src/adversarial/fastLip.jl:38
[2] top-level scope at /Users/cstrong/Desktop/Stanford/Research/NV_Fork/NeuralVerification.jl/examples/SimpleProblem.jl:9
[3] include at ./boot.jl:328 [inlined]
[4] include_relative(::Module, ::String) at ./loading.jl:1094
[5] include(::Module, ::String) at ./Base.jl:31
[6] include(::String) at ./client.jl:431
[7] top-level scope at none:0
in expression starting at /Users/cstrong/Desktop/Stanford/Research/NV_Fork/NeuralVerification.jl/examples/SimpleProblem.jl:9

Code to reproduce:

# Setup problem
network = NeuralVerification.read_nnet("test_rand/networks/rand_[1,10,4,1]_3.nnet")
input_set = NeuralVerification.Hyperrectangle([0.18480275917946454], [0.6737285743432531])
output_set = HalfSpace([-0.1564803654117235], 0.10454913956365774)
problem = NeuralVerification.Problem(network, input_set, output_set)

# ConvDual and FastLip
#println(NeuralVerification.solve(NeuralVerification.ConvDual(), problem))
println(NeuralVerification.solve(NeuralVerification.FastLip(), problem))

Network:

//Default header text.
//Should replace with the real deal.
3, 1, 1, 10,
1, 10, 4, 1,
This line extraneous
-6.55e4,
6.55e4,
0.0,0.0,
1.0,1.0,
0.5288322389598363,
0.9823479701889837,
-0.5370789843033767,
-0.6263944851903522,
0.8971037043271797,
-0.802149016020731,
-0.6506999340714135,
0.9262012389766037,
0.03793705401523262,
-0.48287090754589146,
-0.6396030243168989,
-0.07336989391175264,
0.6348597054162952,
0.0482645113529645,
0.1921283453146474,
0.19997122595307992,
-0.09040415116558531,
-0.7532703509068335,
0.8801314550640673,
0.6640872178337465,
0.056674958167578726, 0.15445231894531286, -0.8263951384621664, -0.8694522989776954, -0.25418017585238006, 0.9586053750447525, -0.24627106224512962, 0.965702425851183, 0.19121822301940306, -0.5904194344887888,
0.011143978631912521, -0.822653382380937, 0.3164795494607673, -0.36975727437930095, 0.957297373679391, -0.3298287969334641, 0.006619748099108591, -0.6271523021609804, 0.25658155164872243, -0.8559382256105543,
-0.6402439454154596, 0.6757712495549013, -0.05786803222093395, -0.13834098396467143, -0.443813494042117, 0.0862127472144465, -0.6347596682197061, -0.5037016661679949, -0.8582507677657771, 0.08903020583983112,
-0.5176111310429126, -0.10355107470752722, 0.7744781778659333, 0.7205321670017155, 0.10109704829500155, -0.2864020619978742, -0.6260918478070154, 0.7217029739447907, 0.4297788124923083, -0.9844047983689155,
0.2641123726837802,
0.028585968331774403,
0.06068658450837505,
0.4517535541843194,
0.8670791194974665, -0.35750313130254696, 0.024010063821840788, 0.8662035529181007,
0.32595512763536316,

[changliuliu]

It seems we need to better type converter between HalfSpace and HPolytope. @tomerarnon, any thoughts?

[tomerarnon]

Maybe that conversion used to be legal, and while we could technically patch it up with HPolytope([halfspace]) – actually, ConvDual should only handle HalfSpace output constraints anyhow. We should therefore rewrite dual_value and the corresponding line in FastLip to handle exclusively halfspaces instead.