MCPcopy Create free account
hub / github.com/NeuralNetworkVerification/Marabou / dLSELowerBound2

Method dLSELowerBound2

src/nlr/DeepPolySoftmaxElement.cpp:427–499  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

425}
426
427double DeepPolySoftmaxElement::dLSELowerBound2( const Vector<double> &inputMids,
428 const Vector<double> &inputLbs,
429 const Vector<double> &inputUbs,
430 unsigned i,
431 unsigned di )
432{
433 double max = FloatUtils::negativeInfinity();
434 unsigned maxInputIndex = 0;
435 unsigned index = 0;
436 for ( const auto &mid : inputMids )
437 {
438 if ( mid > max )
439 {
440 max = mid;
441 maxInputIndex = index;
442 }
443 ++index;
444 }
445
446 if ( maxInputIndex == i )
447 return dERLowerBound( inputMids, inputLbs, inputUbs, i, di );
448 else
449 {
450 double val = LSELowerBound2( inputMids, inputLbs, inputUbs, i );
451
452 double sum = 0;
453 for ( unsigned j = 0; j < inputMids.size(); ++j )
454 {
455 if ( j == maxInputIndex )
456 sum += 1;
457 else
458 {
459 double ljjstar = inputLbs[j] - inputUbs[maxInputIndex];
460 double ujjstar = inputUbs[j] - inputLbs[maxInputIndex];
461 double xjjstar = inputMids[j] - inputMids[maxInputIndex];
462 sum += ( ujjstar - xjjstar ) / ( ujjstar - ljjstar ) * std::exp( ljjstar ) +
463 ( xjjstar - ljjstar ) / ( ujjstar - ljjstar ) * std::exp( ujjstar );
464 }
465 }
466 double val2 = std::exp( inputMids[i] - inputMids[maxInputIndex] ) / ( sum * sum );
467
468 if ( i == di )
469 {
470 double ldijstar = inputLbs[i] - inputUbs[maxInputIndex];
471 double udijstar = inputUbs[i] - inputLbs[maxInputIndex];
472 return val -
473 val2 * ( std::exp( udijstar ) - std::exp( ldijstar ) ) / ( udijstar - ldijstar );
474 }
475 else if ( maxInputIndex == di )
476 {
477 double sum2 = 0;
478 for ( unsigned j = 0; j < inputMids.size(); ++j )
479 {
480 if ( j == maxInputIndex )
481 continue;
482 else
483 {
484 double ljjstar = inputLbs[j] - inputUbs[maxInputIndex];

Callers

nothing calls this directly

Calls 1

sizeMethod · 0.45

Tested by

no test coverage detected