Produce proofs for Sign, Max, Absolute Value and Disjunction constrai…

…nts (#689)
NeuralNetworkVerification · Dec 11, 2023 · 8349949 · 8349949
1 parent a2077b4
commit 8349949
Show file tree

Hide file tree

Showing 55 changed files with 22,793 additions and 485 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,9 +1,8 @@
 # Changelog
 
-## Version 1.1.0
-
-* Added support for onnx networks with `tanh` nodes to command-line interface.
+## Next Release
+* Added support for onnx networks with tanh nodes to command-line interface.
+* Added proof producing versions of Sign, Max, Absolute Value and Disjunction constraints
 
 ## Version 1.0.0
-
 * Initial versioned release
diff --git a/maraboupy/Marabou.py b/maraboupy/Marabou.py
@@ -126,7 +126,7 @@ def createOptions(numWorkers=1, initialTimeout=5, initialSplits=0, onlineSplits=
                   preprocessorBoundTolerance=0.0000000001, dumpBounds=False,
                   tighteningStrategy="deeppoly", milpTightening="none", milpSolverTimeout=0,
                   numSimulations=10, numBlasThreads=1, performLpTighteningAfterSplit=False,
-                  lpSolver=""):
+                  lpSolver="", produceProofs=False):
     """Create an options object for how Marabou should solve the query
 
     Args:
@@ -179,4 +179,5 @@ def createOptions(numWorkers=1, initialTimeout=5, initialSplits=0, onlineSplits=
     options._numBlasThreads = numBlasThreads
     options._performLpTighteningAfterSplit = performLpTighteningAfterSplit
     options._lpSolver = lpSolver
+    options._produceProofs = produceProofs
     return options
diff --git a/maraboupy/MarabouCore.cpp b/maraboupy/MarabouCore.cpp
@@ -231,7 +231,7 @@ struct MarabouOptions {
         , _tighteningStrategyString( Options::get()->getString( Options::SYMBOLIC_BOUND_TIGHTENING_TYPE ).ascii() )
         , _milpTighteningString( Options::get()->getString( Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE ).ascii() )
         , _lpSolverString( Options::get()->getString( Options::LP_SOLVER ).ascii() )
-        , _produceProofs( Options::get()->getBool( Options::PRODUCE_PROOFS ))
+        , _produceProofs( Options::get()->getBool( Options::PRODUCE_PROOFS ) )
     {};
 
   void setOptions()

diff --git a/regress/regress1/CMakeLists.txt b/regress/regress1/CMakeLists.txt
@@ -140,6 +140,8 @@ foreach(file ${unsat_ipqs})
 endforeach()
 
 # Proof production tests
+
+# ReLU
 marabou_add_acasxu_proof_test(1 "ACASXU_experimental_v2a_5_9" "3" unsat)
 marabou_add_acasxu_proof_test(1 "ACASXU_experimental_v2a_5_7" "3" unsat)
 marabou_add_acasxu_proof_test(1 "ACASXU_experimental_v2a_3_7" "3" unsat)
@@ -150,3 +152,17 @@ marabou_add_coav_proof_test(1 "reluBenchmark0.453322172165s_UNSAT.nnet" unsat)
 marabou_add_coav_proof_test(1 "reluBenchmark0.30711388588s_UNSAT.nnet" unsat)
 marabou_add_coav_proof_test(1 "reluBenchmark0.725997209549s_UNSAT.nnet" unsat)
 marabou_add_coav_proof_test(1 "reluBenchmark1.81178617477s_UNSAT.nnet" unsat)
+
+# Absolute value
+marabou_add_input_query_test(1 ACASXU_abstest1.ipq unsat "--prove-unsat" "ipq")
+marabou_add_input_query_test(1 ACASXU_abstest2.ipq unsat "--prove-unsat" "ipq")
+
+# ReLU ad Max
+marabou_add_input_query_test(1 ACASXU_maxtest1.ipq unsat "--prove-unsat" "ipq")
+marabou_add_input_query_test(1 ACASXU_maxtest2.ipq unsat "--prove-unsat" "ipq")
+
+# Sign
+marabou_add_input_query_test(1 deep_6_index_5566.ipq unsat "--prove-unsat" "ipq")
+marabou_add_input_query_test(1 deep_6_index_5567.ipq unsat "--prove-unsat" "ipq")
+marabou_add_input_query_test(1 deep_6_index_5525.ipq unsat "--prove-unsat" "ipq")
+marabou_add_input_query_test(1 deep_6_index_7779.ipq unsat "--prove-unsat" "ipq")