Reinforcement Learning

Mathematical definitions and executable algorithms exposed under TorchLean.rl.

References (background and terminology):

• Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed.): http://incompleteideas.net/book/the-book-2nd.html
• Puterman, Markov Decision Processes (finite discounted MDPs): https://doi.org/10.1002/9780470316887
• Gymnasium API reference (reset/step, terminated vs truncated): https://gymnasium.farama.org/

The measure-theoretic MDP from NN.Spec.RL.MarkovMDP: a general state space whose transitions are probability kernels, with the expected next value as a Bochner integral.

Both state types expose init and update. A value state uses sample averages:

let state : rl.bandits.ValueState Float 3 := rl.bandits.ValueState.init
let state := state.update action reward
let action := state.greedy?

A preference state instead learns a softmax policy: state.update action reward stepSize, with baseline := false to omit the running-average baseline. Read its probabilities with state.policy. Exploration draws for epsilonGreedy? are supplied by the caller.

Compute a target, then move one table entry toward it with update:

let target := rl.tabular.qLearningTarget q nextState reward discount
let q := rl.tabular.update q (state, action, PUnit.unit) target stepSize

State-value tables use (state, PUnit.unit) instead. The coordinate is checked against the tensor's shape by Lean; update does not convert it through a runtime index list.

Keep target selection separate from the scalar error function:

let target := rl.value.dqnTarget reward discount done nextValues
let loss := rl.value.loss values action target
let robustLoss := rl.value.loss values action target
  (error := fun prediction target => rl.core.huberLoss prediction target threshold)

For a temporal-difference residual, subtract Tensor.getScalar values action from the target. DDPG's critic uses rl.core.discountedBackup; its actor minimizes the negative critic value.

Differentiable DQN losses over TorchLean backend references.

These helpers build scalar semi-gradient losses for eager or typed graph autograd. Targets and action indicators are detached; the selected online Q values receive the loss gradient.

huber prediction target detaches Bellman targets before reducing the elementwise loss. loss qValues actions target also detaches the one-hot actions and averages over transitions.

probabilities applies softmax. probability and logProbability guard a selected probability with epsilon; logSoftmax instead selects an unclamped log-softmax entry. entropy uses guarded weights without renormalizing, whereas kl clamps and normalizes both probability vectors.

sample seed counter values consumes probability weights. Set logits := true to apply softmax first. Both modes return the next counter and chosen action; supplied weights are not validated. For TRPO's unpenalized surrogate, use ratio * advantage; the trust-region constraint is separate.

Differentiable policy-gradient losses over TorchLean backend references.

The pure exports above are algebra over concrete spec tensors. These helpers are the training-time counterpart: they build scalar losses from backend refs, so the same formulas can run through eager or typed graph autograd.

objective ratio advantage clipEps is the clipped surrogate to maximize. When starting from policy logits and a cached old log-probability, use objectiveFromLogits; it applies the guarded selected probability from policy.logProbability. loss negates that objective and adds value regression and entropy terms. These pure functions do not construct a differentiation tape.

objective records the per-sample clipped surrogate from logits and one-hot actions; loss records the mean policy, value and entropy loss. Both use policy.autograd.logProbability's finite log-softmax guard. create actor critic bundles the two models into an objective definition for a PPO batch. The pure ppo.loss above instead operates on concrete tensors for one action.

totalReward evaluates one greedy-policy episode without recording its history. meanReward averages these episode totals, not individual step rewards. path instead records the checked session states, including the initial state; those states can contain nonnumeric environment data.