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.

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

Deeppoly analysis #420

Merged
merged 68 commits into from
Jan 13, 2021
Merged

Conversation

wu-haoze
Copy link
Collaborator

@wu-haoze wu-haoze commented Jan 6, 2021

Adding support for deeppoly analysis for ReLU activation described in https://files.sri.inf.ethz.ch/website/papers/DeepPoly.pdf.

  1. Currently supporting six abstract transformers (DeepPoly{ReLU, WeightedSum, Input, MaxPool, Absolute, Sign}Element.h).
  2. DeepPolyAnalysis.h contains the method to run the abstract interpretation.
  3. Adding an option to choose whether to use sbt or deeppoly or none during the search.
  4. Adding an option to print out bounds for each neuron after preprocessing (this would help comparing different bound tightening passes).

maraboupy/MarabouCore.cpp Outdated Show resolved Hide resolved
src/configuration/GlobalConfiguration.cpp Outdated Show resolved Hide resolved
src/engine/Engine.cpp Show resolved Hide resolved
src/nlr/DeepPolyAbsoluteValueElement.cpp Outdated Show resolved Hide resolved
src/nlr/DeepPolyAnalysis.cpp Outdated Show resolved Hide resolved
src/nlr/DeepPolyAnalysis.cpp Show resolved Hide resolved
src/nlr/DeepPolyWeightedSumElement.cpp Outdated Show resolved Hide resolved
src/nlr/DeepPolySignElement.cpp Outdated Show resolved Hide resolved
src/nlr/NetworkLevelReasoner.h Outdated Show resolved Hide resolved
src/nlr/DeepPolyMaxPoolElement.cpp Show resolved Hide resolved
src/nlr/DeepPolyMaxPoolElement.cpp Show resolved Hide resolved
@wu-haoze wu-haoze merged commit 3ae3237 into NeuralNetworkVerification:master Jan 13, 2021
@wu-haoze wu-haoze deleted the deeppoly branch January 13, 2021 04:28
matanost pushed a commit that referenced this pull request Nov 2, 2021
* dump bounds

* clean up

* add deep poly element class

* add more execution

* Memory allocation

* constructor

* documentation

* ws

* symbolicBoundsInTermsOfPredecessor

* symbolic in terms of predecessor

* clean up

* clean up

* first attempt

* clean up

* add log

* clean up

* clean up

* clean up

* clean up

* option

* option

* options

* clean up

* remove print statements

* clean up deep poly analysis

* clean up deep poly elements (WIP)

* clean up

* cleaned up ws element

* clean up

* Documentation

* add test for DeepPolyAnalysis

* update unit test

* disable logging

* change default values in option

* add options to python api

* remove symbolic bound trightening type

* fix indentation

* sign constraint

* absolute value

* clean up

* better ways to get source index in ReLU, Absolute, and Sign

* refactoring get source layers

* clean up

* minor

* update in DeepPolySignElement

* max element

* print source layer in dump topology

* source layer dependency

* residual

* wip residual

* residual layers

* progress toward residual layer

* add more tests

* residual

* addressing Guy's cosmetic comments

* construct deep poly only once

* turn off logging

* more tests for max constraints

* Clean up and more documentation

* minor

* optimization in backsubstitution resulting in tighter bounds

* fix test

* minor

Co-authored-by: Guy Katz <guykatz@cs.huji.ac.il>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants