Reference · Algorithm guarantees

rainbow.algorithms.proofs.sparse-sampling

Algorithm guaranteessrc/rainbow/algorithms/proofs/sparse_sampling.clj1 definitions, 4 theorems

AHoF D35 Sparse Sampling: the sample-complexity count of the sparse-sampling MDP planner (Kearns-Mansour-Ng). To estimate the value at a state to horizon H, the planner recurses, drawing C sampled next-states for each of the |A| actions at every node, so the sampled look-ahead tree has node-count |A| C H = (|A| * C) ^ H leaves -- exponential in the horizon but INDEPENDENT of the (possibly infinite) state-space size, which is the defining property that makes sparse sampling a tractable planner for large MDPs. Proved native and axiom-free using exact natural exponentiation (nat/power): the count is the branching factor |A|*C raised to the horizon. The value backup and the sampling itself are executable concerns; what is proved here is the sample-complexity count and worked instances. Requires nat, nat/multiply, and nat/power (nat/power added alongside). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 2 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.sparse-sampling` prints this classification.

Depends onmath.nat.power

sparse-sampling/node-count :
  (x₁ x₂ x₃ : ℕ)
  → ℕ

sparse-sampling/node-count-is-power :
  (actions samples horizon : ℕ)
  → sparse-sampling/node-count actions samples horizon = nat/power (nat/multiply actions samples) horizon

sparse-sampling/horizon-zero-single-node :
  (actions samples : ℕ)
  → sparse-sampling/node-count actions samples 0 = 1

sparse-sampling/node-count-example :
  → sparse-sampling/node-count 2 3 2 = 36

sparse-sampling/node-count-deep-example :
  → sparse-sampling/node-count 2 2 3 = 64