Backward Analysis using Preimage Approximation

CHANGELOG.md

@@ -5,6 +5,7 @@
   - Dropped support for parsing Tensorflow network format. Newest Marabou version that supports Tensorflow is at commit 190555573e4702.
   - Fixed bug in the parsing of `transpose` nodes in command line C++ parser.
   - Implemented forward-backward abstract interpretation, symbolic bound tightening, interval arithmetic and simulations for all activation functions.
+  - Implemented backward analysis using preimage-approximation algorithm for `Relu`, `LeakyRelu`, `Sign` and `Bilinear` Layers.
   - Added the BaBSR heuristic as a new branching strategy for ReLU Splitting
 
 ## Version 2.0.0

src/configuration/GlobalConfiguration.cpp

@@ -67,6 +67,13 @@ const unsigned GlobalConfiguration::ROW_BOUND_TIGHTENER_SATURATION_ITERATIONS =
 const double GlobalConfiguration::COST_FUNCTION_ERROR_THRESHOLD = 0.0000000001;
 
 const unsigned GlobalConfiguration::SIMULATION_RANDOM_SEED = 1;
+const unsigned GlobalConfiguration::VOLUME_ESTIMATION_RANDOM_SEED = 1;
+const unsigned GlobalConfiguration::PREIMAGE_APPROXIMATION_OPTIMIZATION_RANDOM_SEED = 1;
+const unsigned GlobalConfiguration::VOLUME_ESTIMATION_ITERATIONS = 25000;
+const unsigned GlobalConfiguration::PREIMAGE_APPROXIMATION_OPTIMIZATION_MAX_ITERATIONS = 25;
+const double GlobalConfiguration::PREIMAGE_APPROXIMATION_OPTIMIZATION_STEP_SIZE = 0.025;
+const double GlobalConfiguration::PREIMAGE_APPROXIMATION_OPTIMIZATION_LEARNING_RATE = 0.25;
+const double GlobalConfiguration::PREIMAGE_APPROXIMATION_OPTIMIZATION_WEIGHT_DECAY = 0;
 
 const bool GlobalConfiguration::USE_HARRIS_RATIO_TEST = true;
 

src/configuration/GlobalConfiguration.h

@@ -151,6 +151,27 @@ class GlobalConfiguration
     // Random seed for generating simulation values.
     static const unsigned SIMULATION_RANDOM_SEED;
 
+    // Random seed for EstimateVolume procedure (PreimageApproximation).
+    static const unsigned VOLUME_ESTIMATION_RANDOM_SEED;
+
+    // Number of iterations for EstimateVolume procedure (PreimageApproximation).
+    static const unsigned VOLUME_ESTIMATION_ITERATIONS;
+
+    // Random seed for PreimageApproximation optimization.
+    static const unsigned PREIMAGE_APPROXIMATION_OPTIMIZATION_RANDOM_SEED;
+
+    // Maximum iterations for PreimageApproximation optimization.
+    static const unsigned PREIMAGE_APPROXIMATION_OPTIMIZATION_MAX_ITERATIONS;
+
+    // Step size for PreimageApproximation optimization.
+    static const double PREIMAGE_APPROXIMATION_OPTIMIZATION_STEP_SIZE;
+
+    // Learning rate for PreimageApproximation optimization.
+    static const double PREIMAGE_APPROXIMATION_OPTIMIZATION_LEARNING_RATE;
+
+    // Weight decay for PreimageApproximation optimization.
+    static const double PREIMAGE_APPROXIMATION_OPTIMIZATION_WEIGHT_DECAY;
+
     // How often should projected steepest edge reset the reference space?
     static const unsigned PSE_ITERATIONS_BEFORE_RESET;
 

src/configuration/OptionParser.cpp

@@ -267,7 +267,8 @@ void OptionParser::initialize()
                 &( ( *_stringOptions )[Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE] ) )
                 ->default_value( ( *_stringOptions )[Options::MILP_SOLVER_BOUND_TIGHTENING_TYPE] ),
             "The MILP solver bound tightening type: "
-            "lp/backward-once/backward-converge/lp-inc/milp/milp-inc/iter-prop/none." )
+            "lp/backward-once/backward-converge/backward-preimage-approx/lp-inc/milp/milp-inc/"
+            "iter-prop/none." )
 #endif
         ;
 

src/configuration/Options.cpp

@@ -209,6 +209,8 @@ MILPSolverBoundTighteningType Options::getMILPSolverBoundTighteningType() const
             return MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_ONCE;
         if ( strategyString == "backward-converge" )
             return MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE;
+        if ( strategyString == "backward-preimage-approx" )
+            return MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_PREIMAGE_APPROX;
         else if ( strategyString == "milp" )
             return MILPSolverBoundTighteningType::MILP_ENCODING;
         else if ( strategyString == "milp-inc" )

src/engine/Engine.cpp

@@ -1594,6 +1594,7 @@ void Engine::performMILPSolverBoundedTightening( Query *inputQuery )
         case MILPSolverBoundTighteningType::LP_RELAXATION_INCREMENTAL:
         case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_ONCE:
         case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE:
+        case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_PREIMAGE_APPROX:
             _networkLevelReasoner->lpRelaxationPropagation();
             break;
         case MILPSolverBoundTighteningType::MILP_ENCODING:
@@ -1658,6 +1659,15 @@ void Engine::performAdditionalBackwardAnalysisIfNeeded()
                 printf( "Backward analysis tightened %u bounds\n", tightened );
         }
     }
+
+    if ( _milpSolverBoundTighteningType ==
+         MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_PREIMAGE_APPROX )
+    {
+        performMILPSolverBoundedTightening( &( *_preprocessedQuery ) );
+        unsigned tightened = performSymbolicBoundTightening( &( *_preprocessedQuery ) );
+        if ( _verbosity > 0 )
+            printf( "Backward analysis tightened %u bounds\n", tightened );
+    }
 }
 
 void Engine::performMILPSolverBoundedTighteningForSingleLayer( unsigned targetIndex )
@@ -1685,6 +1695,7 @@ void Engine::performMILPSolverBoundedTighteningForSingleLayer( unsigned targetIn
             return;
         case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_ONCE:
         case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_CONVERGE:
+        case MILPSolverBoundTighteningType::BACKWARD_ANALYSIS_PREIMAGE_APPROX:
         case MILPSolverBoundTighteningType::ITERATIVE_PROPAGATION:
         case MILPSolverBoundTighteningType::NONE:
             return;
@@ -3879,4 +3890,4 @@ void Engine::addPLCLemma( std::shared_ptr<PLCLemma> &explanation )
     ASSERT( explanation && _UNSATCertificate && _UNSATCertificateCurrentPointer )
     _statistics.incUnsignedAttribute( Statistics::NUM_LEMMAS );
     _UNSATCertificateCurrentPointer->get()->addPLCLemma( explanation );
-}
+}

src/engine/MILPSolverBoundTighteningType.h

@@ -34,6 +34,9 @@ enum class MILPSolverBoundTighteningType {
     // Perform backward analysis
     BACKWARD_ANALYSIS_ONCE = 5,
     BACKWARD_ANALYSIS_CONVERGE = 6,
+    // Perform backward analysis using the PreimageApproximation Algorithm (arXiv:2305.03686v4
+    // [cs.SE])
+    BACKWARD_ANALYSIS_PREIMAGE_APPROX = 7,
     // Option to have no MILP bound tightening performed
     NONE = 10,
 };