Backward Analysis using Preimage Approximation #861

ido-shm-uel · 2025-02-06T17:08:26Z

Implemented PreimageApproximation Algorithm (simplified, without branch-and-bound) for ReLU, LeakyReLU, Sign and Billinear Layers (arXiv:2305.03686v4 [cs.SE], arXiv:2405.21063 [cs.LG]).
Added option to perform LP relaxation using backward-preimage-approx.
Added unit tests at Test_NetworkLevelReasoner.h.

Added assignment and store-into-other NLR tests for every activation function.

…ction.

0-2-0: Implementing layer simulations for every activation function.

0-2-1: Testing layer simulations for every activation function.

0-3-0: Implementing interval arithmetic for all activation functions.

0-3-1: Adding interval arithmetic tests for all activation functions.

…nction. 0-4-0: Implementing symbolic bound tightening for every activation function.

…tions. 0-4-1: Adding symbolic bound tightening tests for all activation functions.

0-5-0: Adding rounding constant for LP relaxation propagation.

… activation functions. 0-5-1: Implementing forward-backward LP propagation algorithm for all activation functions.

…n functions. 0-5-2: Adding forward-backward LP propagation tests for all activation functions.

…rithms, adjusting in Engine. 0-6-0: Adding MILP bound types for two backpropagation of bounds algorithms, adjusting in Engine.

0-6-1: Adjusting in Options for two new MILP Bound types.

…rithms). 0-6-2: Introducing Polygonal Tightenings (output type of two new algorithms).

0-6-3: Adjusting in NLR, LayerOwner for Polygonal Tightenings.

…rithms will optimize value of parameter). 0-6-4: Introducing parameterised bounds in LPFormulator (two new algorithms will optimize value of parameter).

0-6-5: Current state of PreimageApproximation + cleanup + corrections.

0-6-6: New constants for PreimageApproximation (random seeds).

…algorithm (gradient-free optimization for PreimageApproximation). 0-6-7: TEMPORARY CHANGE - use boost v1.85 for Differential Evolution algorithm (gradient-free optimization for PreimageApproximation).

0-6-8: Revert last change.

0-6-9: Adapt DifferentialEvolution from Boost v1.85.

…ented). 0-6-10: Current state of PreimageApproximation (EstimateVolume implemented).

0-6-11: Add constants for PreimageApproximation.

…descent). 0-6-12: Current state of PreimageApproximation (implement coordinate descent).

…ow). 0-6-13: Timing PreimageApproximation with coordinate descent (very slow).

0-6-14: Small Fix (same as 0-5---4).

UNSAT certification statistics (NeuralNetworkVerification#850) (Fork Sync)

…imization algorithms, parameters, clang-format,) - Apply 0-5--6 fixes (Backward-Forward Algorithm branch) to this branch. - Add new optimization algorithms for PreimageApproximation: Coordinate Descent, Gradient Descent, Adam Optimizer. - Change default algorithm (Adam) + parameters to reduce runtime. - Apply clang-format to all files changed.

…pdateRandomly() when the chosen plConstraintToUpdate is fixed

smal fix for bug in SumOfInfeasibilitiesManager::proposePhasePatternU… - - Merge idan0610's fork to solve regression tests failling due to fixed Sign Layer splitting (MarabouError 7).

wu-haoze

Hi @ido-shm-uel , thanks for this addition. I have some questions and (mostly minor) code style suggestions. Please see my comments!

wu-haoze · 2025-02-20T14:36:11Z

src/engine/PolygonalTightening.h

+
+#endif // __PolygonalTightening_h__
+
+//


Remove lines after 95 as they are obsolete since we switched to cmake.

wu-haoze · 2025-02-20T14:40:04Z

src/nlr/LPFormulator.cpp

 void LPFormulator::optimizeBoundsWithLpRelaxation( const Map<unsigned, Layer *> &layers,
-                                                   bool backward )
+                                                   bool backward,
+                                                   std::vector<double> coeffs )


use the internal Vector instead. Also, please pass by reference to avoid keep copying the coeffs vectors.

Vector<double> &coeffs

wu-haoze · 2025-02-20T14:40:36Z

src/nlr/LPFormulator.cpp

-void LPFormulator::optimizeBoundsOfNeuronsWithLpRlaxation( ThreadArgument &args, bool backward )
+void LPFormulator::optimizeBoundsOfNeuronsWithLpRelaxation( ThreadArgument &args,
+                                                            bool backward,
+                                                            std::vector<double> coeffs )


similarly, please pass by reference and change the datatype.

wu-haoze · 2025-02-20T14:40:50Z

src/nlr/LPFormulator.cpp

                                       GurobiWrapper &gurobi,
-                                       unsigned lastLayer )
+                                       unsigned lastLayer,
+                                       std::vector<double> coeffs )


wu-haoze · 2025-02-20T14:41:10Z

src/nlr/LPFormulator.cpp

                                            GurobiWrapper &gurobi,
-                                            unsigned firstLayer )
+                                            unsigned firstLayer,
+                                            std::vector<double> coeffs )


wu-haoze · 2025-02-20T14:57:01Z

