Add Guroby encoder for max constratints. #402

tagomaru · 2020-11-05T21:52:22Z

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

This PR is going to add Guroby encoder for max constraints.

Sample NNET:

// simple_model 
2,2,3,3,
2,2,3,
0,
-100000.0,-100000.0,
100000.0,100000.0,
0.0,0.0,0.0,
1.0,1.0,1.0,
1.0,1.0,
-1.0,-1.0,
0.0,
0.0,
2.0,-1.0,
-1.0,1.0,
1.0,-1.0,
0.0,
0.0,
0.0,

Sample Code:

from maraboupy import Marabou as marabou
nnet_file_name = "./simple_model.nnet"
net = marabou.read_nnet(nnet_file_name)
net.setLowerBound(net.outputVars[0][0], 2)
net.setUpperBound(net.outputVars[0][0], 2)
net.setLowerBound(net.inputVars[0][0], 1)
net.setUpperBound(net.inputVars[0][0], 1)
net.addMaxConstraint(set(net.outputVars[0]), net.outputVars[0][0])
options = marabou.createOptions(solveWithMILP=True)
vals, stats = net.solve(options=options)

Test with the above sample code:

command

python3 guroby_max.py

result

...

sat
input 0 = 1.0
input 1 = -0.0
output 0 = 2.0
output 1 = -1.0
output 2 = 1.0

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

wu-haoze · 2020-11-08T20:56:58Z

src/engine/MILPEncoder.cpp

+    }
+
+    return ubs[umaxIndex];  
+}


Add a new line here

wu-haoze · 2020-11-08T21:11:23Z

src/engine/MILPEncoder.cpp

+    unsigned i = 0;
+    for ( const auto &x : xs ) {
+        // add binary variable
+        gurobi.addVariable( Stringf( "a%u", x ),


Naming the auxiliary variable like this would result in duplicated variable names. For instance, if we have two Max constraints Max([x1,x2], x4) and Max([x1,x3], x5), we would introduce the variable a1 twice, while we actually need two fresh variables.
One solution is to keep track of the latest index of the auxiliary variable. Please check the encodeReLUConstraint() method above.

wu-haoze · 2020-11-08T21:13:27Z

src/engine/MILPEncoder.cpp

+        terms.clear();
+
+        // add constraint: y >= x_i
+        terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", y ) ) );


"y >= x_i" is already encoded as an inequality here:

Marabou/src/engine/MaxConstraint.cpp

Lines 489 to 515 in 3bf23be

void MaxConstraint::addAuxiliaryEquations( InputQuery &inputQuery )

{

for ( auto element : _elements )

{

// If element is equal to _f, skip this step.

// The reason is to avoid adding equations like `1.00x00 -1.00x00 -1.00x01 = 0.00`.

if ( element == _f )

continue;

// Create an aux variable

unsigned auxVariable = inputQuery.getNumberOfVariables();

inputQuery.setNumberOfVariables( auxVariable + 1 );

// f >= element, or f - elemenet - aux = 0, for non-negative aux

Equation equation( Equation::EQ );

equation.addAddend( 1.0, _f );

equation.addAddend( -1.0, element );

equation.addAddend( -1.0, auxVariable );

equation.setScalar( 0 );

inputQuery.addEquation( equation );

// Set the bounds for the aux variable

inputQuery.setLowerBound( auxVariable, 0 );

// Todo: upper bound for aux?

}

}

.
I think you could just remove line 182 - 188.

wu-haoze · 2020-11-08T21:13:51Z

src/engine/MILPEncoder.cpp

+    }
+
+    return ubs[umaxIndex];  
+}


Add a newline here

wu-haoze · 2020-11-08T21:21:30Z

src/engine/MILPEncoder.cpp

