16template<
typename FunctionType>
18template<
typename FunctionType>
21template<
typename FunctionType,
typename ConstantType>
22ConstantType GradientDescentInstantiationSearcher<FunctionType, ConstantType>::doStep(
30 ConstantType projectedGradient;
33 ConstantType newPlainPosition = oldPosAsConstant + precisionAsConstant * gradient.at(steppingParameter);
38 if (newPlainPosition < lower || newPlainPosition > upper) {
39 projectedGradient = 0;
41 projectedGradient = gradient.at(steppingParameter);
48 if (oldPosAsConstant < precisionAsConstant) {
49 projectedGradient = 1000;
51 projectedGradient = -1000;
53 projectedGradient = gradient.at(steppingParameter);
65 projectedGradient = gradient.at(steppingParameter) + logarithmicBarrierTerm / (oldPosAsConstant - precisionAsConstant);
68 gradient.at(steppingParameter) - logarithmicBarrierTerm / (
utility::one<ConstantType>() - precisionAsConstant - oldPosAsConstant);
71 if (oldPosAsConstant < precisionAsConstant) {
78 projectedGradient = gradient.at(steppingParameter);
83 if (Adam* adam = boost::get<Adam>(&gradientDescentType)) {
86 adam->decayingStepAverage[steppingParameter] =
87 adam->averageDecay * adam->decayingStepAverage[steppingParameter] + (
utility::one<ConstantType>() - adam->averageDecay) * projectedGradient;
88 adam->decayingStepAverageSquared[steppingParameter] = adam->squaredAverageDecay * adam->decayingStepAverageSquared[steppingParameter] +
91 const ConstantType correctedGradient =
93 const ConstantType correctedSquaredGradient =
96 const ConstantType toSqrt = correctedSquaredGradient;
97 ConstantType sqrtResult = constantTypeSqrt(toSqrt);
99 step = (adam->learningRate / (sqrtResult + precisionAsConstant)) * correctedGradient;
100 }
else if (RAdam* radam = boost::get<RAdam>(&gradientDescentType)) {
108 radam->decayingStepAverageSquared[steppingParameter] = radam->squaredAverageDecay * radam->decayingStepAverageSquared[steppingParameter] +
111 radam->decayingStepAverage[steppingParameter] =
112 radam->averageDecay * radam->decayingStepAverage[steppingParameter] + (
utility::one<ConstantType>() - radam->averageDecay) * projectedGradient;
114 const ConstantType biasCorrectedMovingAverage =
116 const ConstantType squaredAverageDecayPow =
utility::pow(radam->squaredAverageDecay, stepNum + 1);
118 const ConstantType lengthApproxSMA =
122 if (lengthApproxSMA > 4) {
124 const ConstantType adaptiveLearningRate =
125 constantTypeSqrt((
utility::one<ConstantType>() - squaredAverageDecayPow) / radam->decayingStepAverageSquared[steppingParameter]);
127 const ConstantType varianceRectification =
128 constantTypeSqrt(((lengthApproxSMA - 4) / (maxLengthApproxSMA - 4)) * ((lengthApproxSMA - 2) / (maxLengthApproxSMA - 2)) *
129 ((maxLengthApproxSMA) / (lengthApproxSMA)));
131 step = radam->learningRate * varianceRectification * biasCorrectedMovingAverage * adaptiveLearningRate;
134 step = radam->learningRate * biasCorrectedMovingAverage;
136 }
else if (RmsProp* rmsProp = boost::get<RmsProp>(&gradientDescentType)) {
137 rmsProp->rootMeanSquare[steppingParameter] = rmsProp->averageDecay * rmsProp->rootMeanSquare[steppingParameter] +
140 const ConstantType toSqrt = rmsProp->rootMeanSquare[steppingParameter] + precisionAsConstant;
141 ConstantType sqrtResult = constantTypeSqrt(toSqrt);
143 step = (rmsProp->learningRate / sqrtResult) * projectedGradient;
144 }
else if (Plain* plain = boost::get<Plain>(&gradientDescentType)) {
147 step = -plain->learningRate;
149 step = plain->learningRate;
154 step = plain->learningRate * projectedGradient;
156 }
else if (Momentum* momentum = boost::get<Momentum>(&gradientDescentType)) {
159 step = -momentum->learningRate;
161 step = momentum->learningRate;
166 step = momentum->learningRate * projectedGradient;
168 step += momentum->momentumTerm * momentum->pastStep.at(steppingParameter);
169 momentum->pastStep[steppingParameter] = step;
170 }
else if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
173 step = -nesterov->learningRate;
175 step = nesterov->learningRate;
180 step = nesterov->learningRate * projectedGradient;
182 step += nesterov->momentumTerm * nesterov->pastStep.at(steppingParameter);
183 nesterov->pastStep[steppingParameter] = step;
190 position[steppingParameter] = newPos;
196 position[steppingParameter] =
utility::max(lower, position[steppingParameter]);
197 position[steppingParameter] =
utility::min(upper, position[steppingParameter]);
202template<
typename FunctionType,
typename ConstantType>
204GradientDescentInstantiationSearcher<FunctionType, ConstantType>::stochasticGradientDescent(
206 uint_fast64_t initialStateModel = model.getStates(
"init").getNextSetIndex(0);
208 ExtendedConstantType currentValue;
209 switch (this->synthesisTask->getBound().comparisonType) {
221 uint64_t tinyChangeIterations = 0;
223 std::map<VariableType<FunctionType>, ConstantType> deltaVector;
225 std::vector<VariableType<FunctionType>> parameterEnumeration;
226 for (
auto parameter : this->parameters) {
227 parameterEnumeration.push_back(parameter);
230 utility::Stopwatch printUpdateStopwatch;
231 printUpdateStopwatch.start();
235 uint_fast64_t parameterNum = 0;
236 for (uint_fast64_t stepNum = 0;
true; ++stepNum) {
237 if (printUpdateStopwatch.getTimeInSeconds() >= 15) {
238 printUpdateStopwatch.restart();
242 std::vector<VariableType<FunctionType>> miniBatch;
243 for (uint_fast64_t i = parameterNum;
i < std::min((uint_fast64_t)parameterEnumeration.size(), parameterNum + miniBatchSize);
i++) {
244 miniBatch.push_back(parameterEnumeration[i]);
247 ExtendedConstantType oldValue = currentValue;
252 if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
254 for (
auto const& parameter : miniBatch) {
255 ConstantType
const addedTerm = nesterov->momentumTerm * nesterov->pastStep[parameter];
257 nesterovPredictedPosition[parameter] =
utility::max(precision, nesterovPredictedPosition[parameter]);
258 nesterovPredictedPosition[parameter] =
utility::min(upperBound, nesterovPredictedPosition[parameter]);
263 for (
auto const& parameter : parameters) {
264 nesterovPredictedPosition[parameter] =
281 bool stochasticPosition =
true;
282 for (
auto const& parameter : parameters) {
283 if (nesterovPredictedPosition[parameter] < 0 + precision || nesterovPredictedPosition[parameter] > 1 - precision) {
284 stochasticPosition =
false;
289 bool computeValue =
true;
291 if (!stochasticPosition) {
292 computeValue =
false;
297 std::unique_ptr<storm::modelchecker::CheckResult> intermediateResult = instantiationModelChecker->check(env, nesterovPredictedPosition);
298 std::vector<ConstantType> valueVector = intermediateResult->asExplicitQuantitativeCheckResult<ConstantType>().getFiniteValueVector();
299 if (boost::get<Nesterov>(&gradientDescentType)) {
302 for (
auto const& parameter : parameters) {
303 modelCheckPosition[parameter] =
309 std::unique_ptr<storm::modelchecker::CheckResult> terminationResult = instantiationModelChecker->check(env, modelCheckPosition);
310 std::vector<ConstantType> terminationValueVector = terminationResult->asExplicitQuantitativeCheckResult<ConstantType>().getFiniteValueVector();
311 currentValue = terminationValueVector[initialStateModel];
313 currentValue = valueVector[initialStateModel];
316 if (synthesisTask->getBound().isSatisfied(currentValue) && stochasticPosition) {
320 for (
auto const& parameter : miniBatch) {
321 auto checkResult = derivativeEvaluationHelper->check(env, nesterovPredictedPosition, parameter, valueVector);
322 ConstantType delta =
storm::utility::getFinite(checkResult->getValueVector()[derivativeEvaluationHelper->getInitialState()]);
327 deltaVector[parameter] = delta;
340 VisualizationPoint point;
341 point.position = nesterovPredictedPosition;
342 point.value = currentValue;
343 walk.push_back(point);
350 for (
auto const& parameter : miniBatch) {
351 doStep(parameter, position, deltaVector, stepNum);
355 tinyChangeIterations += miniBatch.size();
356 if (tinyChangeIterations > parameterEnumeration.size()) {
360 tinyChangeIterations = 0;
364 parameterNum = parameterNum + miniBatchSize;
365 if (parameterNum >= parameterEnumeration.size()) {
370 STORM_LOG_WARN(
"Aborting Gradient Descent, returning non-optimal value.");
377template<
typename FunctionType,
typename ConstantType>
381 STORM_LOG_ASSERT(this->synthesisTask,
"Call setup before calling gradientDescent.");
383 resetDynamicValues();
385 STORM_LOG_ASSERT(this->synthesisTask->isBoundSet(),
"Task does not involve a bound.");
389 std::optional<ExtendedConstantType> bestValue;
391 std::random_device device;
392 std::default_random_engine engine(device());
393 std::uniform_real_distribution<> dist(0, 1);
394 bool initialGuess =
true;
399 STORM_LOG_PROGRESS(
"Trying initial guess (p->0.5 for every parameter p or set start point)\n");
402 for (
auto const& param : this->parameters) {
406 point[param] = (*startPoint)[param];
418 initialGuess =
false;
422 stochasticWatch.start();
425 stochasticWatch.stop();
427 bool isFoundPointBetter = !bestValue;
429 switch (this->synthesisTask->getBound().comparisonType) {
432 isFoundPointBetter = prob > *bestValue;
436 isFoundPointBetter = prob < *bestValue;
440 if (isFoundPointBetter) {
441 bestInstantiation = point;
445 if (synthesisTask->getBound().isSatisfied(*bestValue)) {
452 logarithmicBarrierTerm = logarithmicBarrierTerm / 10;
453 STORM_LOG_PROGRESS(
"Smaller term\n" << *bestValue <<
"\n" << logarithmicBarrierTerm <<
"\n");
456 STORM_LOG_PROGRESS(
"Sorry, couldn't satisfy the bound (yet). Best found value so far: " << *bestValue <<
"\n");
463 for (
auto const& parameter : parameters) {
464 bestInstantiation[parameter] =
471 STORM_LOG_ASSERT(bestValue.has_value(),
"Expected at least one evaluated instantiation.");
472 return std::make_pair(bestInstantiation, *bestValue);
475template<
typename FunctionType,
typename ConstantType>
476void GradientDescentInstantiationSearcher<FunctionType, ConstantType>::resetDynamicValues() {
477 if (Adam* adam = boost::get<Adam>(&gradientDescentType)) {
478 for (
auto const& parameter : this->parameters) {
482 }
else if (RAdam* radam = boost::get<RAdam>(&gradientDescentType)) {
483 for (
auto const& parameter : this->parameters) {
487 }
else if (RmsProp* rmsProp = boost::get<RmsProp>(&gradientDescentType)) {
488 for (
auto const& parameter : this->parameters) {
491 }
else if (Momentum* momentum = boost::get<Momentum>(&gradientDescentType)) {
492 for (
auto const& parameter : this->parameters) {
495 }
else if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
496 for (
auto const& parameter : this->parameters) {
502template<
typename FunctionType,
typename ConstantType>
506 for (
auto s = walk.begin(); s != walk.end(); ++s) {
508 auto point = s->position;
509 for (
auto iter = point.begin(); iter != point.end(); ++iter) {
510 std::cout <<
"\"" << iter->first.name() <<
"\"";
513 std::cout <<
"\"value\":" << s->value <<
"}";
514 if (std::next(s) != walk.end()) {
520 std::cout << storm::utility::convertNumber<double>(walk.at(walk.size() - 1).value) <<
"\n";
523template<
typename FunctionType,
typename ConstantType>
524std::vector<typename GradientDescentInstantiationSearcher<FunctionType, ConstantType>::VisualizationPoint>
void printRunAsJson()
Print the previously done run as JSON.
storm::utility::ExtendedValueType< ConstantType > ExtendedConstantType
std::pair< std::map< typename utility::parametric::VariableType< FunctionType >::type, typename utility::parametric::CoefficientType< FunctionType >::type >, ExtendedConstantType > gradientDescent()
Perform Gradient Descent.
std::vector< VisualizationPoint > getVisualizationWalk()
Get the visualization walk that is recorded if recordRun is set to true in the constructor (false by ...
#define STORM_LOG_WARN(message)
#define STORM_LOG_PROGRESS(message)
#define STORM_LOG_ERROR(message)
#define STORM_LOG_ASSERT(cond, message)
typename utility::parametric::CoefficientType< FunctionType >::type CoefficientType
typename utility::parametric::VariableType< FunctionType >::type VariableType
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
ValueType max(ValueType const &first, ValueType const &second)
ExtendedValueType< ValueType > positiveInfinity()
bool isFinite(ExtendedNumber< ValueType > const &value)
ExtendedValueType< ValueType > negativeInfinity()
ValueType min(ValueType const &first, ValueType const &second)
ValueType abs(ValueType const &number)
ValueType pow(ValueType const &value, int_fast64_t exponent)
ValueType const & getFinite(ExtendedNumber< ValueType > const &value)
TargetType convertNumber(SourceType const &number)