Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.epsilon-greedy

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

AHoF epsilon-greedy exploration: the canonical explore/exploit rule for bandits and reinforcement learning. With probability epsilon take a random (exploring) action; otherwise take the greedy action argmax_a Q(a). Given a uniform draw u in [0,1), the agent explores exactly when u falls in the epsilon-band: explores? u epsilon = decide (u <= epsilon) exploit-action Q = argmax_a Q(a) over exact-rational epsilon and Q-values. Defined: the exploration test and the exploit action (via the argmax-index fold). Proved native and axiom-free, as worked instances: draw 1/10 with epsilon 1/4 explores, draw 1/2 with epsilon 1/4 exploits, the worked certificate 1/10 <= 1/4 (native nnrat/at-most), and exploit-action [5,7,4] = 1. That the exploit action is the argmax for every Q, and the rule's classical regret behaviour, are not proved here. The Q estimates, the RNG, and the random action are executable. 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 4 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.epsilon-greedy` prints this classification.

Depends onalgorithms.proofs.argmax-index

epsilon-greedy/explores? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

epsilon-greedy/exploit-action :
  (x₁ : List ℚ≥0)
  → ℕ

epsilon-greedy/draw-explores :
  → ce-is/elite? 1/10 1/4 = data/true

epsilon-greedy/exploration-in-band :
  → 1/10 ≤ 1/4

epsilon-greedy/draw-exploits :
  → ce-is/elite? 1/2 1/4 = data/false

epsilon-greedy/exploit-is-greedy :
  → epsilon-greedy/exploit-action [5, 7, 4] = 1