Auto construction of a network level reasoner #253
Conversation
Merge from master
Merge from master
Merge from master
Merge from master
Symbolic bound tightening in NLR (NeuralNetworkVerification#249)
Symbolic bound tightening over absolute values (NeuralNetworkVerification#251)
Merge from master
| if ( eq._type != Equation::EQ ) | ||
| continue; | ||
|
|
||
| Set<unsigned> eqVars = eq.getParticipatingVariables(); |
There was a problem hiding this comment.
Storing this set across iterations might be more efficient, than repeatedly attempting to reduce it to one. Even though this will probably be a rare case.
This would also address my next comment because it would be sufficient to eliminate just processed variables since the effects would accumulate across layer iterations.
There was a problem hiding this comment.
I didn't understand this comment. What does it mean about the topology if an equation's variables appear across multiple layers?
There was a problem hiding this comment.
Maybe I made an assumption that's incorrect:
I assumed that the equation is a weighted sum of inputs = backwards-facing-variable, so if some variables skip levels then there is no guarantee that all members of the weighted sum belong to the same level, so they may be discharged at different times. So what I was suggesting was a mapping {vars} -> backward-facing-variable, and through iterations we eliminate variables from the set, and when the variable set is empty we know the position of the activation function and can remove the equation from consideration.
|
Hi Aleks, |
Merge from master
Merge from master
src/engine/NetworkLevelReasoner.cpp
Outdated
| if ( bias > 0 ) | ||
| printf( " + %.2lf", bias ); | ||
| else | ||
| printf( " - %.2lf", -bias ); |
There was a problem hiding this comment.
This can also be compacted by moving sign into the formatter.
…ion#253) * types for PL constraints * first attempt at automatically constructing the NLR * first unit test, couple of bug fixes * use PiecewiseLinearFunctionType * cleanup * some cleanup, and store more information about discovered neurons * wip * complete the construction of the NLR * bug fixes * bug fix * dumping functionality * bug fix * test * changes per Aleks' comments * minor * python bindings * minor Co-authored-by: Guy Katz <guykatz@cs.huji.ac.il>
* types for PL constraints * first attempt at automatically constructing the NLR * first unit test, couple of bug fixes * use PiecewiseLinearFunctionType * cleanup * some cleanup, and store more information about discovered neurons * wip * complete the construction of the NLR * bug fixes * bug fix * dumping functionality * bug fix * test * changes per Aleks' comments * minor * python bindings * minor Co-authored-by: Guy Katz <guykatz@cs.huji.ac.il>
When a user has not provided a network level reasoner as part of the input query, Marabou will attempt to automatically figure out the topology of the network and construct one itself. This is needed especially for symbolic bound tightening.