Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.expected-improvement

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

AHoF O63 Expected Improvement acquisition (Bayesian optimization). EI balances exploitation and exploration: the expected amount by which a candidate improves on the current best combines the predicted improvement (weighted by its probability) with the predictive uncertainty (weighted by the density at the best): ei improvement prob uncertainty density = improvement * prob + uncertainty * density over exact nonnegative rationals. The predicted improvement (mean - best), the standard-normal CDF prob and density (involving exp and erf), and the surrogate sigma (a square root) are transcendental / executable concerns -- the probability and density VALUES are supplied as rationals. What is proved here is the deterministic acquisition combination and its guarantee: EI is at least the exploitation term (improvement * prob <= ei), so adding the exploration term never reduces the acquisition below pure exploitation. Requires nnrat/add, nnrat/multiply, nnrat/at-most, and the decidable nnrat order (all in the D63 checkpoint).

Depends onmath.rational.nnrat.add-upper

expected-improvement/ei :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

expected-improvement/ei-unfold :
  (improvement prob uncertainty density : ℚ≥0)
  → ekf/update improvement prob uncertainty density = improvement · prob + uncertainty · density

expected-improvement/ei-example :
  → ekf/update 3 2 1 4 = 10

expected-improvement/ei-at-least-exploitation :
  → 6 ≤ ekf/update 3 2 1 4

expected-improvement/ei-at-least-exploitation-universal :
  (improvement prob uncertainty density : ℚ≥0)
  → improvement · prob ≤ ekf/update improvement prob uncertainty density