18template<
typename FunctionType>
20template<
typename FunctionType>
23template<
typename FunctionType,
typename ConstantType>
27 const ConstantType precisionAsConstant =
28 utility::convertNumber<ConstantType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
30 storm::utility::convertNumber<CoefficientType<FunctionType>>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
32 ConstantType
const oldPosAsConstant = utility::convertNumber<ConstantType>(position[steppingParameter]);
34 ConstantType projectedGradient;
37 ConstantType newPlainPosition = oldPosAsConstant + precisionAsConstant * gradient.at(steppingParameter);
39 region ? utility::convertNumber<ConstantType>(region->getLowerBoundary(steppingParameter)) : utility::zero<ConstantType>() + precisionAsConstant;
41 region ? utility::convertNumber<ConstantType>(region->getUpperBoundary(steppingParameter)) : utility::one<ConstantType>() - precisionAsConstant;
42 if (newPlainPosition < lower || newPlainPosition > upper) {
43 projectedGradient = 0;
45 projectedGradient = gradient.at(steppingParameter);
49 const double expX = std::exp(utility::convertNumber<double>(oldPos));
50 projectedGradient = gradient.at(steppingParameter) * utility::convertNumber<ConstantType>(expX / std::pow(expX + 1, 2));
52 if (oldPosAsConstant < precisionAsConstant) {
53 projectedGradient = 1000;
54 }
else if (oldPosAsConstant > utility::one<ConstantType>() - precisionAsConstant) {
55 projectedGradient = -1000;
57 projectedGradient = gradient.at(steppingParameter);
66 if (oldPosAsConstant >= precisionAsConstant && oldPosAsConstant <= utility::one<ConstantType>() - precisionAsConstant) {
68 if (oldPosAsConstant * 2 < utility::one<ConstantType>()) {
69 projectedGradient = gradient.at(steppingParameter) + logarithmicBarrierTerm / (oldPosAsConstant - precisionAsConstant);
72 gradient.at(steppingParameter) - logarithmicBarrierTerm / (utility::one<ConstantType>() - precisionAsConstant - oldPosAsConstant);
75 if (oldPosAsConstant < precisionAsConstant) {
76 projectedGradient = utility::one<ConstantType>() / logarithmicBarrierTerm;
77 }
else if (oldPosAsConstant > utility::one<ConstantType>() - precisionAsConstant) {
78 projectedGradient = -utility::one<ConstantType>() / logarithmicBarrierTerm;
82 projectedGradient = gradient.at(steppingParameter);
87 if (Adam* adam = boost::get<Adam>(&gradientDescentType)) {
90 adam->decayingStepAverage[steppingParameter] =
91 adam->averageDecay * adam->decayingStepAverage[steppingParameter] + (utility::one<ConstantType>() - adam->averageDecay) * projectedGradient;
92 adam->decayingStepAverageSquared[steppingParameter] = adam->squaredAverageDecay * adam->decayingStepAverageSquared[steppingParameter] +
93 (utility::one<ConstantType>() - adam->squaredAverageDecay) *
utility::pow(projectedGradient, 2);
95 const ConstantType correctedGradient =
96 adam->decayingStepAverage[steppingParameter] / (utility::one<ConstantType>() -
utility::pow(adam->averageDecay, stepNum + 1));
97 const ConstantType correctedSquaredGradient =
98 adam->decayingStepAverageSquared[steppingParameter] / (utility::one<ConstantType>() -
utility::pow(adam->squaredAverageDecay, stepNum + 1));
100 const ConstantType toSqrt = correctedSquaredGradient;
101 ConstantType sqrtResult = constantTypeSqrt(toSqrt);
103 step = (adam->learningRate / (sqrtResult + precisionAsConstant)) * correctedGradient;
104 }
else if (RAdam* radam = boost::get<RAdam>(&gradientDescentType)) {
109 const ConstantType maxLengthApproxSMA = 2 / (utility::one<ConstantType>() - radam->squaredAverageDecay) - utility::one<ConstantType>();
112 radam->decayingStepAverageSquared[steppingParameter] = radam->squaredAverageDecay * radam->decayingStepAverageSquared[steppingParameter] +
113 (utility::one<ConstantType>() - radam->squaredAverageDecay) *
utility::pow(projectedGradient, 2);
115 radam->decayingStepAverage[steppingParameter] =
116 radam->averageDecay * radam->decayingStepAverage[steppingParameter] + (utility::one<ConstantType>() - radam->averageDecay) * projectedGradient;
118 const ConstantType biasCorrectedMovingAverage =
119 radam->decayingStepAverage[steppingParameter] / (utility::one<ConstantType>() -
utility::pow(radam->averageDecay, stepNum + 1));
120 const ConstantType squaredAverageDecayPow =
utility::pow(radam->squaredAverageDecay, stepNum + 1);
122 const ConstantType lengthApproxSMA =
124 ((2 * (utility::convertNumber<ConstantType>(stepNum) + utility::one<ConstantType>()) * squaredAverageDecayPow) / (1 - squaredAverageDecayPow));
126 if (lengthApproxSMA > 4) {
128 const ConstantType adaptiveLearningRate =
129 constantTypeSqrt((utility::one<ConstantType>() - squaredAverageDecayPow) / radam->decayingStepAverageSquared[steppingParameter]);
131 const ConstantType varianceRectification =
132 constantTypeSqrt(((lengthApproxSMA - 4) / (maxLengthApproxSMA - 4)) * ((lengthApproxSMA - 2) / (maxLengthApproxSMA - 2)) *
133 ((maxLengthApproxSMA) / (lengthApproxSMA)));
135 step = radam->learningRate * varianceRectification * biasCorrectedMovingAverage * adaptiveLearningRate;
138 step = radam->learningRate * biasCorrectedMovingAverage;
140 }
else if (RmsProp* rmsProp = boost::get<RmsProp>(&gradientDescentType)) {
141 rmsProp->rootMeanSquare[steppingParameter] = rmsProp->averageDecay * rmsProp->rootMeanSquare[steppingParameter] +
142 (utility::one<ConstantType>() - rmsProp->averageDecay) * projectedGradient * projectedGradient;
144 const ConstantType toSqrt = rmsProp->rootMeanSquare[steppingParameter] + precisionAsConstant;
145 ConstantType sqrtResult = constantTypeSqrt(toSqrt);
147 step = (rmsProp->learningRate / sqrtResult) * projectedGradient;
148 }
else if (Plain* plain = boost::get<Plain>(&gradientDescentType)) {
150 if (projectedGradient < utility::zero<ConstantType>()) {
151 step = -plain->learningRate;
152 }
else if (projectedGradient > utility::zero<ConstantType>()) {
153 step = plain->learningRate;
155 step = utility::zero<ConstantType>();
158 step = plain->learningRate * projectedGradient;
160 }
else if (Momentum* momentum = boost::get<Momentum>(&gradientDescentType)) {
162 if (projectedGradient < utility::zero<ConstantType>()) {
163 step = -momentum->learningRate;
164 }
else if (projectedGradient > utility::zero<ConstantType>()) {
165 step = momentum->learningRate;
167 step = utility::zero<ConstantType>();
170 step = momentum->learningRate * projectedGradient;
172 step += momentum->momentumTerm * momentum->pastStep.at(steppingParameter);
173 momentum->pastStep[steppingParameter] = step;
174 }
else if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
176 if (projectedGradient < utility::zero<ConstantType>()) {
177 step = -nesterov->learningRate;
178 }
else if (projectedGradient > utility::zero<ConstantType>()) {
179 step = nesterov->learningRate;
181 step = utility::zero<ConstantType>();
184 step = nesterov->learningRate * projectedGradient;
186 step += nesterov->momentumTerm * nesterov->pastStep.at(steppingParameter);
187 nesterov->pastStep[steppingParameter] = step;
194 position[steppingParameter] = newPos;
197 auto const lower = region ? region->getLowerBoundary(steppingParameter) : utility::zero<CoefficientType<FunctionType>>() + precision;
198 auto const upper = region ? region->getUpperBoundary(steppingParameter) : utility::one<CoefficientType<FunctionType>>() - precision;
200 position[steppingParameter] =
utility::max(lower, position[steppingParameter]);
201 position[steppingParameter] =
utility::min(upper, position[steppingParameter]);
203 return utility::abs<ConstantType>(oldPosAsConstant - utility::convertNumber<ConstantType>(position[steppingParameter]));
206template<
typename FunctionType,
typename ConstantType>
207ConstantType GradientDescentInstantiationSearcher<FunctionType, ConstantType>::stochasticGradientDescent(
208 std::map<VariableType<FunctionType>, CoefficientType<FunctionType>>& position) {
209 uint_fast64_t initialStateModel = model.getStates(
"init").getNextSetIndex(0);
211 ConstantType currentValue;
212 switch (this->synthesisTask->getBound().comparisonType) {
215 currentValue = -utility::infinity<ConstantType>();
219 currentValue = utility::infinity<ConstantType>();
224 uint64_t tinyChangeIterations = 0;
226 std::map<VariableType<FunctionType>, ConstantType> deltaVector;
228 std::vector<VariableType<FunctionType>> parameterEnumeration;
229 for (
auto parameter : this->parameters) {
230 parameterEnumeration.push_back(parameter);
233 utility::Stopwatch printUpdateStopwatch;
234 printUpdateStopwatch.start();
238 uint_fast64_t parameterNum = 0;
239 for (uint_fast64_t stepNum = 0;
true; ++stepNum) {
240 if (printUpdateStopwatch.getTimeInSeconds() >= 15) {
241 printUpdateStopwatch.restart();
245 std::vector<VariableType<FunctionType>> miniBatch;
246 for (uint_fast64_t i = parameterNum;
i < std::min((uint_fast64_t)parameterEnumeration.size(), parameterNum + miniBatchSize);
i++) {
247 miniBatch.push_back(parameterEnumeration[i]);
250 ConstantType oldValue = currentValue;
251 CoefficientType<FunctionType>
const precision = storm::utility::convertNumber<CoefficientType<FunctionType>>(
252 storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
255 std::map<VariableType<FunctionType>, CoefficientType<FunctionType>> nesterovPredictedPosition(position);
256 if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
257 CoefficientType<FunctionType>
const upperBound = (utility::one<CoefficientType<FunctionType>>() - precision);
258 for (
auto const& parameter : miniBatch) {
259 ConstantType
const addedTerm = nesterov->momentumTerm * nesterov->pastStep[parameter];
260 nesterovPredictedPosition[parameter] += storm::utility::convertNumber<CoefficientType<FunctionType>>(addedTerm);
261 nesterovPredictedPosition[parameter] =
utility::max(precision, nesterovPredictedPosition[parameter]);
262 nesterovPredictedPosition[parameter] =
utility::min(upperBound, nesterovPredictedPosition[parameter]);
267 for (
auto const& parameter : parameters) {
268 nesterovPredictedPosition[parameter] =
269 utility::one<CoefficientType<FunctionType>>() /
271 utility::convertNumber<CoefficientType<FunctionType>>(std::exp(-utility::convertNumber<double>(nesterovPredictedPosition[parameter]))));
285 bool stochasticPosition =
true;
286 for (
auto const& parameter : parameters) {
287 if (nesterovPredictedPosition[parameter] < 0 + precision || nesterovPredictedPosition[parameter] > 1 - precision) {
288 stochasticPosition =
false;
293 bool computeValue =
true;
295 if (!stochasticPosition) {
296 computeValue =
false;
301 std::unique_ptr<storm::modelchecker::CheckResult> intermediateResult = instantiationModelChecker->check(env, nesterovPredictedPosition);
302 std::vector<ConstantType> valueVector = intermediateResult->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
303 if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
304 std::map<VariableType<FunctionType>, CoefficientType<FunctionType>> modelCheckPosition(position);
306 for (
auto const& parameter : parameters) {
307 modelCheckPosition[parameter] =
308 utility::one<CoefficientType<FunctionType>>() /
310 utility::convertNumber<CoefficientType<FunctionType>>(std::exp(-utility::convertNumber<double>(modelCheckPosition[parameter]))));
313 std::unique_ptr<storm::modelchecker::CheckResult> terminationResult = instantiationModelChecker->check(env, modelCheckPosition);
314 std::vector<ConstantType> terminationValueVector = terminationResult->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
315 currentValue = terminationValueVector[initialStateModel];
317 currentValue = valueVector[initialStateModel];
320 if (synthesisTask->getBound().isSatisfied(currentValue) && stochasticPosition) {
324 for (
auto const& parameter : miniBatch) {
325 auto checkResult = derivativeEvaluationHelper->check(env, nesterovPredictedPosition, parameter, valueVector);
326 ConstantType delta = checkResult->getValueVector()[derivativeEvaluationHelper->getInitialState()];
331 deltaVector[parameter] = delta;
336 currentValue = utility::infinity<ConstantType>();
338 currentValue = -utility::infinity<ConstantType>();
344 VisualizationPoint point;
345 point.position = nesterovPredictedPosition;
346 point.value = currentValue;
347 walk.push_back(point);
354 for (
auto const& parameter : miniBatch) {
355 doStep(parameter, position, deltaVector, stepNum);
358 if (storm::utility::abs<ConstantType>(oldValue - currentValue) < terminationEpsilon) {
359 tinyChangeIterations += miniBatch.size();
360 if (tinyChangeIterations > parameterEnumeration.size()) {
364 tinyChangeIterations = 0;
368 parameterNum = parameterNum + miniBatchSize;
369 if (parameterNum >= parameterEnumeration.size()) {
374 STORM_LOG_WARN(
"Aborting Gradient Descent, returning non-optimal value.");
381template<
typename FunctionType,
typename ConstantType>
382std::pair<std::map<VariableType<FunctionType>, CoefficientType<FunctionType>>, ConstantType>
384 STORM_LOG_ASSERT(this->synthesisTask,
"Call setup before calling gradientDescent");
386 resetDynamicValues();
388 STORM_LOG_ASSERT(this->synthesisTask->isBoundSet(),
"Task does not involve a bound.");
391 ConstantType bestValue;
392 switch (this->synthesisTask->getBound().comparisonType) {
395 bestValue = -utility::infinity<ConstantType>();
399 bestValue = utility::infinity<ConstantType>();
403 std::random_device device;
404 std::default_random_engine engine(device());
405 std::uniform_real_distribution<> dist(0, 1);
406 bool initialGuess =
true;
411 STORM_PRINT_AND_LOG(
"Trying initial guess (p->0.5 for every parameter p or set start point)\n");
414 for (
auto const& param : this->parameters) {
416 logarithmicBarrierTerm = utility::convertNumber<ConstantType>(0.1);
418 point[param] = (*startPoint)[param];
420 point[param] = utility::convertNumber<CoefficientType<FunctionType>>(0.5 + 1e-6);
423 logarithmicBarrierTerm > utility::convertNumber<ConstantType>(0.00001)) {
426 logarithmicBarrierTerm = utility::convertNumber<ConstantType>(0.1);
427 point[param] = utility::convertNumber<CoefficientType<FunctionType>>(dist(engine));
430 initialGuess =
false;
434 stochasticWatch.start();
436 ConstantType prob = stochasticGradientDescent(point);
437 stochasticWatch.stop();
439 bool isFoundPointBetter =
false;
440 switch (this->synthesisTask->getBound().comparisonType) {
443 isFoundPointBetter = prob > bestValue;
447 isFoundPointBetter = prob < bestValue;
450 if (isFoundPointBetter) {
451 bestInstantiation = point;
455 if (synthesisTask->getBound().isSatisfied(bestValue)) {
462 logarithmicBarrierTerm = logarithmicBarrierTerm / 10;
463 STORM_PRINT_AND_LOG(
"Smaller term\n" << bestValue <<
"\n" << logarithmicBarrierTerm <<
"\n");
466 STORM_PRINT_AND_LOG(
"Sorry, couldn't satisfy the bound (yet). Best found value so far: " << bestValue <<
"\n");
473 for (
auto const& parameter : parameters) {
474 bestInstantiation[parameter] =
475 utility::one<CoefficientType<FunctionType>>() /
477 utility::convertNumber<CoefficientType<FunctionType>>(std::exp(-utility::convertNumber<double>(bestInstantiation[parameter]))));
481 return std::make_pair(bestInstantiation, bestValue);
484template<
typename FunctionType,
typename ConstantType>
486 if (Adam* adam = boost::get<Adam>(&gradientDescentType)) {
487 for (
auto const& parameter : this->parameters) {
488 adam->decayingStepAverage[parameter] = utility::zero<ConstantType>();
489 adam->decayingStepAverageSquared[parameter] = utility::zero<ConstantType>();
491 }
else if (RAdam* radam = boost::get<RAdam>(&gradientDescentType)) {
492 for (
auto const& parameter : this->parameters) {
493 radam->decayingStepAverage[parameter] = utility::zero<ConstantType>();
494 radam->decayingStepAverageSquared[parameter] = utility::zero<ConstantType>();
496 }
else if (RmsProp* rmsProp = boost::get<RmsProp>(&gradientDescentType)) {
497 for (
auto const& parameter : this->parameters) {
498 rmsProp->rootMeanSquare[parameter] = utility::zero<ConstantType>();
500 }
else if (Momentum* momentum = boost::get<Momentum>(&gradientDescentType)) {
501 for (
auto const& parameter : this->parameters) {
502 momentum->pastStep[parameter] = utility::zero<ConstantType>();
504 }
else if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
505 for (
auto const& parameter : this->parameters) {
506 nesterov->pastStep[parameter] = utility::zero<ConstantType>();
511template<
typename FunctionType,
typename ConstantType>
514 for (
auto s = walk.begin(); s != walk.end(); ++s) {
516 auto point = s->position;
517 for (
auto iter = point.begin(); iter != point.end(); ++iter) {
519 STORM_PRINT(
":" << utility::convertNumber<double>(iter->second) <<
",");
522 if (std::next(s) != walk.end()) {
528 STORM_PRINT(storm::utility::convertNumber<double>(walk.at(walk.size() - 1).value) <<
"\n");
531template<
typename FunctionType,
typename ConstantType>
532std::vector<typename GradientDescentInstantiationSearcher<FunctionType, ConstantType>::VisualizationPoint>
void printRunAsJson()
Print the previously done run as JSON.
std::vector< VisualizationPoint > getVisualizationWalk()
Get the visualization walk that is recorded if recordRun is set to true in the constructor (false by ...
std::pair< std::map< typename utility::parametric::VariableType< FunctionType >::type, typename utility::parametric::CoefficientType< FunctionType >::type >, ConstantType > gradientDescent()
Perform Gradient Descent.
#define STORM_LOG_WARN(message)
#define STORM_LOG_ERROR(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_PRINT_AND_LOG(message)
#define STORM_PRINT(message)
Define the macros that print information and optionally also log it.
typename utility::parametric::VariableType< FunctionType >::type VariableType
typename utility::parametric::CoefficientType< FunctionType >::type CoefficientType
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
ValueType max(ValueType const &first, ValueType const &second)
ValueType min(ValueType const &first, ValueType const &second)
ValueType pow(ValueType const &value, int_fast64_t exponent)