Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Sigmoid support Ph1 #483

Merged
merged 9 commits into from
Nov 29, 2021
Merged

Sigmoid support Ph1 #483

merged 9 commits into from
Nov 29, 2021

Conversation

tagomaru
Copy link
Contributor

@tagomaru tagomaru commented Oct 26, 2021 •
edited
Loading

This PR is going to support sigmoid with DeepPoly.
Please note this can support only some UNSAT cases in not a complete but sound way.

Toy model for test

onnx: resources/onnx/fc_2-2sigmoids-3.onnx
keras: resources/keras/fc_2-2sigmoids-3.h5

image

UNSAT case

Python code

from maraboupy import Marabou
import numpy as np

# load network
filename = '../../resources/onnx/fc_2-2sigmoids-3.onnx'
network = Marabou.read_onnx(filename)

inputVars = network.inputVars[0][0]
outputVars = network.outputVars[0]
network.setLowerBound(inputVars[0], 1)
network.setUpperBound(inputVars[0], 1)
network.setLowerBound(inputVars[1], 0)
network.setUpperBound(inputVars[1], 0)
network.setUpperBound(outputVars[0], 1) # CAUSE VIOLATION

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

vals, stats = network.solve(options = options)

Result

...
Layer 0:
        Neuron1 LB: 1.0000, UB: 1.0000 
        Neuron2 LB: 0.0000, UB: 0.0000 

Layer 1:
        Neuron1 LB: 1.0000, UB: 1.0000 
        Neuron2 LB: -1.0000, UB: -1.0000 

Layer 2:
        Neuron1 LB: 0.7311, UB: 0.7311 
        Neuron2 LB: 0.2689, UB: 0.2689 

Layer 3:
        Neuron1 LB: 1.1932, UB: 1.0000 
        Neuron2 LB: -0.4621, UB: -0.4621 
        Neuron3 LB: 0.4621, UB: 0.4621 

Violation at Neuron_0 of Layer_3 - LB: 1.19, UB: 1.00
unsat

This caused a violation at Neuron_0 of Layer_3 since LB > UB there.

UNKNOWN case

Python code

from maraboupy import Marabou
import numpy as np

# load network
filename = '../../resources/onnx/fc_2-2sigmoids-3.onnx'
network = Marabou.read_onnx(filename)

inputVars = network.inputVars[0][0]
outputVars = network.outputVars[0]
network.setLowerBound(inputVars[0], 1)
network.setUpperBound(inputVars[0], 1)
network.setLowerBound(inputVars[1], 0)
network.setUpperBound(inputVars[1], 0)
network.setUpperBound(outputVars[0], 2) # NOT CAUSE VIOLATION

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

vals, stats = network.solve(options = options)

Result

Layer 0:
        Neuron1 LB: 1.0000, UB: 1.0000 
        Neuron2 LB: 0.0000, UB: 0.0000 

Layer 1:
        Neuron1 LB: 1.0000, UB: 1.0000 
        Neuron2 LB: -1.0000, UB: -1.0000 

Layer 2:
        Neuron1 LB: 0.7311, UB: 0.7311 
        Neuron2 LB: 0.2689, UB: 0.2689 

Layer 3:
        Neuron1 LB: 1.1932, UB: 1.1932 
        Neuron2 LB: -0.4621, UB: -0.4621 
        Neuron3 LB: 0.4621, UB: 0.4621 

Caught a MarabouError. Code: 900. Message: Marabou doesn't support sigmoid except some UNSAT cases yet.
unsat

This caused MarabouError since Marabou couldn't determine whether this was UNSAT. (Actually this case should be SAT, but It doesn't support SAT case yet.)

@tagomaru
initial commit for ph1
04ab4e3 
Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>
@tagomaru
Sigmoid support Ph1
95de338 
Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>
@tagomaru
remove some comments
8cb2547 
Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>
@wu-haoze wu-haoze self-requested a review October 26, 2021 21:29
wu-haoze
wu-haoze requested changes Nov 5, 2021
View reviewed changes
maraboupy/Marabou.py Outdated Show resolved Hide resolved
src/engine/Engine.cpp Outdated
@@ -1204,6 +1209,10 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess )
}
});

