Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.ucb

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

AHoF O64 Upper Confidence Bound acquisition (Bayesian optimization / bandits): select the next query by optimistically combining the surrogate's predicted mean with an exploration bonus proportional to the predictive uncertainty: ucb mean weight uncertainty = mean + weight * uncertainty over exact nonnegative rationals. The predictive mean and uncertainty come from the surrogate (a Gaussian process, whose sigma involves a square root, is an executable / not-exact-rational concern) and the exploration weight is a supplied rational; what is proved here is the deterministic optimistic combination and its optimism guarantee: the acquisition is at least the predicted mean (ucb >= mean), so UCB never underexplores relative to pure exploitation. Worked instances reduce by reflexivity on the exact rational arithmetic. Requires nnrat/add, nnrat/multiply, nnrat/at-most, and the decidable nnrat order (all in the D63 checkpoint).

Depends onmath.rational.nnrat.add-upper

ucb/acquisition :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

ucb/acquisition-unfold :
  (mean weight uncertainty : ℚ≥0)
  → sac/soft-value mean weight uncertainty = mean + weight · uncertainty

ucb/acquisition-example :
  → sac/soft-value 5 1 2 = 7

ucb/at-least-mean :
  → 5 ≤ sac/soft-value 5 1 2

ucb/at-least-mean-universal :
  (mean weight uncertainty : ℚ≥0)
  → mean ≤ sac/soft-value mean weight uncertainty