PPO Actor-Critic Models

Reusable actor/critic MLP constructors for PPO examples.

These helpers cover the neural-network shape. Environment collection, trust-boundary checks, advantage computation, and optimizer loops stay in the examples/runtime modules.

structure TorchLean.nn.models.PPO.Config : Type

Configuration for a simple PPO actor/critic pair over vector observations.

• observationWidth : ℕ

  Number of features in each environment observation.

• hiddenWidth : ℕ

  Width of the actor and critic hidden layers.

• actionCount : ℕ

  Number of discrete actions represented by the actor logits.

@[instance_reducible]

instance TorchLean.nn.models.PPO.instReprConfig : Repr Config

def TorchLean.nn.models.PPO.instReprConfig.repr : Config → ℕ → Std.Format

def TorchLean.nn.models.PPO.Internal.validateNetwork (kind : String) (config : Config) : Except String Unit

Validate dimensions used by both PPO networks.

def TorchLean.nn.models.PPO.Internal.validateActor (config : Config) : Except String Unit

Validate the actor, including its action-logit width.

def TorchLean.nn.models.PPO.Config.validate (config : Config) : Except String Unit

Validate the complete actor-critic configuration.

@[reducible, inline]

abbrev TorchLean.nn.models.PPO.Config.inputShape (config : Config) (batchShape : Shape := []) : Shape

Observation tensor shape with an arbitrary batch shape.

@[reducible, inline]

abbrev TorchLean.nn.models.PPO.Config.actorOutputShape (config : Config) (batchShape : Shape := []) : Shape

Actor-logit tensor shape with the same batch shape as the observations.

@[reducible, inline]

abbrev TorchLean.nn.models.PPO.Config.criticOutputShape (_config : Config) (batchShape : Shape := []) : Shape

Critic-value tensor shape with the same batch shape as the observations.

def TorchLean.nn.models.PPO.actor (config : Config) (batchShape : Shape := []) : Builder (Sequential (config.inputShape batchShape) (config.actorOutputShape batchShape))

Actor MLP mapping observations to action logits.

def TorchLean.nn.models.PPO.critic (config : Config) (batchShape : Shape := []) : Builder (Sequential (config.inputShape batchShape) (config.criticOutputShape batchShape))

Critic MLP mapping observations to a scalar value estimate.