Sigmoid support with linearization #492

tagomaru · 2021-12-04T02:10:10Z

This PR is going to support sigmoid constraints with linearization approach.

How does it work?

The below example test code shows how it works.

test_mnist_model_with_sigmoids.py

from maraboupy import Marabou
import numpy as np

# load network
filename = '../../resources/onnx/robust_model_sigmoid_linear.onnx'
network = Marabou.read_onnx(filename)

options = Marabou.createOptions(
    verbosity=0,
    solveWithMILP=True,
    milpTightening="none")

input = np.ones([28, 28]) * 0.5

# UNSAT
vals, stats, maxClass = network.evaluateLocalRobustness(
    input=input, 
    epsilon=0.05,
    originalClass=5,
    options=options,
    targetClass=2)

# UNKNOWN
vals, stats, maxClass = network.evaluateLocalRobustness(
    input=input, 
    epsilon=0.1,
    originalClass=5,
    options=options,
    targetClass=1)

robust_model_sigmoid_linear.onnx is mnist classifier of input -> hidden1(64 sigmoids) -> hidden2(32 sigmoids) -> output.
It was trained by an adversarial training with PGD attack of epsilon 0.1.
Accuracy of test data is 0.9543, and accuracy of PGD test data is 0.8546.

Result

$ python test_mnist_model_with_sigmoids.py 
(removed...)
Academic license - for non-commercial use only - expires 2022-08-26
unsat
Academic license - for non-commercial use only - expires 2022-08-26
Caught a MarabouError. Code: 900. Message: UNKNOWN (Marabou doesn't support UNKNOWN cases with exitCode yet.)
unsat

unsat: Solution was not found even in overapproximated linearization way.
unknown: Solution was found in overapproximated linearization way. So unknown whether the result of the original query is SAT or UNSAT.

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

wu-haoze · 2022-01-14T16:47:21Z

resources/bnn_queries/smallBNN_original

@@ -3,6 +3,7 @@
 1628
 1668
 1628
+0


What is this change?

Ah I think I understand. It denotes the number of transcendental constraints.

src/common/GurobiWrapper.h

src/engine/Engine.cpp

wu-haoze · 2022-01-14T18:04:46Z

src/engine/InputQuery.cpp


    printf( "Number of variables: %u\n", _numberOfVariables );
    printf( "Number of lower bounds: %u\n", _lowerBounds.size() );
    printf( "Number of upper bounds: %u\n", _upperBounds.size() );
    printf( "Number of equations: %u\n", _equations.size() );
-    printf( "Number of constraints: %u\n", _plConstraints.size() );
+    printf( "Number of piecewise-linear constraints: %u\n", _plConstraints.size() );
+    printf( "Number of transcendental constraints: %u\n", _tsConstraints.size() );


Maybe we can just replace _plConstraints with _nonLinearConstaints which include both the PL constraints and the transcendental constraints. This way the previously generated input query file would remain valid.

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

wu-haoze · 2022-01-17T20:01:30Z

src/engine/MILPEncoder.cpp

+    double sourceLb = _tableau.getLowerBound( sourceVariable );
+    double sourceUb = _tableau.getUpperBound( sourceVariable );
+
+    if ( sourceLb < 0 && sourceUb > 0 )


Use FloatUtils::gt() and FloatUtils::lt() instead of <, >

Marabou/src/common/FloatUtils.h

Line 89 in 9c08e9c

static bool lt( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )

wu-haoze · 2022-01-17T20:01:45Z

src/engine/MILPEncoder.cpp

+    if ( sourceLb < 0 && sourceUb > 0 )
+    {
+        List<GurobiWrapper::Term> terms;
+        String binVarName = Stringf( "a%u", _binVarIndex ); // a = 1 -> the caes where x_b >= 0, otherwise where x_b <= 0


caes -> case

wu-haoze · 2022-01-17T20:02:43Z

src/engine/MILPEncoder.cpp

+        int binVal = 1;
+
+        // tangent line: x_f = tangentSlope * (x_b - tangentPoint) + yAtTangentPoint
+        double tangentPoint = ( 0 + sourceUb ) / 2;


( 0 + sourceUb ) / 2 => sourceUb / 2

wu-haoze · 2022-01-17T20:06:07Z

src/engine/MILPEncoder.cpp

+        gurobi.addGeqIndicatorConstraint( binVarName, binVal, terms, 0 );  
+        terms.clear(); 
+
+        // upper bound of x_b


Addition of the upper bound is redundant?

wu-haoze · 2022-01-17T20:07:11Z

src/engine/MILPEncoder.cpp

+        gurobi.addGeqIndicatorConstraint( binVarName, binVal, terms, y_l );  
+        terms.clear(); 
+
+        // upper bound of x_f


Similarly, this should be redundant?

wu-haoze · 2022-01-17T20:07:52Z

src/engine/MILPEncoder.cpp

+                            0,
+                            1,
+                            GurobiWrapper::BINARY );
+        //


Remove extra // to be consistent with rest of the code base?

wu-haoze · 2022-01-17T20:08:25Z

src/engine/MILPEncoder.cpp

+        binVal = 0;
+
+        // tangent line: x_f = tangentSlope * (x_b - tangentPoint) + yAtTangentPoint
+        tangentPoint = ( sourceLb + 0 ) / 2;


tangentPoint = sourceLb / 2

wu-haoze · 2022-01-17T20:09:45Z

src/engine/MILPEncoder.cpp

+        terms.clear();
+
+        // secant line: x_f = secantSlope * (x_b - sourceLb) + y_l
+        y_u = sigmoid->sigmoid( 0 );


No need to recompute this? Instead, y_u = y_l

wu-haoze · 2022-01-17T20:10:22Z

src/engine/MILPEncoder.cpp

+        gurobi.addLeqIndicatorConstraint( binVarName, binVal, terms, y_u );  
+        terms.clear();       
+
+        //


Remove extra //

wu-haoze · 2022-01-17T20:11:21Z

src/engine/MILPEncoder.cpp

+        gurobi.addLeqIndicatorConstraint( binVarName, binVal, terms, -secantSlope * sourceLb + y_l );
+        terms.clear();
+
+        // lower bound of x_b


Similarly, there is no need to add lowerbounds for x_b and x_f in this case?

wu-haoze · 2022-01-17T20:13:21Z

src/engine/MILPEncoder.cpp

+    terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", targetVariable ) ) );
+    terms.append( GurobiWrapper::Term( -tangentSlope, Stringf( "x%u", sourceVariable ) ) );
+
+    if ( sourceLb >= 0 )


Use FloatUtils::gte

Marabou/src/common/FloatUtils.h

Line 84 in 9c08e9c

static bool gte( double x, double y, double epsilon = GlobalConfiguration::DEFAULT_EPSILON_FOR_COMPARISONS )

wu-haoze · 2022-01-17T20:14:52Z

src/engine/MILPEncoder.cpp

+    {
+        gurobi.addLeqConstraint( terms, -tangentSlope * tangentPoint + yAtTangentPoint );
+    }
+    else if ( sourceUb <= 0 )


else if ( sourceUb <= 0 ) => else

src/engine/MILPEncoder.cpp

wu-haoze · 2022-01-17T20:18:23Z

src/engine/MILPEncoder.cpp

+    double y_l = sigmoid->sigmoid( sourceLb );
+    double y_u = sigmoid->sigmoid( sourceUb );
+
+    if ( sourceUb != sourceLb )


Maybe handle the case of "sourceUb == sourceLb" in the very beginning of this method?

wu-haoze · 2022-01-17T20:20:21Z

src/engine/MILPEncoder.cpp

+        terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", targetVariable ) ) );
+        terms.append( GurobiWrapper::Term( -secantSlope, Stringf( "x%u", sourceVariable ) ) );
+
+        if ( sourceLb >= 0 )


Use FloatUtils::gte

wu-haoze · 2022-01-17T20:20:29Z

src/engine/MILPEncoder.cpp

+        {
+            gurobi.addGeqConstraint( terms, -secantSlope * sourceLb + y_l );
+        }
+        else if ( sourceUb <= 0 )


else if ( sourceUb <= 0 ) => else

wu-haoze

Overall looks good and the implementation looks correct. I have a few more minor comments though for code readability/efficiency.

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

* linearlization done, but queryLoader not yet Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * QueryLoader Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * robust_model_sigmoid_linear Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * remove debug print Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * fixed some bugs and removed codes supporting unknown Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * explicitly include GurobiWrapper.h in MILPEncoder.cpp Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * updating GurobiWrapper.h to make a compiler detect the update Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * update indent Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * rollback Marabou.py Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * change ci.yml Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * fix ci error Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * add interfaces in GurobiWrapper Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * fix queryloader bug Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * rollback queryloader stuff Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * reflect Andrew's comments Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> Co-authored-by: Haoze(Andrew) Wu <haozewu@stanford.edu>

tagomaru added 15 commits December 3, 2021 16:21

linearlization done, but queryLoader not yet

902b9bc

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

QueryLoader

7b9dc27

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

robust_model_sigmoid_linear

761c225

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

remove debug print

b10130f

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

Merge branch 'master' into sigmoid-spport-linerlization

57ae081

Merge branch 'master' into sigmoid-spport-linerlization

9c28eab

fixed some bugs and removed codes supporting unknown

1fc5b94

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

explicitly include GurobiWrapper.h in MILPEncoder.cpp

3c6f73f

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

updating GurobiWrapper.h to make a compiler detect the update

229f083

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

update indent

31b9f74

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

rollback Marabou.py

557b312

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

change ci.yml

714afb1

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

fix ci error

2cc5ad2

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

add interfaces in GurobiWrapper

86b0348

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

fix queryloader bug

38fcae6

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

wu-haoze self-requested a review January 14, 2022 16:46

wu-haoze requested changes Jan 14, 2022

View reviewed changes

rollback queryloader stuff

b6f8ad4

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

wu-haoze reviewed Jan 17, 2022

View reviewed changes

src/engine/MILPEncoder.cpp Show resolved Hide resolved

wu-haoze reviewed Jan 17, 2022

View reviewed changes

wu-haoze and others added 2 commits January 17, 2022 12:22

Merge branch 'master' into sigmoid-spport-linerlization

a9337f2

reflect Andrew's comments

a06bc59

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>

wu-haoze approved these changes Jan 19, 2022

View reviewed changes

wu-haoze merged commit 6ef249d into NeuralNetworkVerification:master Jan 19, 2022

tagomaru deleted the sigmoid-spport-linerlization branch January 19, 2022 05:00

tagomaru restored the sigmoid-spport-linerlization branch March 4, 2022 18:22

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Sigmoid support with linearization #492

Sigmoid support with linearization #492

tagomaru commented Dec 4, 2021 •

edited

Loading

wu-haoze Jan 14, 2022

wu-haoze Jan 14, 2022

tagomaru Jan 14, 2022

wu-haoze Jan 14, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022 •

edited

Loading

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022 •

edited

Loading

wu-haoze Jan 17, 2022

wu-haoze Jan 17, 2022

wu-haoze left a comment

@@ @@ -3,6 +3,7 @@ @@
 
 
 
+

Sigmoid support with linearization #492

Sigmoid support with linearization #492

Conversation

tagomaru commented Dec 4, 2021 • edited Loading

How does it work?

test_mnist_model_with_sigmoids.py

Result

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

wu-haoze Jan 17, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

wu-haoze Jan 17, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

wu-haoze left a comment

Choose a reason for hiding this comment

tagomaru commented Dec 4, 2021 •

edited

Loading

wu-haoze Jan 17, 2022 •

edited

Loading

wu-haoze Jan 17, 2022 •

edited

Loading