Incremental linearization (#535)

* initial commit for incremental linearization Signed-off-by: tagomaru <[email protected]> * fix build error Signed-off-by: tagomaru <[email protected]> * fix build error Signed-off-by: tagomaru <[email protected]> * merge two PLW into one Signed-off-by: tagomaru <[email protected]> * add only a secant line by default for the first linearization Signed-off-by: tagomaru <[email protected]> * devide SplitPoint into TangentPoint and SecantPoint Signed-off-by: tagomaru <[email protected]> * clip use option Signed-off-by: tagomaru <[email protected]> * support numWorkers Signed-off-by: tagomaru <[email protected]> * add concat * clang format * new file uncommited * clang format * fix test --------- Signed-off-by: tagomaru <[email protected]> Co-authored-by: anwu1219 <[email protected]>
NeuralNetworkVerification · Feb 19, 2024 · 3c2d389 · 3c2d389
1 parent ed292e5
commit 3c2d389
Show file tree

Hide file tree

Showing 28 changed files with 1,028 additions and 96 deletions.
diff --git a/maraboupy/test/test_core.py b/maraboupy/test/test_core.py
@@ -141,13 +141,6 @@ def test_dump_query():
         assert vals[var] <= ipq.getUpperBound(var)
     assert exitCode == "sat"
 
-    # Marabou should find tighter bounds than LARGE after bound propagation, including
-    # for variable 2, where no upper bound was explicitly given
-    assert ipq.getUpperBound(1) < LARGE
-    assert ipq.getLowerBound(2) > -LARGE
-    assert ipq.getUpperBound(2) < LARGE
-
-
 def define_ipq(property_bound):
     """
     This function defines a simple input query directly through MarabouCore

diff --git a/maraboupy/test/test_onnx.py b/maraboupy/test/test_onnx.py
@@ -73,6 +73,13 @@ def test_softmax():
     filename =  "softmax-last-layer.onnx"
     evaluateFile(filename)
 
+def test_sigmoid():
+    """
+    Test loading network with sigmoid activations
+    """
+    filename =  "mnist2x5_sigmoid.onnx"
+    evaluateFile(filename)
+
 def test_gtsrb():
     """
     Test a convolutional network, exported from tensorflow

diff --git a/resources/onnx/mnist2x5_sigmoid.onnx b/resources/onnx/mnist2x5_sigmoid.onnx
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -54,3 +54,4 @@ add_subdirectory(${INPUT_PARSERS_DIR})
 add_subdirectory(query_loader)
 add_subdirectory(nlr)
 add_subdirectory(proofs)
+add_subdirectory(cegar)
diff --git a/src/cegar/CMakeLists.txt b/src/cegar/CMakeLists.txt
@@ -0,0 +1,23 @@
+file(GLOB SRCS "*.cpp")
+file(GLOB HEADERS "*.h")
+
+
+target_sources(${MARABOU_LIB} PRIVATE ${SRCS})
+target_include_directories(${MARABOU_LIB} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}")
+
+target_sources(${MARABOU_TEST_LIB} PRIVATE ${SRCS})
+target_include_directories(${MARABOU_TEST_LIB} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}")
+
+set (CEGAR_TESTS_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tests")
+macro(cegar_add_unit_test name)
+    set(USE_REAK_COMMON TRUE)
+    set(USE_REAL_ENGINE TRUE)
+    marabou_add_test(${CEGAR_TESTS_DIR}/Test_${name} cegar USE_REAL_COMMON
+        USE_REAL_ENGINE "unit")
+endmacro()
+
+cegar_add_unit_test(IncrementalLinearization)
+
+if (${BUILD_PYTHON})
+    target_include_directories(${MARABOU_PY} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}")
+endif()
diff --git a/src/cegar/IncrementalLinearization.cpp b/src/cegar/IncrementalLinearization.cpp
@@ -0,0 +1,153 @@
+/*********************                                                        */
+/*! \file IncrementalLinearizatoin.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Teruhiro Tagomori, Andrew Wu
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ **/
+
+#include "IncrementalLinearization.h"
+
+#include "Engine.h"
+#include "FloatUtils.h"
+#include "GurobiWrapper.h"
+#include "InputQuery.h"
+#include "Options.h"
+#include "TimeUtils.h"
+
+#include <random>
+
+namespace CEGAR {
+
+IncrementalLinearization::IncrementalLinearization( InputQuery &inputQuery, Engine *engine )
+    : _inputQuery( inputQuery )
+    , _engine( std::unique_ptr<Engine>( engine ) )
+    , _timeoutInMicroSeconds( 0 )
+    , _round( 0 )
+    , _numAdditionalEquations( 0 )
+    , _numAdditionalPLConstraints( 0 )
+    , _numConstraintsToRefine(
+          Options::get()->getInt( Options::NUM_CONSTRAINTS_TO_REFINE_INC_LIN ) )
+    , _refinementScalingFactor(
+          Options::get()->getFloat( Options::REFINEMENT_SCALING_FACTOR_INC_LIN ) )
+{
+    srand( Options::get()->getInt( Options::SEED ) );
+    for ( const auto &c : _inputQuery.getNonlinearConstraints() )
+        _nlConstraints.append( c );
+}
+
+void IncrementalLinearization::solve()
+{
+    /*
+      Invariants at the beginning of the loop:
+      1. _inputQuery contains the assignment in the previous refinement round
+      2. _timeoutInMicroSeconds is positive
+    */
+    while ( true )
+    {
+        struct timespec start = TimeUtils::sampleMicro();
+
+        // Refine the non-linear constraints using the counter-example stored
+        // in the _inputQuery
+        InputQuery refinement;
+        refinement.setNumberOfVariables( _inputQuery.getNumberOfVariables() );
+        _engine->extractSolution( refinement );
+        _engine->extractBounds( refinement );
+        unsigned numRefined = refine( refinement );
+
+        printStatus();
+        if ( numRefined == 0 )
+            return;
+
+        // Create a new engine
+        _engine = std::unique_ptr<Engine>( new Engine() );
+        _engine->setVerbosity( 0 );
+
+        // Solve the refined abstraction
+        if ( _engine->processInputQuery( _inputQuery ) )
+        {
+            double timeoutInSeconds =
+                static_cast<long double>( _timeoutInMicroSeconds ) / MICROSECONDS_TO_SECONDS;
+            INCREMENTAL_LINEARIZATION_LOG(
+                Stringf( "Solving with timeout %.2f seconds", timeoutInSeconds ).ascii() );
+            _engine->solve( timeoutInSeconds );
+        }
+
+        if ( _engine->getExitCode() == IEngine::UNKNOWN )
+        {
+            unsigned long long timePassed =
+                TimeUtils::timePassed( start, TimeUtils::sampleMicro() );
+            if ( timePassed >= _timeoutInMicroSeconds )
+            {
+                // Enter another round but should quit immediately.
+                _timeoutInMicroSeconds = 1;
+            }
+            else
+                _timeoutInMicroSeconds -= TimeUtils::timePassed( start, TimeUtils::sampleMicro() );
+            _numConstraintsToRefine =
+                std::min( _nlConstraints.size(),
+                          (unsigned)( _numConstraintsToRefine * _refinementScalingFactor ) );
+        }
+        else
+            return;
+    }
+}
+
+unsigned IncrementalLinearization::refine( InputQuery &refinement )
+{
+    INCREMENTAL_LINEARIZATION_LOG( "Performing abstraction refinement..." );
+
+    unsigned numRefined = 0;
+    for ( const auto &nlc : _nlConstraints )
+    {
+        numRefined += nlc->attemptToRefine( refinement );
+        if ( numRefined >= _numConstraintsToRefine )
+            break;
+    }
+    _inputQuery.setNumberOfVariables( refinement.getNumberOfVariables() );
+    for ( const auto &e : refinement.getEquations() )
+        _inputQuery.addEquation( e );
+    _numAdditionalEquations += refinement.getEquations().size();
+
+    for ( const auto &plc : refinement.getPiecewiseLinearConstraints() )
+    {
+        _inputQuery.addPiecewiseLinearConstraint( plc );
+    }
+    _numAdditionalPLConstraints += refinement.getPiecewiseLinearConstraints().size();
+    // Ownership of the additional constraints are transferred.
+    refinement.getPiecewiseLinearConstraints().clear();
+
+    INCREMENTAL_LINEARIZATION_LOG(
+        Stringf( "Refined %u non-linear constraints", numRefined ).ascii() );
+    return numRefined;
+}
+
+void IncrementalLinearization::printStatus()
+{
+    printf( "\n--- Incremental linearization round %u ---\n", ++_round );
+    printf( "Added %u equations, %u piecewise-linear constraints.\n",
+            _numAdditionalEquations,
+            _numAdditionalPLConstraints );
+}
+
+Engine *IncrementalLinearization::releaseEngine()
+{
+    return _engine.release();
+}
+
+void IncrementalLinearization::setInitialTimeoutInMicroSeconds(
+    unsigned long long timeoutInMicroSeconds )
+{
+    _timeoutInMicroSeconds =
+        ( timeoutInMicroSeconds == 0 ? FloatUtils::infinity() : timeoutInMicroSeconds );
+}
+
+} // namespace CEGAR
diff --git a/src/cegar/IncrementalLinearization.h b/src/cegar/IncrementalLinearization.h
@@ -0,0 +1,86 @@
+/*********************                                                        */
+/*! \file IncrementalLinearization.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Teruhiro Tagomori, Andrew Wu
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2017-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+ **/
+
+#ifndef __IncrementalLinearization_h__
+#define __IncrementalLinearization_h__
+
+#include "InputQuery.h"
+#include "MStringf.h"
+#include "Map.h"
+
+#define INCREMENTAL_LINEARIZATION_LOG( x, ... )                                                    \
+    LOG( GlobalConfiguration::CEGAR_LOGGING, "IncrementalLinearization: %s\n", x )
+
+class Engine;
+class InputQuery;
+
+namespace CEGAR {
+
+class IncrementalLinearization
+{
+public:
+    enum {
+        MICROSECONDS_TO_SECONDS = 1000000,
+    };
+
+    IncrementalLinearization( InputQuery &inputQuery, Engine *engine );
+
+    /*
+      Solve with incremental linarizations.
+      Only for the purpose of Nonlinear Constraints
+    */
+    void solve();
+
+    Engine *releaseEngine();
+
+    void setInitialTimeoutInMicroSeconds( unsigned long long timeoutInMicroSeconds );
+
+    /*
+      Refine the abstraction by adding constraints to exclude
+      the counter-example related to the given constraint
+
+      Returns the number of refined non-linear constraints
+    */
+    unsigned refine( InputQuery &inputQuery );
+
+private:
+    InputQuery &_inputQuery;
+    std::unique_ptr<Engine> _engine;
+
+    /*
+      A local copy of all the non-linear constraints in _inputQuery
+    */
+    Vector<NonlinearConstraint *> _nlConstraints;
+
+    unsigned long long _timeoutInMicroSeconds;
+
+    // How many rounds of incremental linearization have been performed
+    unsigned _round;
+
+    // Number of additional equations
+    unsigned _numAdditionalEquations;
+    // Number of additional piecewise-linear constraints
+    unsigned _numAdditionalPLConstraints;
+
+    // Hyper-parmeters of incremental linearization
+    unsigned _numConstraintsToRefine;
+    double _refinementScalingFactor;
+
+    void printStatus();
+};
+
+} // namespace CEGAR
+
+
+#endif // __IncrementalLinearization_h__