Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.cross-entropy

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/cross_entropy.clj1 definitions, 3 theorems

AHoF O41 Cross-Entropy Method: a model-based stochastic optimizer that, each iteration, samples a population, keeps the top-scoring ELITE, and refits the sampling distribution to the elite. The elite-selection core is the membership test -- a sample is elite when its objective value reaches the elite threshold (the rho-quantile of the population scores): elite? score threshold = decide (threshold <= score) over the decidable rational order (maximization convention). Defined: the elite test. Proved native and axiom-free, as worked instances: score 7 against threshold 5 is elite, score 3 against threshold 5 is not, and the worked certificate 5 <= 7 (native nnrat/at-most). Soundness of the elite test for all scores, and the method's classical convergence behaviour, are not proved here. The population sampling, the quantile threshold computation, and the distribution refit are executable concerns. Requires nnrat/at-most, audit/decide-nnrat-at-most, and nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.cross-entropy` prints this classification.

cross-entropy/elite? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

cross-entropy/selects-elite :
  → bo/is-safe 7 5 = data/true

cross-entropy/elite-meets-threshold :
  → 5 ≤ 7

cross-entropy/excludes-non-elite :
  → bo/is-safe 3 5 = data/false