Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.thompson

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

AHoF Thompson Sampling (posterior sampling) for multi-armed bandits: instead of an explicit exploration bonus, draw one sample from each arm's posterior over its mean reward and pull the arm with the largest sample. Arms with uncertain posteriors are explored automatically (their samples vary widely), while the best-known arm is exploited most often. Given the per-arm posterior samples, the selected arm is the argmax: thompson-select samples = argmax_a samples(a) over exact-rational samples (returning the selected arm index). Proved native and axiom-free: the selection is exactly the proved argmax-index fold; a worked selection; and the certificate that the selected arm's sample is at least each other arm's sample (native nnrat/at-most), so posterior sampling pulls the currently-most-promising arm. The posterior model and the sampler are executable; what is proved is the argmax arm selection over the samples. Requires argmax-index/argmax-index, nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and 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.thompson` prints this classification.

Depends onalgorithms.proofs.argmax-index

thompson/select :
  (x₁ : List ℚ≥0)
  → ℕ

thompson/selects-largest-sample :
  → knn/predict [5, 8, 4] = 1

thompson/selected-dominates-arm-zero :
  → 5 ≤ 8

thompson/selected-dominates-arm-two :
  → 4 ≤ 8