Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.sac

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

AHoF D45 Soft Actor-Critic: an off-policy actor-critic that optimizes a MAXIMUM-ENTROPY objective, augmenting the reward with an entropy bonus so the policy stays as stochastic as possible while succeeding -- improving exploration and robustness. The soft (entropy-regularized) value of a state is soft-value reward alpha entropy = reward + alpha * entropy over exact-rational reward, temperature alpha, and policy entropy. Proved native and axiom-free: the soft-value combination; a worked soft value; and that at temperature 0 (alpha = 0) the soft value collapses to the plain reward (recovering standard RL) -- reducing by reflexivity. The critic, the reward, and the entropy estimate are executable; what is proved is the entropy-regularized soft-value combination. Requires nnrat/add, nnrat/multiply (both in the D63 checkpoint). Scope (measured by the kernel): this module has 2 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.sac` prints this classification.

sac/soft-value :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

sac/soft-value-example :
  → sac/soft-value 1 1/2 1 = 3/2

sac/collapses-to-reward :
  → sac/soft-value 2 0 5 = 2