From 110f414207d632819dea4cf01a1ddaca86d0cca3 Mon Sep 17 00:00:00 2001 From: Martin Suda Date: Fri, 16 Oct 2020 16:55:15 +0200 Subject: [PATCH] model communicates logits rather than bools (good/bad) --- Kernel/Clause.cpp | 4 +-- Kernel/Clause.hpp | 10 +++--- .../PredicateSplitPassiveClauseContainer.cpp | 13 +++++--- Saturation/SaturationAlgorithm.cpp | 6 ++-- Shell/Options.cpp | 33 +++++++++++++++++++ Shell/Options.hpp | 2 ++ 6 files changed, 54 insertions(+), 14 deletions(-) diff --git a/Kernel/Clause.cpp b/Kernel/Clause.cpp index 5349c10cdc..a82636f6b1 100644 --- a/Kernel/Clause.cpp +++ b/Kernel/Clause.cpp @@ -75,7 +75,7 @@ Clause::Clause(unsigned length,const Inference& inf) _component(false), _store(NONE), _numSelected(0), - _modelSaidYes(1), // be optimistic by default (delayed eval takes care of demoting the bad guys) + _modelSaid(std::numeric_limits::lowest()), // be optimistic by default (delayed eval takes care of demoting the bad guys) _weight(0), _weightForClauseSelection(0), _refCnt(0), @@ -439,7 +439,7 @@ vstring Clause::toString() const } if(env.options->evalForKarel()) { - result += ",msY:" + Int::toString(_modelSaidYes); + result += ",msY:" + Int::toString(_modelSaid); } result += ",thAx:" + Int::toString((int)(_inference.th_ancestors)); diff --git a/Kernel/Clause.hpp b/Kernel/Clause.hpp index c2f2bc7ef0..80b6cea1be 100644 --- a/Kernel/Clause.hpp +++ b/Kernel/Clause.hpp @@ -346,12 +346,12 @@ class Clause unsigned numPositiveLiterals(); // number of positive literals in the clause - void modelSaid(bool value) { - _modelSaidYes = value; + void setModelSaid(float value) { + _modelSaid = value; } - bool modelSaidYes() const { - return _modelSaidYes; + float modelSaid() const { + return _modelSaid; } protected: @@ -374,7 +374,7 @@ class Clause /** number of selected literals */ unsigned _numSelected : 20; - unsigned _modelSaidYes : 1; + float _modelSaid; // small is good /** weight */ mutable unsigned _weight; diff --git a/Saturation/PredicateSplitPassiveClauseContainer.cpp b/Saturation/PredicateSplitPassiveClauseContainer.cpp index f6b8a5af6b..02de2338da 100644 --- a/Saturation/PredicateSplitPassiveClauseContainer.cpp +++ b/Saturation/PredicateSplitPassiveClauseContainer.cpp @@ -103,6 +103,7 @@ void PredicateSplitPassiveClauseContainer::add(Clause* cl) ASS(cl->store() == Clause::PASSIVE); auto bestQueueIndex = bestQueue(evaluateFeature(cl)); + if (_layeredArrangement) { // add clause to all queues starting from best queue for clause @@ -236,11 +237,12 @@ Clause* PredicateSplitPassiveClauseContainer::popSelected() if (currIndex < (long int)_queues.size()-1 && // not the last index _delayedEvaluator) { // we can re-evaluate + _delayedEvaluator(cl); if (evaluateFeature(cl) > _cutoffs[currIndex]) { // we don't like the clause here! - // cout << "Didn't like " << cl->number() << " in " << currIndex << endl; + //cout << "Didn't like " << cl->number() << " in " << currIndex << endl; goto search_for_an_appropriate_queue; } } @@ -566,20 +568,23 @@ float PositiveLiteralMultiSplitPassiveClauseContainer::evaluateFeatureEstimate(u NeuralEvalSplitPassiveClauseContainer::NeuralEvalSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector> queues) : PredicateSplitPassiveClauseContainer(isOutermost, opt, name, std::move(queues), - Lib::vvector({0.0, std::numeric_limits::max()}), + opt.neuralEvalSplitQueueCutoffs(), opt.neuralEvalSplitQueueRatios(), true /* monotone queue split hard-wired here */) {} float NeuralEvalSplitPassiveClauseContainer::evaluateFeature(Clause* cl) const { CALL("NeuralEvalSplitPassiveClauseContainer::evaluateFeature"); - return 1.0-(float)cl->modelSaidYes(); // 0.0 is good, 1.0 is bad (because the hard-wired < comparison in PredicateSplitPassiveClauseContainer) + + // cout << "evaluateFeature " << cl->number() << " " << cl->modelSaid() << endl; + + return cl->modelSaid(); // small is good, large is bad } float NeuralEvalSplitPassiveClauseContainer::evaluateFeatureEstimate(unsigned numPositiveLiterals, const Inference& inference) const { CALL("NeuralEvalSplitPassiveClauseContainer::evaluateFeatureEstimate"); - return 0.0; // simply estimate that the clause is good + return std::numeric_limits::lowest(); // simply estimate that the clause is good } }; diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index ff56667883..ea6ebbc6e3 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -215,7 +215,7 @@ static std::unique_ptr makeLevel5(bool isOutermost, cons if (opt.useNeuralEvalSplitQueues()) { Lib::vvector> queues; - Lib::vvector cutoffs = opt.positiveLiteralSplitQueueCutoffs(); + Lib::vvector cutoffs = opt.neuralEvalSplitQueueCutoffs(); for (unsigned i = 0; i < cutoffs.size(); i++) { auto queueName = name + "NESQ" + Int::toString(cutoffs[i]) + ":"; @@ -540,7 +540,7 @@ void SaturationAlgorithm::embed_and_evaluate(Clause* cl, const char* method_name inputs.push_back(id); auto out = _model.forward(inputs); - cl->modelSaid(out.toBool()); + cl->setModelSaid(-out.toDouble()); // already here, we reverse the logit's logic to "small is good"! } } @@ -1367,7 +1367,7 @@ void SaturationAlgorithm::addToPassive(Clause* cl) if (_opt.evalForKarel()) { // talkToKarel(cl); // delayed evaluation trick (TODO: do this for initial as well?) - cl->modelSaid(true); + // cl->modelSaid(true); // the clause is born as good; see Clause::Clause } { diff --git a/Shell/Options.cpp b/Shell/Options.cpp index da704a9af5..2bb4a28359 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -1021,6 +1021,12 @@ void Options::Options::init() _useNeuralEvalSplitQueues.reliesOn(_evalForKarel.is(notEqual(vstring("")))); _useNeuralEvalSplitQueues.tag(OptionTag::SATURATION); + _neuralEvalSplitQueueCutoffs = StringOptionValue("neural_eval_split_queue_cutoffs", "nesqc", "0"); + _neuralEvalSplitQueueCutoffs.description = "The cutoff-values for the neural-eval-split-queues (the cutoff value for the last queue is omitted, since it has to be infinity)."; + _lookup.insert(&_neuralEvalSplitQueueCutoffs); + _neuralEvalSplitQueueCutoffs.reliesOn(_useNeuralEvalSplitQueues.is(equal(true))); + _neuralEvalSplitQueueCutoffs.tag(OptionTag::SATURATION); + _neuralEvalSplitQueueRatios = StringOptionValue("neural_eval_split_queue_ratios", "nesqr", "10,1"); _neuralEvalSplitQueueRatios.description = "The ratios for picking clauses from the neural-eval-split-queues using weighted round robin. If a queue is empty, the clause will be picked from the next non-empty queue to the right." " There should be exactly two numbers in the list."; @@ -3529,3 +3535,30 @@ Lib::vvector Options::neuralEvalSplitQueueRatios() const return inputRatios; } +Lib::vvector Options::neuralEvalSplitQueueCutoffs() const +{ + CALL("Options::neuralEvalSplitQueueCutoffs"); + // initialize cutoffs and add float-max as last value + Lib::vvector cutoffs; + vstringstream cutoffsStream(_neuralEvalSplitQueueCutoffs.actualValue); + std::string currentCutoff; + while (std::getline(cutoffsStream, currentCutoff, ',')) + { + cutoffs.push_back(std::stof(currentCutoff)); + } + cutoffs.push_back(std::numeric_limits::max()); + + // sanity checks + for (unsigned i = 0; i < cutoffs.size(); i++) + { + auto cutoff = cutoffs[i]; + + if (i > 0 && cutoff <= cutoffs[i-1]) + { + USER_ERROR("The cutoff values (supplied by option '-nesqc') must be strictly increasing"); + } + } + + return cutoffs; +} + diff --git a/Shell/Options.hpp b/Shell/Options.hpp index 3144e18364..3b380062bf 100644 --- a/Shell/Options.hpp +++ b/Shell/Options.hpp @@ -2131,6 +2131,7 @@ bool _hard; bool useNeuralEvalSplitQueues() const { return _useNeuralEvalSplitQueues.actualValue; } Lib::vvector neuralEvalSplitQueueRatios() const; + Lib::vvector neuralEvalSplitQueueCutoffs() const; void setWeightRatio(int v){ _ageWeightRatio.otherValue = v; } AgeWeightRatioShape ageWeightRatioShape() const { return _ageWeightRatioShape.actualValue; } @@ -2413,6 +2414,7 @@ bool _hard; StringOptionValue _positiveLiteralSplitQueueCutoffs; BoolOptionValue _positiveLiteralSplitQueueLayeredArrangement; BoolOptionValue _useNeuralEvalSplitQueues; + StringOptionValue _neuralEvalSplitQueueCutoffs; StringOptionValue _neuralEvalSplitQueueRatios; BoolOptionValue _randomAWR;