// TODO: Remove this block after getting ready to support sigmoid with MILP.
if ( _exitCode != Engine::UNSAT && inputQuery.getTranscendentalConstraints().size() > 0 )
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we reach here we know that _exitCode != Engine::UNSAT, so we can remove this first condition

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

removed the first check and moved this condition check to solve method.

src/engine/MILPEncoder.cpp Outdated
@@ -58,6 +58,22 @@ void MILPEncoder::encodeInputQuery( GurobiWrapper &gurobi,
"Only ReLU and Max are supported\n" );
}
}

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems this file doesn't need to change in this PR. Maybe remove the comments?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

removed.

src/engine/MILPEncoder.cpp Outdated
@@ -187,3 +203,8 @@ void MILPEncoder::encodeMaxConstraint( GurobiWrapper &gurobi, MaxConstraint *max
}
_binVarIndex++;
}

// TODO:
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remove the comment?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

removed.

src/engine/TranscendentalConstraint.h Outdated
#endif // __TranscendentalConstraint_h__

//
// Local Variables:
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are no longer needed since we switched to cmake

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

removed.

src/engine/SigmoidConstraint.cpp Show resolved Hide resolved
src/engine/tests/Test_SigmoidConstraint.h Show resolved Hide resolved
src/engine/Engine.cpp Outdated
@@ -1182,6 +1182,11 @@ bool Engine::processInputQuery( InputQuery &inputQuery, bool preprocess )

struct timespec end = TimeUtils::sampleMicro();
_statistics.setPreprocessingTime( TimeUtils::timePassed( start, end ) );

// check bound violations of all variables
if ( Options::get()->getBool( Options::CHECK_BOUNDS_BEFORE_SOLVE ) )
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

it is not necessary to conduct this check, because if an invalid bound is derived by DeepPoly, an InfeasibleQueryException will be throw.
See the method Engine::performSymbolicBoundTightening() (in particular Tableau::tightenLowerBound())

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

removed.

src/nlr/NetworkLevelReasoner.cpp Outdated
@@ -289,6 +290,26 @@ void NetworkLevelReasoner::dumpTopology() const
layer.second->dump();
}

void NetworkLevelReasoner::checkBoundsViolations()
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As mentioned in previous comment, this method would not be necessary.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

removed.

@tagomaru
remove checkBounds and etc
1720c03 
Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>
@tagomaru
Merge branch 'master' into sigmoid-support
a21f662
@tagomaru
fix memory leak
516e818 
Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>
@tagomaru
add some tests
30c1ba9 
Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>
wu-haoze
wu-haoze requested changes Nov 22, 2021
View reviewed changes
maraboupy/test/test_network.py Show resolved Hide resolved
src/engine/Engine.cpp Show resolved Hide resolved
src/engine/tests/Test_SigmoidConstraint.h Show resolved Hide resolved
@tagomaru
relect andrew's comments
58d79d6 
Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>
@tagomaru
Merge branch 'master' into sigmoid-support
6c3b0b7
@wu-haoze wu-haoze merged commit b217b7f into NeuralNetworkVerification:master Nov 29, 2021
omriisack pushed a commit to omriisack/Marabou that referenced this pull request Feb 6, 2022
@tagomaru @OmriIsacHUJI
Sigmoid support Ph1 (NeuralNetworkVerification#483)
41b904f 
* initial commit for ph1

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

* Sigmoid support Ph1

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

* remove some comments

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

* remove checkBounds and etc

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

* fix memory leak

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

* add some tests

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

* relect andrew's comments

Signed-off-by: tagomaru <tagomaru@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@wu-haoze wu-haoze wu-haoze approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@tagomaru @wu-haoze