Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bayesian-opt

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/bayesian_opt.clj4 definitions, 4 theorems

Kochenderfer surrogate-optimization / model-validation cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O19.1 probability of improvement : acquisition prefers candidates beating the best O19.3 SafeOpt : query only within the high-confidence safe set O17.14 0.632 bootstrap : convex combo 0.368*train + 0.632*test error O17.12 bootstrap generalization : mean holdout error over resamples Improvement / safety are decidable-order tests with soundness (decide-at-most-true- sound); the bootstrap estimators reuse nnrat/wsum2 (bounded by the convex bound). Native and axiom-free; chains nnrat-convex (-> wsum2, minmax) on d63.

Depends onmath.rational.nnrat.convex

bo/is-improvement :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

bo/is-safe :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

bo/bootstrap-632 :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

bo/bootstrap-mean :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

bo/improvement-sound :
  (candidate best : ℚ≥0)
  (ok : bo/is-safe candidate best = data/true)
  → best ≤ candidate

bo/safe-sound :
  (lcb threshold : ℚ≥0)
  (ok : bo/is-safe lcb threshold = data/true)
  → threshold ≤ lcb

bo/bootstrap-632-within-max :
  (w-train w-test train test : ℚ≥0)
  (hw : w-train + w-test = 1)
  → bo/bootstrap-632 w-train w-test train test ≤ minmax/max train test

bo/bootstrap-mean-example :
  → bo/bootstrap-632 1/2 1/2 1 0 = 1/2