Leaky relu #468
Leaky relu #468
Conversation
| xPts, | ||
| yPts ); | ||
| } | ||
| catch (GRBException e ) |
There was a problem hiding this comment.
space after (.
Please refrain from abbreviations: pts --> points
src/common/GurobiWrapper.cpp
Outdated
| } | ||
| } | ||
|
|
||
|
|
| @@ -71,6 +71,12 @@ class GurobiWrapper | |||
| // Add a new EQ constraint, e.g. 3x + 4y = -5 | |||
| void addEqConstraint( const List<Term> &terms, double scalar ); | |||
|
|
|||
| // Add a piece-wise linear constraint | |||
There was a problem hiding this comment.
Is this a new Gurobi interface we're starting to use? Perhaps all existing encodings should use it, too?
There was a problem hiding this comment.
I agree it's worth studying whether we should switch to gurobi PLW constraints altogether
| @@ -23,6 +23,8 @@ class GlobalConfiguration | |||
| public: | |||
| static void print(); | |||
|
|
|||
| static const double LEAKY_RELU_SLOPE; | |||
There was a problem hiding this comment.
Is it a single slope for all leaky relus in the query? Because the python interface suggested each could have a separate slope.
There was a problem hiding this comment.
I agree that we should allow each leaky relu to have their own slope.
src/engine/InputQuery.cpp
Outdated
|
|
||
| List<NeuronInformation> newNeurons; | ||
|
|
||
| // Look for ReLUs where all b variables have already been handled |
src/engine/MILPEncoder.cpp
Outdated
| @@ -91,7 +94,7 @@ void MILPEncoder::encodeEquation( GurobiWrapper &gurobi, const Equation &equatio | |||
| } | |||
| } | |||
|
|
|||
| void MILPEncoder::encodeReLUConstraint( GurobiWrapper &gurobi, ReluConstraint *relu) | |||
| void MILPEncoder::encodeReLUConstraint( GurobiWrapper &gurobi, ReluConstraint *relu ) | |||
| { | |||
|
|
|||
src/engine/MarabouError.h
Outdated
| @@ -49,6 +49,7 @@ class MarabouError : public Error | |||
| NETWORK_LEVEL_REASONER_ACTIVATION_NOT_SUPPORTED = 24, | |||
| NETWORK_LEVEL_REASONER_NOT_AVAILABLE = 24, | |||
| REQUESTED_NONEXISTENT_CASE_SPLIT= 25, | |||
| INVALID_LEAKY_RELU_SLOPE= 26, | |||
There was a problem hiding this comment.
space before =. For prevoius line also
src/nlr/DeepPolyLeakyReLUElement.cpp
Outdated
| _layer = layer; | ||
| _size = layer->getSize(); | ||
| _layerIndex = layer->getLayerIndex(); | ||
| _alpha = layer->getAlpha(); |
There was a problem hiding this comment.
again, I think slope is better than alpha.
Are we sure all leakyRelus in the layer have the same slope?
There was a problem hiding this comment.
rename slope to _alpha in the DeepPoly LeakyReLUElement.
src/nlr/Layer.cpp
Outdated
| NeuronIndex sourceIndex = *_neuronToActivationSources[i].begin(); | ||
| double inputValue = _layerOwner->getLayer( sourceIndex._layer )->getAssignment( sourceIndex._neuron ); | ||
|
|
||
| _assignment[i] = FloatUtils::max( inputValue, slope * inputValue ); |
There was a problem hiding this comment.
unclear. is slope always <=1?
even if so, lets make this more comprehensible
There was a problem hiding this comment.
Yes, currently we need slope to be <= 1, otherwise the symbolic bounds would be incorrect. I added an assertion and also throw an error when this requirement is not met when constructing a LeakyReLU
src/nlr/Layer.cpp
Outdated
| NeuronIndex sourceIndex = *_neuronToActivationSources[i].begin(); | ||
| const Vector<double> &simulations = ( *( _layerOwner->getLayer( sourceIndex._layer )->getSimulations() ) ).get( sourceIndex._neuron ); | ||
| for ( unsigned j = 0; j < simulationSize; ++j ) | ||
| _simulations[i][j] = FloatUtils::max( simulations.get( j ), slope * simulations.get( j ) ); |
There was a problem hiding this comment.
same comment, slope > 1?
There was a problem hiding this comment.
added an assertion.
|
Before merging, this should get a CHANGELOG entry added. |
maraboupy/MarabouNetwork.py
Outdated
| @@ -472,6 +489,8 @@ def evaluateWithMarabou(self, inputValues, filename="evaluateWithMarabou.log", o | |||
| ipq.setLowerBound(k, inputDict[k]) | |||
| ipq.setUpperBound(k, inputDict[k]) | |||
|
|
|||
| MarabouCore.saveQuery(ipq, "test.ipq") | |||
There was a problem hiding this comment.
Is this intended? Or a debugging thing?
src/engine/LeakyReluConstraint.cpp
Outdated
|
|
||
| List<PiecewiseLinearConstraint::Fix> LeakyReluConstraint::getPossibleFixes() const | ||
| { | ||
| return List<PiecewiseLinearConstraint::Fix>(); |
There was a problem hiding this comment.
Should we complete this bit? It's pretty straightforward, no?
src/engine/LeakyReluConstraint.cpp
Outdated
| } | ||
| else | ||
| { | ||
| // Default: start with the inactive case, because it doesn't |
There was a problem hiding this comment.
This seems stale, neither add new equations now, right?
In general, are the heuristics in this function needed, or just some left overs?
There was a problem hiding this comment.
Agreed. The heuristics in the function are used during the search. I removed this comment though.
There was a problem hiding this comment.
I also implemented the getPossibleFixes() method above (can't seem to reply to that comment of yours for some reason..)
|
|
||
| // If we have existing knowledge about the assignment, use it to | ||
| // influence the order of splits | ||
| if ( existsAssignment( _f ) ) |
There was a problem hiding this comment.
Same: is this comment correct, or stale?
There was a problem hiding this comment.
This comment is correct, since we can still heuristically decide on which case split to try first based on the value of the leaky relu output.
src/engine/LeakyReluConstraint.cpp
Outdated
| inactiveAuxUpperBound = getUpperBound( _inactiveAux ); | ||
| } | ||
|
|
||
|
|
| _score = std::abs( computePolarity() ); | ||
| } | ||
|
|
||
| // Not supporting proof production yet |
There was a problem hiding this comment.
After we merge this, please ping Omri in case he wants to add proof support here
src/engine/MILPEncoder.cpp
Outdated
| } | ||
| else | ||
| { | ||
| if ( relax ) { |
src/engine/MILPEncoder.cpp
Outdated
| terms.append( GurobiWrapper::Term( lambda, Stringf( "x%u", sourceVariable ) ) ); | ||
| terms.append( GurobiWrapper::Term( -1, Stringf( "x%u", targetVariable ) ) ); | ||
| gurobi.addGeqConstraint( terms, ( lambda - 1 ) * sourceUb ); | ||
| } else { |
| @@ -125,6 +126,9 @@ class Layer | |||
| double *getLbs() const; | |||
| double *getUbs() const; | |||
|
|
|||
| void setAlpha( double alpha ) { _alpha = alpha; } | |||
| double getAlpha() const { return _alpha; } | |||
There was a problem hiding this comment.
This seems very very specific to appear in "Layer". I see there is nothing specific to any of the other kinds of constraints. Is this really needed?
There was a problem hiding this comment.
I agree this is not ideal but I'm not sure there is a easy good alternative. I think in general the Layer class might need a refactoring. Right now we have parameters specific to certain layers existing as field variables (like weights for the WeightedSum layer). I think the approach moving forward is to have different types of layers as subclasses of the layer abstract class. Alternatively, we can keep a parameter map (e.g., Map<String, void *>) in the layer class which can store things like "weights" and "alpha". I think the latter is the way onnx handles it.
There was a problem hiding this comment.
Okay. Lets at least add a comment that these belong to leaky relus
There was a problem hiding this comment.
Had a comment in that regardes when declaring _alpha in Layer.h. But I added that this can be optimized in the future.
Add a note about alpha in Layer.h
* add leaky relu class * leaky relu in nlr construction * leaky relu layer * add test for nlr construction * deeppoly leaky relu * add test * add file * add test for evalution * leaky relu * leaky relu * minor * multiple-outputs * minor * leaky relu * bug fix * leaky relu * handle case where leaky relu's inactive phase has slope greater than 1 * turn off logging * minor * update leaky ReLU * fix merge conflict * fix leaky relu * add leaky relu * add regression test for leaky relu * add test * relaxation * fix merge conflict * tab width * add one more regression test * addressing Guy's comments * fix merge conflict * Update Layer.h Add a note about alpha in Layer.h
Adding leaky relu support
----update----
3. Also support solving in DeepSoI
4. Added regression tests on leaky relu networks.