Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.policy-gradient

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

AHoF D49 Gradient Ascent Update (policy gradient): the parameter update at the heart of policy-gradient reinforcement learning. Given a policy-gradient estimate, the parameters ascend along it by the learning rate: update theta rate gradient = theta + rate * gradient over the finite-vector parameter state. The gradient estimate (REINFORCE, reward-to-go, actor-critic, ...) and the learning-rate schedule are executable concerns; what is proved here is the deterministic ascent update and worked instances from a zero-initialized parameter, where a unit-rate step lands exactly on the gradient. Requires the shared finite-vector operations (vector/add, vector/scale) over signed rationals -- carried by the D63 checkpoint via the vector layer. 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.policy-gradient` prints this classification.

Depends onmath.finite.vector

policy-gradient/update :
  (x₁ : List ℚ) (x₂ : ℚ≥0) (x₃ : List ℚ)
  → List ℚ

policy-gradient/update-unfold :
  (theta : List ℚ) (rate : ℚ≥0) (gradient : List ℚ)
  → mads/poll theta rate gradient = vector/add theta (vector/scale rate gradient)

policy-gradient/update-unit-2d-example :
  → mads/poll [signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 3, signed/from-nnrat 2] = [signed/from-nnrat 3, signed/from-nnrat 2]

policy-gradient/update-unit-3d-example :
  → mads/poll [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6] = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]