This is to test and illustrate a very basic case of optimization, with types $A$ and $B$, a term $a : A$ and a function $f: A \to B$. We have $f(a)$ as a generator initially, but this should drop out if we have high weight for entropy.
import $cp.bin.`provingground-core-jvm-4d3ce04.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
val A = "A" :: Type
val B = "B" :: Type
val a = "a" :: A
val f = "f" :: (A ->: B)
val ts = TermState(FiniteDistribution.unif(a, f, f(a)), FiniteDistribution.unif(A, B))
val lp = LocalProver(ts).noIsles
val tunedT = lp.tunedGenerators
import monix.execution.Scheduler.Implicits.global
val tunedF = tunedT.runToFuture
lp.nextState.runToFuture
lp.expressionEval.map(_.entropy()).runToFuture
lp.expressionEval.flatMap(_.generatorIterant(1, 1, 0.0001).headOptionL).runToFuture
lp.expressionEval.flatMap(_.generatorIterant(1, 1, 0.0001).take(1000).lastOptionL).runToFuture
lp.expressionEval.flatMap(_.generatorIterant(1, 10, 0.0001).take(1000).lastOptionL).runToFuture
lp.expressionEval.flatMap(_.generatorIterant(0.01, 10, 0.000001).take(1000).lastOptionL).runToFuture
val lp0 = LocalProver(TermState(FiniteDistribution.unif(a, f(a)), FiniteDistribution.unif(A, B)), TermGenParams.zero)
lp0.tunedGenerators.runToFuture
val lp1 = LocalProver(TermState(FiniteDistribution(a -> 0.8, f(a) -> 0.2), FiniteDistribution.unif(A, B)), TermGenParams.zero)
lp1.tunedGenerators.runToFuture
val lp2 = LocalProver(TermState(FiniteDistribution(a -> 0.8, f(a) -> 0.2), FiniteDistribution.unif(A, B)), TermGenParams.zero, klW = 0.00001)
lp2.tunedGenerators.runToFuture
val lp3 = LocalProver(TermState(FiniteDistribution(a -> 0.8, f(a) -> 0.2), FiniteDistribution.unif(A, B)), TermGenParams.zero, klW = 0.1)
lp3.tunedGenerators.runToFuture
val lp4 = LocalProver(TermState(FiniteDistribution(a -> 0.8, f(a) -> 0.2), FiniteDistribution.unif(A, B)), TermGenParams.zero, klW = 0.4)
lp4.tunedGenerators.runToFuture
lp.expressionEval.flatMap(_.generatorIterant(0.0001, 10, 0.000001).take(1000).lastOptionL).runToFuture
lp.expressionEval.flatMap(_.generatorIterant(0.00001, 10, 0.00000001).take(1000).lastOptionL).runToFuture
The code seems correct, but there seems to almost be a phase transition, and for far more unequal weights than expected. The above seems to be the stable case.
val ts = TermState(FiniteDistribution.unif(a, f), FiniteDistribution(A -> 0.01, B -> 0.99))
val lp5 = LocalProver(ts, hW = 0.0001).noIsles
lp5.tunedGenerators.runToFuture
val lp6 = LocalProver(ts, hW = 0.1).noIsles
lp6.tunedGenerators.runToFuture
val ts1 = TermState(FiniteDistribution.unif(a, f), FiniteDistribution(A -> 0.05, B -> 0.95))
val lp7 = LocalProver(ts1, hW = 0.0001).noIsles
lp7.tunedGenerators.runToFuture
lp7.expressionEval.map(_.initTerms).runToFuture
lp7.expressionEval.map(_.vars).runToFuture
val ts2 = TermState(FiniteDistribution.unif(a, f, f(a)), FiniteDistribution(A -> 0.01, B -> 0.99))
val lp8 = LocalProver(ts2, hW = 0.0001).noIsles
lp8.tunedGenerators.runToFuture
val ts3 = TermState(FiniteDistribution.unif(a, f, f(a)), FiniteDistribution(A -> 0.05, B -> 0.95))
val lp9 = LocalProver(ts3, hW = 0.0001).noIsles
val ts4 = TermState(FiniteDistribution.unif(a, f, f(a)), FiniteDistribution(A -> 0.1, B -> 0.9))
val lp10 = LocalProver(ts4, hW = 0.0001).noIsles
lp9.tunedGenerators.runToFuture
lp10.tunedGenerators.runToFuture
val lp11 = LocalProver(ts2, hW = 0.01).noIsles
lp11.tunedGenerators.runToFuture
ts2
val lp12 = LocalProver(ts2, hW = 0.00001, klW = 10).noIsles
lp12.tunedGenerators.runToFuture
lp12.nextState.runToFuture
lp12.tripleT.runToFuture
lp12.tripleTypT.runToFuture
val ts5 = TermState(FiniteDistribution.unif(a, f, f(a)), FiniteDistribution(A -> 0.001, B -> 0.999))
val lp13 = LocalProver(ts5, hW = 0.0001, klW= 10).noIsles
lp13.tunedGenerators.runToFuture
val ts6 = TermState(FiniteDistribution.unif(a, f, f(a)), FiniteDistribution(A -> 0.0001, B -> 0.9999))
val lp14 = LocalProver(ts6, hW = 0.0001, klW= 10).noIsles
lp14.tunedGenerators.runToFuture
After experimentation with the rather simple generation, we find
lp14.expressionEval.map(_.finalDist).runToFuture
import GeneratorVariables._, Expression._, TermRandomVars._
lp14.expressionEval.map(_.finalDist(FinalVal(Elem(f(a), Terms)))).runToFuture
lp14.expressionEval.map(_.entropy(0.0001, 10)).runToFuture
val epT = for {
ev <- lp14.expressionEval
q = ev.finalDist
entp <- ev.WithP(q).entropyProjectionTask(lp14.hW, lp14.klW)
} yield entp
val epF = epT.runToFuture
val entT = for {
ev <- lp14.expressionEval
q = ev.finalDist
der <- ev.WithP(q).jetTask(ev.entropy(lp14.hW, lp14.klW))
} yield der
val entF = entT.runToFuture
val varT = for {
ev <- lp14.expressionEval
vs = ev.vars
} yield vs
val varsF = varT.runToFuture
val klT0 = for {
ev <- lp14.expressionEval
q = ev.finalDist
vs = ev.vars
der <- ev.WithP(q).jetTask(ev.entropy(0, 1))
} yield der.infinitesimal.toVector.zip(vs)
val klF0 = klT0.runToFuture
val entT0 = for {
ev <- lp14.expressionEval
q = ev.finalDist
vs = ev.vars
der <- ev.WithP(q).jetTask(ev.entropy(1, 0))
} yield der.infinitesimal.toVector.zip(vs)
val entF0 = entT0.runToFuture
lp14.expressionEval.map(_.klExp).runToFuture
val shT = for {
ev <- lp14.expressionEval
q = ev.finalDist
vs = ev.vars
der <- ev.WithP(q).jetTask(ev.entropy(0, 1))
gs = ev.gradShift(q, der.infinitesimal.toVector, 1).toVector.collect{case (k, v) if q(k) != v => (k, q(k), v)}
} yield gs
val shF = shT.runToFuture
We note that the entropy shift increases the final value of the probability of $f(a)$, as it should be. Next we check directly for the generator iterant, but in this case initially.
val probT = for {
ev <- lp14.expressionEval
prob <- ev.generatorIterant(0, 1, 0.000001, ev.finalDist).map(_(f(a))).take(20).toListL
} yield prob
val probF = probT.runToFuture
val pshT = for {
ev <- lp14.expressionEval
q = ev.finalDist
vs = ev.vars
der <- ev.WithP(q).entropyProjectionTask(0, 1)
gs = ev.gradShift(q, der, 1).toVector.collect{case (k, v) if q(k) != v => (k, q(k), v)}
} yield gs
val pshF = pshT.runToFuture
val prstshT = for {
ev <- lp14.expressionEval
q = ev.finalDist
vs = ev.vars
der <- ev.WithP(q).entropyProjectionTask(0, 1)
gs = ev.stableGradShift(q, der, 1).toVector.collect{case (k @ InitialVal(Elem(_, Terms)), v) if q(k) != v => (k, q(k), v)}
} yield gs
val prstshF = prstshT.runToFuture
import ExpressionEval._
val ev14 = lp14.expressionEval
val gT = ev14.map(e => generators(e.finalDist))
val gF = gT.runToFuture
val gT = ev14.flatMap(e => e.generatorIterant(0, 1, 0.000001, e.finalDist).take(20).toListL)
val gF = gT.runToFuture
This is not expected behaviour: one would expect the weight of $f(a)$ to rise. Instead it rises for one step and then starts sinking. Should start with a clean notebook and track this down.
val lp0 = LocalProver(TermState(FiniteDistribution.unif(a, f(a), f), FiniteDistribution(A -> 0.01, B -> 0.99)), hW = 0, klW = 10).noIsles
val gT0 = lp0.expressionEval.flatMap(e => e.generatorIterant(0, 1, 0.000001, e.finalDist).take(100).toListL.map(_.zipWithIndex.filter(_._2 % 15 == 0)) )
val gF0 = gT0.runToFuture