Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.cmaes

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

AHoF O42 CMA-ES (Covariance Matrix Adaptation Evolution Strategy) -- the mean recombination step. Each generation, the new distribution mean is the weighted recombination of the selected (elite) samples, ranked best first: recombine w1 x1 w2 x2 = w1 * x1 + w2 * x2 over the finite-vector search state (two elite; the general case folds this over all selected samples with the CMA recombination weights). The rank-one/rank-mu covariance-matrix updates and the step-size adaptation (involving eigen-decompositions and square roots) are executable / not exact-rational concerns; the recombination weights are supplied rationals summing to one. What is proved here is the deterministic weighted recombination and worked instances from a convex combination. Requires the shared finite-vector operations (vector/add, vector/scale) over signed rationals -- carried by the D63 checkpoint via the vector layer. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.cmaes` prints this classification.

Depends onmath.finite.vector

cmaes/recombine :
  (x₁ : ℚ≥0) (x₂ : List ℚ) (x₃ : ℚ≥0) (x₄ : List ℚ)
  → List ℚ

cmaes/recombine-unfold :
  (w1 : ℚ≥0) (x1 : List ℚ) (w2 : ℚ≥0) (x2 : List ℚ)
  → cmaes/recombine w1 x1 w2 x2 = vector/add (vector/scale w1 x1) (vector/scale w2 x2)

cmaes/recombine-top-example :
  → cmaes/recombine 1 [signed/from-nnrat 3, signed/from-nnrat 2] 0 [signed/from-nnrat 5, signed/from-nnrat 5] = [signed/from-nnrat 3, signed/from-nnrat 2]

cmaes/recombine-example :
  → cmaes/recombine 2 [signed/from-nnrat 3, signed/from-nnrat 2] 1 [signed/from-nnrat 1, signed/from-nnrat 4] = [signed/from-nnrat 7, signed/from-nnrat 8]