PPO Training

Shared rollout, GAE, repeated-update, and evaluation schedule for fixed-horizon PPO. Callbacks own model execution and environment interaction; the loop owns RNG progression and update counts.

structure Runtime.RL.PPO.TrainConfig : Type

PPO update counts, evaluation cadence, and the initial rollout seed.

• updates : ℕ
• epochs : ℕ
• evaluationEvery : ℕ
• seed : ℕ

def Runtime.RL.PPO.train {α : Type} [TorchLean.Storage α] [Context α] {observation : Spec.Shape} {actions horizon : ℕ} [NeZero actions] [NeZero horizon] (gamma lam : α) (config : TrainConfig) (collect : ℕ → ℕ → ℕ → IO (Rollout α observation actions horizon × ℕ)) (updateBatch : TrainingBatch α observation actions horizon → IO Unit) (evaluate : ℕ → IO (Float × Bool)) (initialCurve : Training.Curve := { }) : IO Training.Curve

Train from fixed-horizon rollouts and append evaluation points to an existing curve.

collect receives the zero-based update index, seed, and random counter. evaluate receives the completed update count and returns a metric plus an early-stop flag. A stop occurs after recording that metric and before advancing the seed. evaluationEvery = 0 disables periodic evaluation.