diff --git a/CHANGELOG.md b/CHANGELOG.md index 8ecc8e54f..412c3c810 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,7 @@ - Adding incremental infrastructure which allows pushing and popping constraints to/from the InputQuery. - Dropped support for parsing Tensorflow network format. Newest Marabou version that supports Tensorflow is at commit 190555573e4702. - Fixed bug in the parsing of `transpose` nodes in command line C++ parser. + - Added the BaBSR heuristic as a new branching strategy for ReLU Splitting ## Version 2.0.0 diff --git a/src/configuration/GlobalConfiguration.cpp b/src/configuration/GlobalConfiguration.cpp index c70ce013e..b84f9e4a5 100644 --- a/src/configuration/GlobalConfiguration.cpp +++ b/src/configuration/GlobalConfiguration.cpp @@ -106,6 +106,7 @@ const unsigned GlobalConfiguration::REFACTORIZATION_THRESHOLD = 100; const GlobalConfiguration::BasisFactorizationType GlobalConfiguration::BASIS_FACTORIZATION_TYPE = GlobalConfiguration::SPARSE_FORREST_TOMLIN_FACTORIZATION; +const unsigned GlobalConfiguration::BABSR_CANDIDATES_THRESHOLD = 5; const unsigned GlobalConfiguration::POLARITY_CANDIDATES_THRESHOLD = 5; const unsigned GlobalConfiguration::DNC_DEPTH_THRESHOLD = 5; diff --git a/src/configuration/GlobalConfiguration.h b/src/configuration/GlobalConfiguration.h index c89c1d54b..dfa5814bc 100644 --- a/src/configuration/GlobalConfiguration.h +++ b/src/configuration/GlobalConfiguration.h @@ -228,6 +228,11 @@ class GlobalConfiguration }; static const BasisFactorizationType BASIS_FACTORIZATION_TYPE; + /* In the BaBSR-based branching heuristics, only this many earliest nodes are considered to + branch on. + */ + static const unsigned BABSR_CANDIDATES_THRESHOLD; + /* In the polarity-based branching heuristics, only this many earliest nodes are considered to branch on. */ diff --git a/src/configuration/OptionParser.cpp b/src/configuration/OptionParser.cpp index cd94bbc39..358c11734 100644 --- a/src/configuration/OptionParser.cpp +++ b/src/configuration/OptionParser.cpp @@ -152,7 +152,7 @@ void OptionParser::initialize() &( ( *_stringOptions )[Options::SPLITTING_STRATEGY] ) ) ->default_value( ( *_stringOptions )[Options::SPLITTING_STRATEGY] ), "The branching strategy " - "(earliest-relu/pseudo-impact/largest-interval/relu-violation/polarity)." + "(earliest-relu/pseudo-impact/largest-interval/relu-violation/polarity/babsr)." " pseudo-impact is specific to the DeepSoI (default) procedure and relu-violation is " "specific to the Reluplex procedure.\n" )( "soi-split-threshold", diff --git a/src/configuration/Options.cpp b/src/configuration/Options.cpp index bf3b9b913..657ddb6b7 100644 --- a/src/configuration/Options.cpp +++ b/src/configuration/Options.cpp @@ -165,6 +165,8 @@ DivideStrategy Options::getDivideStrategy() const return DivideStrategy::LargestInterval; else if ( strategyString == "pseudo-impact" ) return DivideStrategy::PseudoImpact; + else if ( strategyString == "babsr" ) + return DivideStrategy::BaBSR; else return DivideStrategy::Auto; } diff --git a/src/engine/CMakeLists.txt b/src/engine/CMakeLists.txt index 469ddc0a3..487d806d3 100644 --- a/src/engine/CMakeLists.txt +++ b/src/engine/CMakeLists.txt @@ -47,6 +47,7 @@ engine_add_unit_test(SoftmaxConstraint) engine_add_unit_test(SmtCore) engine_add_unit_test(SumOfInfeasibilitiesManager) engine_add_unit_test(Tableau) +engine_add_unit_test(BaBsrSplitting) if (${BUILD_PYTHON}) target_include_directories(${MARABOU_PY} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}") diff --git a/src/engine/DivideStrategy.h b/src/engine/DivideStrategy.h index 539777816..77e260f2a 100644 --- a/src/engine/DivideStrategy.h +++ b/src/engine/DivideStrategy.h @@ -19,12 +19,13 @@ enum class DivideStrategy { // Relu splitting Polarity = 0, // Pick the ReLU with the polarity closest to 0 among the first K nodes + BaBSR, // Pick the ReLU with the highest BaBSR score EarliestReLU, // Pick a ReLU that appears in the earliest layer ReLUViolation, // Pick the ReLU that has been violated for the most times LargestInterval, // Pick the largest interval every K split steps, use ReLUViolation in other // steps PseudoImpact, // The pseudo-impact heuristic associated with SoI. - Auto, // See decideBranchingHeursitics() in Engine.h + Auto, // See decideBranchingHeuristics() in Engine.h }; #endif // __DivideStrategy_h__ diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp index ee3afa241..311daef54 100644 --- a/src/engine/Engine.cpp +++ b/src/engine/Engine.cpp @@ -2704,6 +2704,77 @@ void Engine::decideBranchingHeuristics() _smtCore.initializeScoreTrackerIfNeeded( _plConstraints ); } +PiecewiseLinearConstraint *Engine::pickSplitPLConstraintBasedOnBaBsrHeuristic() +{ + ENGINE_LOG( Stringf( "Using BaBsr heuristic with normalized scores..." ).ascii() ); + + if ( !_networkLevelReasoner ) + return NULL; + + // Get constraints from NLR + List constraints = + _networkLevelReasoner->getConstraintsInTopologicalOrder(); + + // Temporary vector to store raw scores for normalization + Vector rawScores; + Map scoreToConstraint; + + // Filter for ReLU constraints + for ( auto &plConstraint : constraints ) + { + if ( plConstraint->supportBaBsr() && plConstraint->isActive() && + !plConstraint->phaseFixed() ) + { + ReluConstraint *reluConstraint = dynamic_cast( plConstraint ); + if ( reluConstraint ) + { + // Set NLR if not already set + reluConstraint->initializeNLRForBaBSR( _networkLevelReasoner ); + + // Calculate heuristic score - bias calculation happens inside computeBaBsr + plConstraint->updateScoreBasedOnBaBsr(); + + // Collect raw scores + rawScores.append( plConstraint->getScore() ); + } + } + } + + // Normalize scores + if ( !rawScores.empty() ) + { + double minScore = *std::min_element( rawScores.begin(), rawScores.end() ); + double maxScore = *std::max_element( rawScores.begin(), rawScores.end() ); + double range = maxScore - minScore; + + for ( auto &plConstraint : constraints ) + { + if ( plConstraint->supportBaBsr() && plConstraint->isActive() && + !plConstraint->phaseFixed() ) + { + double rawScore = plConstraint->getScore(); + double normalizedScore = range > 0 ? ( rawScore - minScore ) / range : 0; + + // Store normalized score in the map + scoreToConstraint[normalizedScore] = plConstraint; + if ( scoreToConstraint.size() >= GlobalConfiguration::BABSR_CANDIDATES_THRESHOLD ) + break; + } + } + } + + // Split on neuron or constraint with highest normalized score + if ( !scoreToConstraint.empty() ) + { + ENGINE_LOG( Stringf( "Normalized score of the picked ReLU: %f", + ( *scoreToConstraint.begin() ).first ) + .ascii() ); + return ( *scoreToConstraint.begin() ).second; + } + else + return NULL; +} + PiecewiseLinearConstraint *Engine::pickSplitPLConstraintBasedOnPolarity() { ENGINE_LOG( Stringf( "Using Polarity-based heuristics..." ).ascii() ); @@ -2815,6 +2886,8 @@ PiecewiseLinearConstraint *Engine::pickSplitPLConstraint( DivideStrategy strateg candidatePLConstraint = _smtCore.getConstraintsWithHighestScore(); } } + else if ( strategy == DivideStrategy::BaBSR ) + candidatePLConstraint = pickSplitPLConstraintBasedOnBaBsrHeuristic(); else if ( strategy == DivideStrategy::Polarity ) candidatePLConstraint = pickSplitPLConstraintBasedOnPolarity(); else if ( strategy == DivideStrategy::EarliestReLU ) diff --git a/src/engine/Engine.h b/src/engine/Engine.h index 167fcac46..a3ea1c22d 100644 --- a/src/engine/Engine.h +++ b/src/engine/Engine.h @@ -751,6 +751,11 @@ class Engine */ void decideBranchingHeuristics(); + /* + Pick the ReLU with the highest BaBSR heuristic score. + */ + PiecewiseLinearConstraint *pickSplitPLConstraintBasedOnBaBsrHeuristic(); + /* Among the earliest K ReLUs, pick the one with Polarity closest to 0. K is equal to GlobalConfiguration::POLARITY_CANDIDATES_THRESHOLD diff --git a/src/engine/PiecewiseLinearConstraint.h b/src/engine/PiecewiseLinearConstraint.h index 86f3f20aa..4304baa01 100644 --- a/src/engine/PiecewiseLinearConstraint.h +++ b/src/engine/PiecewiseLinearConstraint.h @@ -315,6 +315,14 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher return false; } + /* + Return true if and only if this piecewise linear constraint supports the BaBsr Heuristic + */ + virtual bool supportBaBsr() const + { + return false; + } + /* Update the preferred direction to take first when splitting on this PLConstraint */ @@ -327,6 +335,9 @@ class PiecewiseLinearConstraint : public ITableau::VariableWatcher return _score; } + virtual void updateScoreBasedOnBaBsr() + { + } virtual void updateScoreBasedOnPolarity() { diff --git a/src/engine/ReluConstraint.cpp b/src/engine/ReluConstraint.cpp index 1aef70432..1f7b71f71 100644 --- a/src/engine/ReluConstraint.cpp +++ b/src/engine/ReluConstraint.cpp @@ -1019,6 +1019,11 @@ bool ReluConstraint::supportPolarity() const return true; } +bool ReluConstraint::supportBaBsr() const +{ + return true; +} + bool ReluConstraint::auxVariableInUse() const { return _auxVarInUse; @@ -1029,6 +1034,31 @@ unsigned ReluConstraint::getAux() const return _aux; } + +double ReluConstraint::computeBaBsr() const +{ + if ( !_networkLevelReasoner ) + throw MarabouError( MarabouError::NETWORK_LEVEL_REASONER_NOT_AVAILABLE ); + + double biasTerm = _networkLevelReasoner->getPreviousBias( this ); + + // get upper and lower bounds + double ub = getUpperBound( _b ); + double lb = getLowerBound( _b ); + + // cast _b and _f to doubles + double reluInput = _tableau->getValue( _b ); // ReLU input before activation + double reluOutput = _tableau->getValue( _f ); // ReLU output after activation + + // compute ReLU score + double scaler = ub / ( ub - lb ); + double term1 = + std::min( scaler * reluInput * biasTerm, ( scaler - 1.0 ) * reluInput * biasTerm ); + double term2 = ( scaler * lb ) * reluOutput; + + return term1 - term2; +} + double ReluConstraint::computePolarity() const { double currentLb = getLowerBound( _b ); @@ -1052,6 +1082,11 @@ PhaseStatus ReluConstraint::getDirection() const return _direction; } +void ReluConstraint::updateScoreBasedOnBaBsr() +{ + _score = std::abs( computeBaBsr() ); +} + void ReluConstraint::updateScoreBasedOnPolarity() { _score = std::abs( computePolarity() ); diff --git a/src/engine/ReluConstraint.h b/src/engine/ReluConstraint.h index 62a3f3e83..5821813e3 100644 --- a/src/engine/ReluConstraint.h +++ b/src/engine/ReluConstraint.h @@ -37,6 +37,15 @@ #include +/* + Namespace for Network Level Reasoner Instance. +*/ +namespace NLR { +class NetworkLevelReasoner; +class Layer; +struct NeuronIndex; +} // namespace NLR + class ReluConstraint : public PiecewiseLinearConstraint { public: @@ -57,6 +66,15 @@ class ReluConstraint : public PiecewiseLinearConstraint */ PiecewiseLinearConstraint *duplicateConstraint() const override; + /* + Initialize the network level reasoner needed for BaBSR branching heuristics. + */ + + void initializeNLRForBaBSR( NLR::NetworkLevelReasoner *nlr ) + { + _networkLevelReasoner = nlr; + } + /* Restore the state of this constraint from the given one. */ @@ -215,6 +233,10 @@ class ReluConstraint : public PiecewiseLinearConstraint bool supportPolarity() const override; + bool supportBaBsr() const override; + + double computeBaBsr() const; + /* Return the polarity of this ReLU, which computes how symmetric the bound of the input to this ReLU is with respect to 0. @@ -227,6 +249,7 @@ class ReluConstraint : public PiecewiseLinearConstraint always between -1 and 1. The closer it is to 0, the more symmetric the bound is. */ + double computePolarity() const; /* @@ -237,12 +260,18 @@ class ReluConstraint : public PiecewiseLinearConstraint PhaseStatus getDirection() const; + /* + Update the score based on the BaBsr heuristic + */ + void updateScoreBasedOnBaBsr() override; + void updateScoreBasedOnPolarity() override; const List getNativeAuxVars() const override; private: unsigned _b, _f; + NLR::NetworkLevelReasoner *_networkLevelReasoner; bool _auxVarInUse; unsigned _aux; diff --git a/src/engine/tests/Test_BaBsrSplitting.h b/src/engine/tests/Test_BaBsrSplitting.h new file mode 100644 index 000000000..8c68e6f76 --- /dev/null +++ b/src/engine/tests/Test_BaBsrSplitting.h @@ -0,0 +1,353 @@ +/********************* */ +/*! \file test_Test_BaBsrSplitting.h + ** \verbatim + ** Top contributors (to current version): + ** Liam Davis + ** This file is part of the Marabou project. + ** Copyright (c) 2017-2024 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + **/ + +#include "../nlr/NetworkLevelReasoner.h" +#include "MockErrno.h" +#include "MockTableau.h" +#include "Query.h" +#include "ReluConstraint.h" +#include "context/context.h" + +#include +#include +#include + +using namespace CVC4::context; + +class MockForNetworkLevelReasoner : public MockErrno +{ +public: +}; + +class Test_BaBsrSplitting : public CxxTest::TestSuite +{ +public: + MockForNetworkLevelReasoner *mock; + MockTableau *tableau; + + void setUp() + { + TS_ASSERT( mock = new MockForNetworkLevelReasoner ); + TS_ASSERT( tableau = new MockTableau() ); + } + + void tearDown() + { + delete tableau; + delete mock; + } + + void populateNetwork( NLR::NetworkLevelReasoner &nlr ) + { + /* + a + x d f + b + y e g + c + */ + + // Create the layers + nlr.addLayer( 0, NLR::Layer::INPUT, 2 ); + nlr.addLayer( 1, NLR::Layer::WEIGHTED_SUM, 3 ); + nlr.addLayer( 2, NLR::Layer::RELU, 3 ); + nlr.addLayer( 3, NLR::Layer::WEIGHTED_SUM, 2 ); + nlr.addLayer( 4, NLR::Layer::RELU, 2 ); + nlr.addLayer( 5, NLR::Layer::WEIGHTED_SUM, 2 ); + + // Mark layer dependencies + for ( unsigned i = 1; i <= 5; ++i ) + nlr.addLayerDependency( i - 1, i ); + + // Set the weights and biases for the weighted sum layers + nlr.setWeight( 0, 0, 1, 0, 1 ); + nlr.setWeight( 0, 0, 1, 1, 2 ); + nlr.setWeight( 0, 1, 1, 1, -3 ); + nlr.setWeight( 0, 1, 1, 2, 1 ); + + nlr.setWeight( 2, 0, 3, 0, 1 ); + nlr.setWeight( 2, 0, 3, 1, -1 ); + nlr.setWeight( 2, 1, 3, 0, 1 ); + nlr.setWeight( 2, 1, 3, 1, 1 ); + nlr.setWeight( 2, 2, 3, 0, -1 ); + nlr.setWeight( 2, 2, 3, 1, -1 ); + + nlr.setWeight( 4, 0, 5, 0, 1 ); + nlr.setWeight( 4, 0, 5, 1, 1 ); + nlr.setWeight( 4, 1, 5, 1, 3 ); + + nlr.setBias( 1, 0, 1 ); + nlr.setBias( 3, 1, 2 ); + + // Mark the ReLU sources + nlr.addActivationSource( 1, 0, 2, 0 ); + nlr.addActivationSource( 1, 1, 2, 1 ); + nlr.addActivationSource( 1, 2, 2, 2 ); + + nlr.addActivationSource( 3, 0, 4, 0 ); + nlr.addActivationSource( 3, 1, 4, 1 ); + + // Variable indexing + nlr.setNeuronVariable( NLR::NeuronIndex( 0, 0 ), 0 ); + nlr.setNeuronVariable( NLR::NeuronIndex( 0, 1 ), 1 ); + + nlr.setNeuronVariable( NLR::NeuronIndex( 1, 0 ), 2 ); + nlr.setNeuronVariable( NLR::NeuronIndex( 1, 1 ), 4 ); + nlr.setNeuronVariable( NLR::NeuronIndex( 1, 2 ), 6 ); + + nlr.setNeuronVariable( NLR::NeuronIndex( 2, 0 ), 3 ); + nlr.setNeuronVariable( NLR::NeuronIndex( 2, 1 ), 5 ); + nlr.setNeuronVariable( NLR::NeuronIndex( 2, 2 ), 7 ); + + nlr.setNeuronVariable( NLR::NeuronIndex( 3, 0 ), 8 ); + nlr.setNeuronVariable( NLR::NeuronIndex( 3, 1 ), 10 ); + + nlr.setNeuronVariable( NLR::NeuronIndex( 4, 0 ), 9 ); + nlr.setNeuronVariable( NLR::NeuronIndex( 4, 1 ), 11 ); + + nlr.setNeuronVariable( NLR::NeuronIndex( 5, 0 ), 12 ); + nlr.setNeuronVariable( NLR::NeuronIndex( 5, 1 ), 13 ); + } + + void test_relu_0() + { + NLR::NetworkLevelReasoner nlr; + populateNetwork( nlr ); + + // Generate Constraints + Query query; + nlr.generateQuery( query ); + List constraints = query.getPiecewiseLinearConstraints(); + + for ( const auto &constraint : constraints ) + { + ReluConstraint *relu = dynamic_cast( constraint ); + nlr.addConstraintInTopologicalOrder( relu ); + } + + // Get Constraints in topological order + List orderedConstraints = + nlr.getConstraintsInTopologicalOrder(); + MockTableau tableau; + + // Test ReLU 0 + ReluConstraint *relu = dynamic_cast( orderedConstraints.front() ); + + // Register Bounds + relu->registerTableau( &tableau ); + relu->initializeNLRForBaBSR( &nlr ); + + unsigned b = relu->getB(); + unsigned f = relu->getF(); + + relu->notifyLowerBound( b, -1 ); + relu->notifyUpperBound( b, 1 ); + relu->notifyLowerBound( f, 0 ); + relu->notifyUpperBound( f, 1 ); + + tableau.setValue( b, 0.5 ); + tableau.setValue( f, 0.5 ); + + // Compute BaBSR and compare + double score = relu->computeBaBsr(); + + TS_ASSERT_EQUALS( score, 0 ); + } + + void test_relu_1() + { + NLR::NetworkLevelReasoner nlr; + populateNetwork( nlr ); + + // Generate Constraints + Query query; + nlr.generateQuery( query ); + List constraints = query.getPiecewiseLinearConstraints(); + + for ( const auto &constraint : constraints ) + { + ReluConstraint *relu = dynamic_cast( constraint ); + nlr.addConstraintInTopologicalOrder( relu ); + } + + // Get Constraints in topological order + List orderedConstraints = + nlr.getConstraintsInTopologicalOrder(); + MockTableau tableau; + + // Test ReLU 1 + auto it = orderedConstraints.begin(); + std::advance( it, 1 ); + ReluConstraint *relu = dynamic_cast( *it ); + + // Register Bounds + relu->registerTableau( &tableau ); + relu->initializeNLRForBaBSR( &nlr ); + + unsigned b = relu->getB(); + unsigned f = relu->getF(); + + relu->notifyLowerBound( b, -1 ); + relu->notifyUpperBound( b, 1 ); + relu->notifyLowerBound( f, 0 ); + relu->notifyUpperBound( f, 1 ); + + tableau.setValue( b, 0.5 ); + tableau.setValue( f, 0.5 ); + + // Compute BaBSR and compare + double score = relu->computeBaBsr(); + + TS_ASSERT_EQUALS( score, 0.25 ); + } + + void test_relu_2() + { + NLR::NetworkLevelReasoner nlr; + populateNetwork( nlr ); + + // Generate Constraints + Query query; + nlr.generateQuery( query ); + List constraints = query.getPiecewiseLinearConstraints(); + + for ( const auto &constraint : constraints ) + { + ReluConstraint *relu = dynamic_cast( constraint ); + nlr.addConstraintInTopologicalOrder( relu ); + } + + // Get Constraints in topological order + List orderedConstraints = + nlr.getConstraintsInTopologicalOrder(); + MockTableau tableau; + + // Test ReLU 2 + auto it = orderedConstraints.begin(); + std::advance( it, 2 ); + ReluConstraint *relu = dynamic_cast( *it ); + + // Register Bounds + relu->registerTableau( &tableau ); + relu->initializeNLRForBaBSR( &nlr ); + + unsigned b = relu->getB(); + unsigned f = relu->getF(); + + relu->notifyLowerBound( b, -1 ); + relu->notifyUpperBound( b, 1 ); + relu->notifyLowerBound( f, 0 ); + relu->notifyUpperBound( f, 1 ); + + tableau.setValue( b, 0.5 ); + tableau.setValue( f, 0.5 ); + + // Compute BaBSR and compare + double score = relu->computeBaBsr(); + + TS_ASSERT_EQUALS( score, 0.25 ); + } + + void test_relu_3() + { + NLR::NetworkLevelReasoner nlr; + populateNetwork( nlr ); + + // Generate Constraints + Query query; + nlr.generateQuery( query ); + List constraints = query.getPiecewiseLinearConstraints(); + + for ( const auto &constraint : constraints ) + { + ReluConstraint *relu = dynamic_cast( constraint ); + nlr.addConstraintInTopologicalOrder( relu ); + } + + // Get Constraints in topological order + List orderedConstraints = + nlr.getConstraintsInTopologicalOrder(); + MockTableau tableau; + + // Test ReLU 3 + auto it = orderedConstraints.begin(); + std::advance( it, 3 ); + ReluConstraint *relu = dynamic_cast( *it ); + + // Register Bounds + relu->registerTableau( &tableau ); + relu->initializeNLRForBaBSR( &nlr ); + + unsigned b = relu->getB(); + unsigned f = relu->getF(); + relu->notifyLowerBound( b, -1 ); + relu->notifyUpperBound( b, 1 ); + relu->notifyLowerBound( f, 0 ); + relu->notifyUpperBound( f, 1 ); + + tableau.setValue( b, 0.5 ); + tableau.setValue( f, 0.5 ); + + // Compute BaBSR and compare + double score = relu->computeBaBsr(); + + TS_ASSERT_EQUALS( score, 0.25 ); + } + + void test_relu_4() + { + NLR::NetworkLevelReasoner nlr; + populateNetwork( nlr ); + + // Generate Constraints + Query query; + nlr.generateQuery( query ); + List constraints = query.getPiecewiseLinearConstraints(); + + for ( const auto &constraint : constraints ) + { + ReluConstraint *relu = dynamic_cast( constraint ); + nlr.addConstraintInTopologicalOrder( relu ); + } + + // Get Constraints in topological order + List orderedConstraints = + nlr.getConstraintsInTopologicalOrder(); + MockTableau tableau; + + // Test ReLU 4 + auto it = orderedConstraints.begin(); + std::advance( it, 4 ); + ReluConstraint *relu = dynamic_cast( *it ); + + // Register Bounds + relu->registerTableau( &tableau ); + relu->initializeNLRForBaBSR( &nlr ); + + unsigned b = relu->getB(); + unsigned f = relu->getF(); + relu->notifyLowerBound( b, -1 ); + relu->notifyUpperBound( b, 1 ); + relu->notifyLowerBound( f, 0 ); + relu->notifyUpperBound( f, 1 ); + + tableau.setValue( b, 0.5 ); + tableau.setValue( f, 0.5 ); + + // Compute BaBSR and compare + double score = relu->computeBaBsr(); + + TS_ASSERT_EQUALS( score, -0.25 ); + } +}; \ No newline at end of file diff --git a/src/engine/tests/Test_ReluConstraint.h b/src/engine/tests/Test_ReluConstraint.h index 6dd7ff8a4..f1fb4e9a0 100644 --- a/src/engine/tests/Test_ReluConstraint.h +++ b/src/engine/tests/Test_ReluConstraint.h @@ -51,18 +51,18 @@ using namespace CVC4::context; class ReluConstraintTestSuite : public CxxTest::TestSuite { public: - MockForReluConstraint *mock; + MockForReluConstraint *nlr; Context ctx; BoundManager *bm; void setUp() { - TS_ASSERT( mock = new MockForReluConstraint ); + TS_ASSERT( nlr = new MockForReluConstraint ); } void tearDown() { - TS_ASSERT_THROWS_NOTHING( delete mock ); + TS_ASSERT_THROWS_NOTHING( delete nlr ); } void test_relu_constraint() diff --git a/src/nlr/NLRError.h b/src/nlr/NLRError.h index dbeface6a..eb19fa05b 100644 --- a/src/nlr/NLRError.h +++ b/src/nlr/NLRError.h @@ -26,6 +26,8 @@ class NLRError : public Error LAYER_TYPE_NOT_SUPPORTED = 1, INPUT_LAYER_NOT_THE_FIRST_LAYER = 2, LEAKY_RELU_SLOPES_NOT_UNIFORM = 3, + RELU_NOT_FOUND = 4, + LAYER_NOT_FOUND = 5 }; NLRError( NLRError::Code code ) diff --git a/src/nlr/NetworkLevelReasoner.cpp b/src/nlr/NetworkLevelReasoner.cpp index 88621fcae..8390a0190 100644 --- a/src/nlr/NetworkLevelReasoner.cpp +++ b/src/nlr/NetworkLevelReasoner.cpp @@ -595,6 +595,81 @@ void NetworkLevelReasoner::generateLinearExpressionForWeightedSumLayer( } } +/* + Initialize and fill ReLU Constraint to previous bias map + for BaBSR Heuristic +*/ +void NetworkLevelReasoner::initializePreviousBiasMap() +{ + // Clear the previous bias map + _previousBiases.clear(); + + // Track accumulated ReLU neurons across layers + unsigned accumulatedNeurons = 0; + + // Iterate through layers to find ReLU layers and their sources + for ( const auto &layerPair : _layerIndexToLayer ) + { + const NLR::Layer *layer = layerPair.second; + + if ( layer->getLayerType() == Layer::RELU ) + { + // Get source layer info + const auto &sourceLayers = layer->getSourceLayers(); + unsigned sourceLayerIndex = sourceLayers.begin()->first; + const NLR::Layer *sourceLayer = getLayer( sourceLayerIndex ); + + // Match ReLU constraints to their source layer biases + unsigned layerSize = layer->getSize(); + + // Iterate through constraints + auto constraintIterator = _constraintsInTopologicalOrder.begin(); + for ( unsigned currentIndex = 0; + currentIndex < accumulatedNeurons && + constraintIterator != _constraintsInTopologicalOrder.end(); + ++currentIndex, ++constraintIterator ) + { + } + + // Now at correct starting position + for ( unsigned i = 0; + i < layerSize && constraintIterator != _constraintsInTopologicalOrder.end(); + ++i, ++constraintIterator ) + { + if ( auto reluConstraint = + dynamic_cast( *constraintIterator ) ) + { + // Store bias in map + _previousBiases[reluConstraint] = sourceLayer->getBias( i ); + } + } + + accumulatedNeurons += layerSize; + } + } +} + +/* + Get previous layer bias of a ReLU neuron + for BaBSR Heuristic +*/ +double NetworkLevelReasoner::getPreviousBias( const ReluConstraint *reluConstraint ) const +{ + // Initialize map if empty + if ( _previousBiases.empty() ) + { + const_cast( this )->initializePreviousBiasMap(); + } + + // Look up pre-computed bias + if ( !_previousBiases.exists( reluConstraint ) ) + { + throw NLRError( NLRError::RELU_NOT_FOUND, "ReluConstraint not found in bias map." ); + } + + return _previousBiases[reluConstraint]; +} + unsigned NetworkLevelReasoner::mergeConsecutiveWSLayers( const Map &lowerBounds, const Map &upperBounds, @@ -679,6 +754,7 @@ bool NetworkLevelReasoner::suitableForMerging( return true; } + void NetworkLevelReasoner::mergeWSLayers( unsigned secondLayerIndex, Map &eliminatedNeurons ) { diff --git a/src/nlr/NetworkLevelReasoner.h b/src/nlr/NetworkLevelReasoner.h index 97af9610f..2660795be 100644 --- a/src/nlr/NetworkLevelReasoner.h +++ b/src/nlr/NetworkLevelReasoner.h @@ -172,6 +172,12 @@ class NetworkLevelReasoner : public LayerOwner */ void generateQuery( Query &query ); + /* + Given a ReLU Constraint, get the previous layer bias + for the BaBSR Heuristic + */ + double getPreviousBias( const ReluConstraint *reluConstraint ) const; + /* Finds logically consecutive WS layers and merges them, in order to reduce the total number of layers and variables in the @@ -236,6 +242,13 @@ class NetworkLevelReasoner : public LayerOwner unsigned outputDimension ); void reduceLayerIndex( unsigned layer, unsigned startIndex ); + /* + Store previous biases for each ReLU neuron in a map for getPreviousBias() + and BaBSR heuristic + */ + Map _previousBiases; + void initializePreviousBiasMap(); + /* If the NLR is manipulated manually in order to generate a new input query, this method can be used to assign variable indices diff --git a/src/nlr/tests/Test_NetworkLevelReasoner.h b/src/nlr/tests/Test_NetworkLevelReasoner.h index 8afb4e032..33b0aff13 100644 --- a/src/nlr/tests/Test_NetworkLevelReasoner.h +++ b/src/nlr/tests/Test_NetworkLevelReasoner.h @@ -2207,4 +2207,65 @@ class NetworkLevelReasonerTestSuite : public CxxTest::TestSuite for ( const auto &bound : expectedBounds ) TS_ASSERT( bounds.exists( bound ) ); } + + void test_get_previous_bias() + { + NLR::NetworkLevelReasoner nlr; + populateNetwork( nlr ); + + // Generate query to create ReLU constraints + Query query; + nlr.generateQuery( query ); + + // Find ReLU constraints from the query + List constraints = query.getPiecewiseLinearConstraints(); + + for ( const auto &constraint : constraints ) + { + ReluConstraint *relu = dynamic_cast( constraint ); + TS_ASSERT( relu ); + + nlr.addConstraintInTopologicalOrder( relu ); + + // First ReLU layer (nodes 2,0 through 2,2) has previous bias 1 + if ( relu->getB() == 3 || relu->getB() == 5 || relu->getB() == 7 ) + { + TS_ASSERT_EQUALS( nlr.getPreviousBias( relu ), 1 ); + } + // Second ReLU layer (nodes 4,0 and 4,1) has previous bias 2 + else if ( relu->getB() == 9 || relu->getB() == 11 ) + { + TS_ASSERT_EQUALS( nlr.getPreviousBias( relu ), 2 ); + } + } + } + + void test_get_previous_bias_error_handling() + { + NLR::NetworkLevelReasoner nlr; + populateNetwork( nlr ); + + // Generate invalid ReLU constraint + ReluConstraint invalidRelu( 15, 16 ); // Variables not in network + + // Should throw since variables don't exist in network + TS_ASSERT_THROWS_EQUALS( nlr.getPreviousBias( &invalidRelu ), + const NLRError &e, + e.getCode(), + NLRError::RELU_NOT_FOUND ); + + // Test missing activation source using fresh network + NLR::NetworkLevelReasoner nlrNoActivations; + // Create minimal network without activation sources + nlrNoActivations.addLayer( 0, NLR::Layer::INPUT, 2 ); + nlrNoActivations.addLayer( 1, NLR::Layer::WEIGHTED_SUM, 2 ); + nlrNoActivations.addLayer( 2, NLR::Layer::RELU, 2 ); + + ReluConstraint missingActivation( 2, 3 ); + + TS_ASSERT_THROWS_EQUALS( nlrNoActivations.getPreviousBias( &missingActivation ), + const NLRError &e, + e.getCode(), + NLRError::RELU_NOT_FOUND ); + } };