DLV and BaB disagreement - likely DLV incompleteness
castrong opened this issue · 1 comments
The following code:
# Setup problem
network = NeuralVerification.read_nnet("./examples/networks/issue_net.nnet")
input_set = NeuralVerification.Hyperrectangle([-0.10334147429868268], [0.32133057065509174])
output_set = LazySets.Hyperrectangle([-0.29647810140569675], [0.914490983040116])
problem = NeuralVerification.Problem(network, input_set, output_set)
# Solve on DLV
println("DLV Result: ", NeuralVerification.solve(NeuralVerification.DLV(), problem))
println("BaB Result: ", NeuralVerification.solve(NeuralVerification.BaB(), problem))
With Network:
//Neural Network File Format by Kyle Julian, Stanford 2016.
4, 1, 1, 12,
1, 10, 12, 10, 1,
This line extraneous
-6.55e4,
6.55e4,
0.0,0.0,
1.0,1.0,
0.6855274865721181,
-0.9771575891696487,
0.24436191691459674,
0.5796979313522272,
0.31736117496886296,
-0.01098060958697955,
0.8213744894997128,
0.8341318198443974,
-0.8209153033350445,
0.8748276255647438,
-0.02780899493631317,
0.6254547742356324,
0.9028629380001885,
0.7421042871086527,
-0.5105259810966238,
0.9865614475416726,
-0.8546646759850591,
-0.802576112682059,
0.8206006475828982,
0.21138724954653476,
0.020565075139380884, 0.47977285921607127, -0.8384535934240396, 0.6926767830304166, -0.24992799881317307, -0.7923556274439023, 0.6505350268500352, 0.84959293851144, -0.7171457493100819, 0.4479244608176405,
-0.9576825703159657, -0.8208635829950746, 0.9967328371620554, -0.38568756074467725, -0.5887147098974772, 0.2117484980258313, -0.8889828629448626, -0.8534402300138528, 0.18211148359530416, 0.08598719524245091,
-0.36817506925059496, 0.34511305065090614, 0.22278999969342506, -0.4673777673425148, -0.1271976652676301, -0.4784969718626999, -0.573716025780147, -0.7575149056807238, 0.8797424159285745, -0.10500125316912978,
0.6774279414034177, -0.14796635045958695, 0.037417248804217706, -0.7163253309065887, 0.8905544493488233, -0.2251935870762991, 0.5892221329874872, -0.47412932191847856, -0.45935517881220367, 0.995361511972702,
-0.2065944670109423, -0.9742963620688045, 0.6038744580446243, 0.5465800370732432, -0.83558215567282, -0.7454780152981848, 0.7220250192107871, -0.8584613482999526, 0.3584187689440155, -0.7170066618828304,
-0.5193392209764243, 0.7818715970564587, 0.2922521555959574, 0.5026137650138649, 0.2743066872973472, -0.9816016832628098, -0.02955072555331162, -0.891375965224507, 0.22401710270400343, -0.396342518279706,
0.011545282937801549, -0.5491887912356015, -0.22192483941297114, -0.6075347324538964, 0.90433099246028, 0.36485388035023725, 0.34744109523580624, -0.9975593520547261, 0.07017773106941183, -0.2939772750089795,
0.5996053962661256, -0.8851118745713809, 0.07372797031461831, -0.7481007235025774, 0.5963707941486445, 0.05791729798424905, -0.28756919674485903, -0.16318354185670358, -0.39285954737813444, -0.5475444099631899,
0.1412508030824391, 0.9019111366506687, -0.3172528845164808, 0.06725966099722847, -0.954094604916957, 0.7518021589915471, -0.1795971244896868, 0.9868401855882358, 0.6053555740278038, 0.8502437048068914,
0.6187042424474174, -0.45550155659273717, 0.5228066756103655, 0.21174763488890846, 0.47564081497244715, 0.9358669244150932, -0.13910517607432027, 0.8894104506559537, -0.8604981615066007, 0.6926865682069265,
0.5914476409709466, -0.9716494727071341, -0.22986423143197499, -0.3764994324215727, 0.9878065260380313, 0.8606407627163879, -0.02078902318557274, -0.8977088782432743, -0.6957219303789253, 0.6441992768091946,
-0.4607444448862754, 0.9027690207535604, -0.7247585900908344, -0.3107573629992295, 0.04453449811424148, -0.02338338160334974, 0.38646110096957775, 0.7896444773350613, 0.28881867866758526, -0.3958259874719894,
0.726209989148729,
0.5656006425747826,
0.514464310247214,
0.36296583838117424,
0.4870751139556715,
0.7377130283755933,
-0.13221237906210526,
-0.11514799126622632,
0.21449374428736734,
0.9588947975004651,
-0.3090596075708629,
-0.40170169478839846,
-0.7221274956673138, -0.7405883860124152, -0.49270951493391024, -0.5584899565292152, -0.2892979010190655, -0.8556305250147185, -0.5945416401090711, -0.8037760645691847, -0.4569070886785762, 0.6553459260723096, 0.3806675582455612, -0.1481190175802065,
0.216598046789803, -0.6799291724853576, 0.4944323131709183, 0.13725084918401587, 0.9710244287519063, 0.581992391091708, 0.26754394164913053, -0.19909822089558782, -0.853778569230113, 0.016489984639596944, -0.344571508385207, -0.579410234644913,
-0.00855894128064838, -0.5669659770629218, 0.5408715615083972, 0.5133205832639693, -0.6456232889742668, -0.2977893735583437, -0.8579750397037262, -0.435155510223292, -0.09655246998869238, 0.6735802095734971, -0.9234637130468286, 0.15530072629225478,
0.4737081955792868, -0.58319811840067, -0.1921543526864391, -0.5783517477767068, 0.4207706288038402, -0.4729271473718386, 0.7685775813184015, -0.9347361444025166, -0.5508314592874997, 0.2669522397525541, -0.4337036474088163, 0.8509039651798491,
0.04135961363364382, -0.1421464528202816, 0.26368054699090404, -0.8486533414898854, 0.38544270139018577, -0.13561988366163336, -0.2863942481260513, -0.2168537111694251, -0.21232515401218777, -0.3750314162577135, -0.8465208396784107, -0.9416275464400852,
-0.9857180510672663, -0.9027803408624124, -0.6519485042057593, -0.39455337238180244, -0.0864103595252792, -0.48267276562818395, -0.014691500861953699, 0.4045519978160117, -0.8300042297644978, 0.019723710641907477, -0.48201490541113357, -0.8659657393646252,
-0.18289622183314824, -0.02097761127463027, -0.685024929182863, 0.7920619781022755, 0.7700481750075898, -0.45817226786407605, -0.5748057316431514, -0.235627727154331, -0.6452487655685912, 0.004151148148205497, -0.02542401308394915, 0.07389955714509666,
-0.826615422258627, 0.22668445600642206, -0.5966298311740923, -0.14595827849028042, 0.7853297440205398, -0.020616580439481336, -0.047263572116301944, 0.7996209715057909, -0.8440175140345034, -0.623787516600264, -0.5291558629820172, -0.6316744877089091,
-0.8488994714962037, 0.26066860030615846, 0.5230369839127933, -0.36194708942263976, -0.45927224673292777, -0.943164131772432, 0.8106021131645167, 0.05647981928411516, 0.34070505167527676, 0.3093812927309081, 0.8745139997534164, -0.8039982920141124,
0.6758096026958684, -0.9664865175660222, 0.853513120125585, -0.35828950114853875, -0.9497914410585024, 0.06246927033801075, 0.3472537292179476, -0.48072971151973354, -0.41559655797298367, 0.7262559428033741, -0.8979283192284915, 0.27074820323064586,
-0.9697133669338274,
0.5198217766153634,
0.7440285167589615,
-0.1221561580157835,
0.26422978480920145,
0.7596226808676572,
0.9949539708495787,
-0.6047506676747569,
-0.45877638795841413,
-0.7963894899189654,
-0.31452863395591235, 0.11529303795464863, 0.7855794788287289, -0.6759802351783284, 0.5630056978948752, 0.6943065855395743, -0.40266701105687996, -0.2354663461525246, 0.6196050823719204, -0.03168094553802625,
-0.7769094155628848,
Leads to the following output:
DLV Result: violated
BaB Result: holds
DLV is either performing incompletely, or BaB is performing unsoundly. BaB also agrees with Reluval so it's likely that DLV is incorrect.
I just realized that in the NV.jl implementation of DLV it is sound but not complete. As a result, this does not seem to actually be an issue.