+    i = 0;
+    for ( const auto &x : xs ) {
+        // add constraint: y <= x_i + (1 - a_i) * (umax - l)
+        double umax = getUmax( ubs, i, m );


if we store the <upper bound, variable> pair in a priority queue, we should be able to compute each Umax in O(log n) time. Currently it is computed in linear time, which might create overhead as the network size increases.

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

tagomaru · 2020-11-18T20:23:33Z

I changed this status to WIP since Test_preprocessor failed after merging master.

12/58 Test #16: Test_Preprocessor .................***Failed    1.07 sec
Assertion violation! File /Users/teruhiro/Documents/work/Marabou/src/engine/InputQuery.cpp, line 279

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

tagomaru · 2020-11-22T03:53:00Z

Evaluation result for CNN having max pooling layer:

1. MILP

Model

The onnx file (resources/onnx/cnn_max_mninst2.onnx) of the model was converted from resources/keras/cnn_max_mnist2.h5.

model = models.Sequential()
model.add(layers.Conv2D(8, (4, 4), activation='relu', input_shape=(28, 28, 1)))
model.add(layers.Conv2D(4, (4, 4), activation='relu'))
model.add(layers.MaxPooling2D((2, 2)))
model.add(layers.Flatten())
model.add(layers.Dense(32, activation='relu'))
model.add(layers.Dense(10, activation='softmax'))

softmax was changed to linear function after compile.

Test program (onnx_cnn_max_mnist2.py)

from maraboupy import Marabou
import numpy as np

options = Marabou.createOptions(verbosity = 2, solveWithMILP=True)
filename = 'cnn_max_mninst2.onnx'
network = Marabou.read_onnx(filename)

inputVars = network.inputVars[0][0]
outputVars = network.outputVars[0]

delta = 0.1
for h in range(inputVars.shape[0]):
    for w in range(inputVars.shape[1]):
        network.setLowerBound(inputVars[h][w][0], 0.5-delta)
        network.setUpperBound(inputVars[h][w][0], 0.5+delta)

# network.setLowerBound(outputVars[0], 1.0)

vals, stats = network.solve(options = options)
assert len(vals) > 0

dataONNX = np.zeros(inputVars.shape)
for i in range(inputVars.shape[0]):
    for j in range(inputVars.shape[1]):
        dataONNX[i][j][0] = vals[28 * i + j]

onnxEval = network.evaluateWithoutMarabou([dataONNX])

print('\nonnx output:\n', onnxEval)

Execution

$ /usr/bin/time -l python3 onnx_cnn_max_mnist2.py
(removed)
output 0 = -0.11791291526924269
output 1 = -0.1608994968618801
output 2 = -3.053131166312996
output 3 = -1.9990824676561814
output 4 = 1.0521385098435299
output 5 = -1.4255639982065038
output 6 = 0.02008915031516549
output 7 = -1.215866175485384
output 8 = -0.7083881322782134
output 9 = -0.47855364129358235

onnx output:
 [[-0.11791354 -0.1609008  -3.0531301  -1.9990811   1.0521375  -1.4255633
   0.02008897 -1.2158666  -0.7083874  -0.47855455]]
    96692.76 real     93300.76 user       412.88 sys
12301275136  maximum resident set size
         0  average shared memory size
         0  average unshared data size
         0  average unshared stack size
   8717705  page reclaims
      1576  page faults
         0  swaps
         0  block input operations
         0  block output operations
         0  messages sent
         0  messages received
         0  signals received
     12856  voluntary context switches
  19258691  involuntary context switches

Elapsed time

Total 27 hours. (20 hours until preprocess was done)

2. Marabou

7 DAYS has passed, but it did not finish.
I killed the process.

wu-haoze · 2020-11-24T20:09:32Z

src/engine/InputQuery.cpp

+                _plConstraints.append( newPlc );
+                ++numberOfDisjunctions;
+            }
+            else if ( constraint->getType() == MAX &&


I think we assume that network level reasoner can pick up all the Max constraint. Maybe just remove the logic for Max here?

Your understanding is right.
However, when the network reasoner is true, the below part also picks up max constraints.
To avoid to pick up doubly, this neglects max constraints here.

for ( const auto &constraint : other._networkLevelReasoner-> getConstraintsInTopologicalOrder() ) { auto *newPlc = constraint->duplicateConstraint(); _plConstraints.append( newPlc ); _networkLevelReasoner->addConstraintInTopologicalOrder( newPlc ); }

Does it make sense?

wu-haoze · 2020-11-24T20:16:13Z

src/engine/MILPEncoder.cpp

+    for ( const auto &x : xs ) 
+    {
+        // add binary variable
+        gurobi.addVariable( Stringf( "a%u_%u", _binVarIndex, x ),


Please explain the name convention for future reference.

wu-haoze · 2020-11-24T20:17:09Z

src/engine/MILPEncoder.h

@@ -51,6 +51,8 @@ class MILPEncoder
    */
    Map<unsigned, String> _variableToVariableName;

+    unsigned _binVarIndex = 0;


Add documentation.

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

* Add Guroby encoder for max constratints. Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * change indents Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * fix error on windows Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * cosmetic Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * improvement Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * do not count max constratints doubly Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * fix bug Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * change comment Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * add h5 and onnx files Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * add comments for bin vars Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * add onnx and keras files for evaluation Signed-off-by: tagomaru <tagomaru@users.noreply.github.com> * Update InputQuery.h Co-authored-by: Haoze(Andrew) Wu <haozewu@stanford.edu>

Add Guroby encoder for max constratints.

0275e98

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

tagomaru requested a review from wu-haoze November 5, 2020 21:52

tagomaru added 3 commits November 5, 2020 13:57

change indents

8a5c3ea

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

fix error on windows

afcd646

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

cosmetic

35fd279

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

wu-haoze requested changes Nov 8, 2020

View reviewed changes

tagomaru added 2 commits November 10, 2020 23:41

improvement

ef74682

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

merge master

5ee3371

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

tagomaru changed the title ~~Add Guroby encoder for max constratints.~~ WIP Add Guroby encoder for max constratints. Nov 18, 2020

tagomaru added 2 commits November 18, 2020 22:30

do not count max constratints doubly

173990e

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

fix bug

f2154b3

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

tagomaru changed the title ~~WIP Add Guroby encoder for max constratints.~~ Add Guroby encoder for max constratints. Nov 20, 2020

tagomaru added 2 commits November 20, 2020 13:23

change comment

3553662

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

add h5 and onnx files

33dbaec

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

wu-haoze approved these changes Nov 24, 2020

View reviewed changes

tagomaru and others added 4 commits December 3, 2020 11:38

add comments for bin vars

476f2f9

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

add onnx and keras files for evaluation

9112a4b

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

Update InputQuery.h

0473cf6

Merge branch 'master' into gurobi-max-constraint

588d6f2

wu-haoze merged commit 163ef59 into NeuralNetworkVerification:master Jan 8, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add Guroby encoder for max constratints. #402

Add Guroby encoder for max constratints. #402

tagomaru commented Nov 5, 2020

wu-haoze Nov 8, 2020

tagomaru Nov 9, 2020

tagomaru Nov 16, 2020

wu-haoze Nov 8, 2020

tagomaru Nov 9, 2020

tagomaru Nov 16, 2020

wu-haoze Nov 8, 2020

tagomaru Nov 9, 2020

tagomaru Nov 16, 2020

wu-haoze Nov 8, 2020

tagomaru Nov 9, 2020

tagomaru Nov 16, 2020

wu-haoze Nov 8, 2020

tagomaru Nov 11, 2020

tagomaru commented Nov 18, 2020

tagomaru commented Nov 22, 2020 •

edited

Loading

wu-haoze Nov 24, 2020

tagomaru Dec 3, 2020

wu-haoze Nov 24, 2020

tagomaru Dec 3, 2020

wu-haoze Nov 24, 2020

tagomaru Dec 3, 2020

	void MaxConstraint::addAuxiliaryEquations( InputQuery &inputQuery )
	{
	for ( auto element : _elements )
	{
	// If element is equal to _f, skip this step.
	// The reason is to avoid adding equations like `1.00x00 -1.00x00 -1.00x01 = 0.00`.
	if ( element == _f )
	continue;

	// Create an aux variable
	unsigned auxVariable = inputQuery.getNumberOfVariables();
	inputQuery.setNumberOfVariables( auxVariable + 1 );

	// f >= element, or f - elemenet - aux = 0, for non-negative aux
	Equation equation( Equation::EQ );
	equation.addAddend( 1.0, _f );
	equation.addAddend( -1.0, element );
	equation.addAddend( -1.0, auxVariable );
	equation.setScalar( 0 );
	inputQuery.addEquation( equation );

	// Set the bounds for the aux variable
	inputQuery.setLowerBound( auxVariable, 0 );

	// Todo: upper bound for aux?
	}
	}

Add Guroby encoder for max constratints. #402

Add Guroby encoder for max constratints. #402

Conversation

tagomaru commented Nov 5, 2020

Sample NNET:

Sample Code:

Test with the above sample code:

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tagomaru commented Nov 18, 2020

tagomaru commented Nov 22, 2020 • edited Loading

Evaluation result for CNN having max pooling layer:

1. MILP

Model

Test program (onnx_cnn_max_mnist2.py)

Execution

Elapsed time

2. Marabou

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

tagomaru commented Nov 22, 2020 •

edited

Loading