Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.reinforce

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

AHoF D46 REINFORCE (likelihood-ratio policy gradient): the Monte-Carlo policy gradient estimator weights each sampled trajectory's score-function by its return. The estimate is the (mean of the) sum of return times score over the sampled trajectories: estimate r1 s1 r2 s2 = r1 * s1 + r2 * s2 over exact nonnegative rationals (two trajectories; the general estimator folds this over the batch and divides by the count). The trajectory returns and the score-function values grad log pi are problem/executable data supplied as rationals; the division by the batch size for the mean is executable. What is proved here is the deterministic return-weighted score combination and worked instances that reduce by reflexivity on the exact rational arithmetic. Requires nnrat/add and nnrat/multiply (in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 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.ahof.reinforce` prints this classification.

reinforce/estimate :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

reinforce/estimate-unfold :
  (r1 s1 r2 s2 : ℚ≥0)
  → qmdp/value r1 s1 r2 s2 = r1 · s1 + r2 · s2

reinforce/estimate-example :
  → qmdp/value 2 3 1 4 = 10

reinforce/zero-return-ignored :
  → qmdp/value 0 9 1 4 = 4