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

Backward forward algorithm #845

Merged
merged 22 commits into from
Feb 13, 2025
Merged

Backward forward algorithm #845

Show file tree
Hide file tree
Changes from 17 commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
e00d517
Add files via upload
ido-shm-uel Oct 1, 2024
04cc0b1
Revert last change.
ido-shm-uel Oct 1, 2024
80be6dc
Added assginment, store-into-other NLR tests for every activation fun…
ido-shm-uel Oct 1, 2024
9fbca7b
Add files via upload
ido-shm-uel Oct 1, 2024
f7aee6d
Add files via upload
ido-shm-uel Oct 1, 2024
33f5d5f
Add files via upload
ido-shm-uel Oct 1, 2024
6d1c898
Add files via upload
ido-shm-uel Oct 1, 2024
ee5dd00
0-4-0: Implementing symbolic bound tightening for every activation fu…
ido-shm-uel Oct 1, 2024
85fe8f3
0-4-1: Adding symbolic bound tightening tests for all activation func…
ido-shm-uel Oct 1, 2024
32d7c52
0-5-0: Adding rounding constant for LP relaxation propagation.
ido-shm-uel Oct 1, 2024
5a7c5d8
0-5-1: Implementing forward-backward LP propagation algorithm for all…
ido-shm-uel Oct 1, 2024
79f7a84
0-5-2: Adding forward-backward LP propagation tests for all activatio…
ido-shm-uel Oct 1, 2024
a8c238d
0-5---3: Minor fix.
ido-shm-uel Oct 14, 2024
b20c410
0-5--4: Another fix.
ido-shm-uel Oct 31, 2024
0f49553
0-5---5: Fixing fix 0-5--4 for this branch.
ido-shm-uel Nov 6, 2024
e7af43d
0-5---6: Corrections in Backward-Forward Algorithm, SBT
ido-shm-uel Nov 12, 2024
72e0687
Merge branch 'NeuralNetworkVerification:master' into Backward-Forward…
ido-shm-uel Dec 5, 2024
9f4de6c
0-5--7: clang-format
ido-shm-uel Dec 13, 2024
ca7a2fb
Merge pull request #3 from NeuralNetworkVerification/master
ido-shm-uel Feb 6, 2025
67ef78d
Update CHANGELOG.md
ido-shm-uel Feb 6, 2025
9b8b1bf
Update OptionParser.cpp
ido-shm-uel Feb 6, 2025
94aa3cb
Merge branch 'master' into Backward-Forward-Algorithm
wu-haoze Feb 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/configuration/GlobalConfiguration.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ const unsigned GlobalConfiguration::SIMULATION_RANDOM_SEED = 1;
const bool GlobalConfiguration::USE_HARRIS_RATIO_TEST = true;

const double GlobalConfiguration::SYMBOLIC_TIGHTENING_ROUNDING_CONSTANT = 0.00000000001;
const double GlobalConfiguration::LP_TIGHTENING_ROUNDING_CONSTANT = 0.00000001;

const double GlobalConfiguration::SIGMOID_CUTOFF_CONSTANT = 20;

Expand Down
3 changes: 2 additions & 1 deletion src/configuration/GlobalConfiguration.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -195,8 +195,9 @@ class GlobalConfiguration
Symbolic bound tightening options
*/

// Symbolic tightening rounding constant
// Symbolic tightening, LP rounding constants
static const double SYMBOLIC_TIGHTENING_ROUNDING_CONSTANT;
static const double LP_TIGHTENING_ROUNDING_CONSTANT;

static const double SIGMOID_CUTOFF_CONSTANT;

Expand Down
4 changes: 3 additions & 1 deletion src/engine/Engine.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1579,7 +1579,9 @@ void Engine::performMILPSolverBoundedTightening( Query *inputQuery )

// TODO: Remove this block after getting ready to support sigmoid with MILP Bound
// Tightening.
if ( _milpSolverBoundTighteningType != MILPSolverBoundTighteningType::NONE &&
if ( ( _milpSolverBoundTighteningType == MILPSolverBoundTighteningType::MILP_ENCODING ||
_milpSolverBoundTighteningType == MILPSolverBoundTighteningType::MILP_ENCODING_INCREMENTAL ||
_milpSolverBoundTighteningType == MILPSolverBoundTighteningType::ITERATIVE_PROPAGATION ) &&
_preprocessedQuery->getNonlinearConstraints().size() > 0 )
throw MarabouError( MarabouError::FEATURE_NOT_YET_SUPPORTED,
"Marabou doesn't support sigmoid with MILP Bound Tightening" );
Expand Down
560 changes: 554 additions & 6 deletions src/nlr/LPFormulator.cpp
View file
Open in desktop

Large diffs are not rendered by default.

17 changes: 16 additions & 1 deletion src/nlr/LPFormulator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,22 @@ class LPFormulator : public ParallelSolver

void
addMaxLayerToLpRelaxation( GurobiWrapper &gurobi, const Layer *layer, bool createVariables );


void
addRoundLayerToLpRelaxation( GurobiWrapper &gurobi, const Layer *layer, bool createVariables );

void
addAbsoluteValueLayerToLpRelaxation( GurobiWrapper &gurobi, const Layer *layer, bool createVariables );

void
addSigmoidLayerToLpRelaxation( GurobiWrapper &gurobi, const Layer *layer, bool createVariables );

void
addSoftmaxLayerToLpRelaxation( GurobiWrapper &gurobi, const Layer *layer, bool createVariables );

void
addBilinearLayerToLpRelaxation( GurobiWrapper &gurobi, const Layer *layer, bool createVariables );

void addWeightedSumLayerToLpRelaxation( GurobiWrapper &gurobi,
const Layer *layer,
bool createVariables );
Expand Down
Loading
Loading