Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.mcts

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

AHoF D36 Monte Carlo Tree Search: incrementally grow a search tree by selection, expansion, simulation, and backpropagation. The TREE POLICY selects the child maximizing the UCB score -- exploitation (mean value) plus an exploration bonus: ucb-score exploit explore = exploit + explore tree-policy-value children = list-maximum (map ucb-score children) over exact-rational UCB scores. Proved native and axiom-free: the UCB score is the sum of exploitation and exploration; the tree policy selects the maximum UCB (the proved list-maximum fold); a worked selection; and that the selected UCB dominates every child's UCB (child <= selected as native nnrat/at-most) -- so MCTS descends toward the most promising child. The exploration bonus (a sqrt/log term) and the rollout/backprop are executable; what is proved is the UCB tree-policy selection over supplied rational scores. Requires list-maximum/maximum, nnrat/add, 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.mcts` prints this classification.

Depends onalgorithms.proofs.list-maximum

mcts/ucb-score :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

mcts/tree-policy-value :
  (x₁ : List ℚ≥0)
  → ℚ≥0

mcts/ucb-score-example :
  → astar/f-value 3 2 = 5

mcts/selects-max-ucb :
  → greedy/value [5, 7, 4] = 7

mcts/dominates-first :
  → 5 ≤ 7

mcts/dominates-third :
  → 4 ≤ 7