NSVerify and ILP disagreement - likely ILP unsoundness.

[castrong]

With Code:

# Setup problem
network = NeuralVerification.read_nnet("./examples/networks/issue_net.nnet")
input_set = LazySets.Hyperrectangle([0.3239560971706661, -0.051023198756482646, 0.10643884307283402, 0.2617471526666566, -0.4876992062506713], [0.27511191847549554, 0.4726664814672026, 0.4758823479375396, 0.3623388331604731, 0.22049620536613213])
output_set = NeuralVerification.PolytopeComplement(LazySets.HPolytope([LazySets.HalfSpace([1.0], 0.46396369980702556), LazySets.HalfSpace([-1.0], -0.4508776562797363)]))
problem = NeuralVerification.Problem(network, input_set, output_set)

ns_status = NeuralVerification.solve(NeuralVerification.NSVerify(), problem).status
ilp_status =  NeuralVerification.solve(NeuralVerification.ILP(), problem).status
println("NSVerify status: ", ns_status)
println("ILP status: ", ilp_status)

**And Network: **
//Neural Network File Format by Kyle Julian, Stanford 2016.
2, 1, 1, 8,
1, 8, 1,
This line extraneous
-6.55e4,
6.55e4,
0.0,0.0,
1.0,1.0,
0.8678491028912014, -0.5203780903607784, -0.5142031406625782, -0.6977040448276313, -0.976885080551285,
-0.1460743574085881, 0.3154578548182978, 0.9532183372024212, -0.574760350454679, 0.6341150831930098,
-0.7898630677526377, -0.7313180250715745, -0.20467484308960016, 0.40858515372716386, -0.6385823044294656,
-0.35203560829994407, 0.3166304799264661, -0.4619174469634739, 0.9392249552449465, 0.9352413917562559,
-0.5166440988054104, -0.7696079370706981, -0.6942957067572171, 0.7201009053603964, -0.007367629464616776,
-0.11301221277218598, -0.8316575309519427, -0.5740001481764962, 0.585516746004052, -0.1275076273402127,
0.6528733981400743, -0.528579455088038, 0.5254640882299264, -0.18236568211966997, 0.4216232004175584,
0.09289100811092821, -0.5906110198701051, -0.294992020863452, -0.7075907072711356, 0.05897916487234678,
-0.7916178249103649,
0.8827517443779862,
0.9343433076177265,
0.6578225443695569,
-0.3738002314516393,
0.06144220503151221,
-0.4321020299223699,
0.9526704735111897,
0.3026126411435861, 0.8315846865097773, -0.3369949483042576, -0.39003179677505795, -0.5689773963054372, -0.39423845997276885, 0.7920399806911957, 0.27837965275096366,
-0.7002483710662677,

**We get output: **

NSVerify status: violated
ILP status: holds

Either NSVerify is incomplete or ILP is unsound. MIPVerify, Planet, and Reluplex agree with NSVerify so it's likely that ILP is acting unsoundly.

[changliuliu]

This will be addressed by #154 (comment)

iLP only checks one linear branch of the network that has the same activation as the center of the input set. Hence it should return false for any input set that goes beyond one linear branch.

Now instead of comparing the maximum allowable disturbance with the maximum input radius (scalar to scalar comparison), we check the possible deviation in every dimension (vector to vector comparison). If in either dimension, the input radius is greater than the allowable disturbance in that dimension, we will return a :violation.