src/nlr/Layer.cpp

            // Concrete upper bound: x_f <= ub_b
            double width = sourceUb - sourceLb;
-            double coeff = ( sourceUb - _alpha * sourceLb ) / width;
+            double weight = ( sourceUb - _alpha * sourceLb ) / width;


What is the rationale behind this name change? It seems we are mostly using coeffs when it comes to symbolic bounds?

wu-haoze · 2025-02-20T14:58:16Z

src/nlr/Layer.h

-    void computeSymbolicBounds();
    void computeIntervalArithmeticBounds();
+    void computeSymbolicBounds();
+    void computeParameterisedSymbolicBounds( std::vector<double> coeffs,


Change to Vector &coeffs here and below.

wu-haoze · 2025-02-20T14:59:53Z

src/nlr/NetworkLevelReasoner.h

    void obtainCurrentBounds();
    void intervalArithmeticBoundPropagation();
    void symbolicBoundPropagation();
+    void parameterisedSymbolicBoundPropagation( std::vector<double> coeffs );


pass by reference.

wu-haoze · 2025-02-20T15:00:55Z

src/engine/PolygonalTightening.h

+    /*
+      Equality operator.
+    */
+    bool operator==( const PolygonalTightening &other ) const


Could you point to me where this equality operator is used?

wu-haoze · 2025-02-20T15:02:43Z

src/engine/PolygonalTightening.h

+ ** directory for licensing information.\endverbatim
+ **
+ ** [[ Add lengthier description here ]]
+


Could you add a description of what this class is supposed to represent? Does this represent a linear symbolic bound in terms of neurons? Also, this file should probably be in src/nlr/ since it's very NLR specific.

Sync Fork.

SBT for Sigmoid: Corrected criterion for fixed Sigmoid neuron. SBT for Softmax: Symbolic bounds now stored correctly in _symbolicLb, _symbolicUb. SBT for Bilinear: Fixed calculation for symbolic lower/upper bias, fixed mistaken assumption both source neurons are from same layer. Parameterized SBT for Bilinear: Fixed calculation for symbolic lower/upper bias, fixed mistaken assumption both source neurons are from same layer. LP relaxation for Bilinear: Fixed mistaken assumption both source neurons are from same layer. Parameterized LP relaxation for Bilinear: Fixed mistaken assumption both source neurons are from same layer. Minor changes for code of PreimageApproximation optimization function: size_t -> unsigned, define sign variable at start of function, use Vector( double, unsigned ) constructor and std::min/std::max.

Fixed typos in documentation of some tests, Corrected one SBT Softmax test and two PreimageApproximation Bilinear tests, removed all void populateNetworkBackward*() functions from Test_NetworkLevelReasoner.h (all unused, duplicated from Test_LPRelaxation,h).

Interval Arithmetic and Symbolic Bound Tightening for Max, Softmax, Bilinear mistakenly assume 1. All source neurons are from same layer. 2. The size of the current layer is equal to the number of source neurons of any softmax neuron. Fixed both errors.

…tion#889).

…-FIX Corrections for SBT and LP relaxations with Sigmoid, Max, Softmax, Bilinear layers.

ido-shm-uel added 30 commits October 1, 2024 22:56

Add files via upload

e00d517

Added assignment and store-into-other NLR tests for every activation function.

Revert last change.

04cc0b1

Added assginment, store-into-other NLR tests for every activation fun…

80be6dc

…ction.

Add files via upload

9fbca7b

0-2-0: Implementing layer simulations for every activation function.

Add files via upload

f7aee6d

0-2-1: Testing layer simulations for every activation function.

Add files via upload

33f5d5f

0-3-0: Implementing interval arithmetic for all activation functions.

Add files via upload

6d1c898

0-3-1: Adding interval arithmetic tests for all activation functions.

0-4-0: Implementing symbolic bound tightening for every activation fu…

ee5dd00

…nction. 0-4-0: Implementing symbolic bound tightening for every activation function.

0-4-1: Adding symbolic bound tightening tests for all activation func…

85fe8f3

…tions. 0-4-1: Adding symbolic bound tightening tests for all activation functions.

0-5-0: Adding rounding constant for LP relaxation propagation.

32d7c52

0-5-0: Adding rounding constant for LP relaxation propagation.

0-5-1: Implementing forward-backward LP propagation algorithm for all…

5a7c5d8

… activation functions. 0-5-1: Implementing forward-backward LP propagation algorithm for all activation functions.

0-5-2: Adding forward-backward LP propagation tests for all activatio…

79f7a84

…n functions. 0-5-2: Adding forward-backward LP propagation tests for all activation functions.

0-6-0: Adding MILP bound types for two backpropagation of bounds algo…

9ee7609

…rithms, adjusting in Engine. 0-6-0: Adding MILP bound types for two backpropagation of bounds algorithms, adjusting in Engine.

0-6-1: Adjusting in Options for two new MILP Bound types.

2d9b85a

0-6-1: Adjusting in Options for two new MILP Bound types.

0-6-2: Introducing Polygonal Tightenings (output type of two new algo…

f5c7d1c

…rithms). 0-6-2: Introducing Polygonal Tightenings (output type of two new algorithms).

0-6-3: Adjusting in NLR, LayerOwner for Polygonal Tightenings.

b363d05

0-6-3: Adjusting in NLR, LayerOwner for Polygonal Tightenings.

0-6-4: Introducing parameterised bounds in LPFormulator (two new algo…

7993b1e

…rithms will optimize value of parameter). 0-6-4: Introducing parameterised bounds in LPFormulator (two new algorithms will optimize value of parameter).

0-6-5: Current state of PreimageApproximation + cleanup + corrections.

c888160

0-6-5: Current state of PreimageApproximation + cleanup + corrections.

0-6-6: New constants for PreimageApproximation (random seeds).

cd5f2de

0-6-6: New constants for PreimageApproximation (random seeds).

0-6-7: TEMPORARY CHANGE - use boost v1.85 for Differential Evolution …

d86c0a3

…algorithm (gradient-free optimization for PreimageApproximation). 0-6-7: TEMPORARY CHANGE - use boost v1.85 for Differential Evolution algorithm (gradient-free optimization for PreimageApproximation).

0-6-8: Revert last change.

4467e09

0-6-8: Revert last change.

0-6-9: Adapt DifferentialEvolution from Boost v1.85.

88e339a

0-6-9: Adapt DifferentialEvolution from Boost v1.85.

0-6-10: Current state of PreimageApproximation (EstimateVolume implem…

8031a41

…ented). 0-6-10: Current state of PreimageApproximation (EstimateVolume implemented).

0-6-11: Add constants for PreimageApproximation.

dd584e7

0-6-11: Add constants for PreimageApproximation.

0-6-12: Current state of PreimageApproximation (implement coordinate …

cd52524

…descent). 0-6-12: Current state of PreimageApproximation (implement coordinate descent).

0-6-13: Timing PreimageApproximation with coordinate descent (very sl…

b719359

…ow). 0-6-13: Timing PreimageApproximation with coordinate descent (very slow).

0-6-14: Small Fix (same as 0-5---4).

f29ccf0

0-6-14: Small Fix (same as 0-5---4).

Merge pull request #1 from NeuralNetworkVerification/master

3ee6903

UNSAT certification statistics (NeuralNetworkVerification#850) (Fork Sync)

Delete src/nlr/PolygonalTightening.h

22f0eaa

ido-shm-uel and others added 10 commits February 6, 2025 01:14

Update GlobalConfiguration.cpp

7696156

Update CHANGELOG.md

2c6aba8

Update OptionParser.cpp

2894e4f

smal fix for bug in SumOfInfeasibilitiesManager::proposePhasePatternU…

5f7a24f

…pdateRandomly() when the chosen plConstraintToUpdate is fixed

Sync Fork.

e7618fb

Add files via upload

0884a78

Add files via upload

40f2fe2

Add files via upload

a95e3a1

Add files via upload

f7adf2b

Merge pull request #7 from idan0610/fix_soi_proposal_bug

6e34c3f

smal fix for bug in SumOfInfeasibilitiesManager::proposePhasePatternU… - - Merge idan0610's fork to solve regression tests failling due to fixed Sign Layer splitting (MarabouError 7).

wu-haoze requested changes Feb 20, 2025

View reviewed changes

ido-shm-uel added 3 commits February 26, 2025 20:13

Vector<double> &coeffs passed by refrence, removed PolygonalTightening.

c74870e

Sync Fork.

a226133

.

eb0e58f

ido-shm-uel closed this Feb 27, 2025

ido-shm-uel reopened this Feb 27, 2025

ido-shm-uel closed this Feb 27, 2025

.

2df9d58

ido-shm-uel reopened this Feb 27, 2025

ido-shm-uel added 2 commits March 13, 2025 14:37

Corrections to PreimageApproximation, parameterizes SBT.

eafa24c

Remove redundant setAlpha in ReLU NLR unit tests.

b1711aa

wu-haoze approved these changes Jul 31, 2025

View reviewed changes

ido-shm-uel added 8 commits September 17, 2025 20:48

Merge pull request #14 from NeuralNetworkVerification/master

9304f52

Sync Fork.

Clang-Format

29bfda9

Manually Sync Fork: Towards Proof Minimization (NeuralNetworkVerifica…

8fcd8b0

…tion#889).

Fix merge conflict.

ad41336

Merge pull request #17 from ido-shm-uel/Preimage-Approximation-SBT-LP…

d150c12

…-FIX Corrections for SBT and LP relaxations with Sigmoid, Max, Softmax, Bilinear layers.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Backward Analysis using Preimage Approximation #861

Backward Analysis using Preimage Approximation #861

Uh oh!

ido-shm-uel commented Feb 6, 2025

Uh oh!

wu-haoze left a comment

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

wu-haoze Feb 20, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants


		#endif // __PolygonalTightening_h__

		//

Backward Analysis using Preimage Approximation #861

Are you sure you want to change the base?

Backward Analysis using Preimage Approximation #861

Uh oh!

Conversation

ido-shm-uel commented Feb 6, 2025

Uh oh!

wu-haoze left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants