DQN Replay Mini-Example

This example runs the runtime pieces used by an off-policy DQN-style update:

1. construct typed transitions;
2. insert them into a bounded replay buffer;
3. sample a minibatch;
4. evaluate a DQN minibatch loss from caller-provided online/target Q-functions.

The Q-functions are hand-written closures rather than neural networks, so the example stays focused on replay buffers and minibatch losses. A full trainable DQN run can later swap those closures for compiled TorchLean models and an optimizer step.

Run from the repo root through the maintained example runner:

lake exe torchlean dqn_replay

References:

• Mnih et al., "Human-level control through deep reinforcement learning" (2015): https://doi.org/10.1038/nature14236
• Lin, "Self-Improving Reactive Agents Based on Reinforcement Learning, Planning and Teaching" (1992), early experience replay.

def NN.Examples.Models.RL.DQNReplay.exeName : String

@[reducible, inline]

abbrev NN.Examples.Models.RL.DQNReplay.ObsShape : Shape

@[reducible, inline]

abbrev NN.Examples.Models.RL.DQNReplay.NActions : ℕ

def NN.Examples.Models.RL.DQNReplay.obsA : TorchLean.Tensor.T Float ObsShape

A compact two-feature observation.

def NN.Examples.Models.RL.DQNReplay.obsB : TorchLean.Tensor.T Float ObsShape

A second observation used as the next state.

def NN.Examples.Models.RL.DQNReplay.transitionA : Runtime.RL.Core.Transition Float ObsShape NActions

One typed transition inserted into the replay buffer.

def NN.Examples.Models.RL.DQNReplay.transitionB : Runtime.RL.Core.Transition Float ObsShape NActions

A second transition, marked terminal, so the sample contains both bootstrap modes.

def NN.Examples.Models.RL.DQNReplay.onlineQ (obs : TorchLean.Tensor.T Float ObsShape) : TorchLean.Tensor.T Float (Spec.Shape.dim NActions Spec.Shape.scalar)

Compact online Q-function used by the example.

def NN.Examples.Models.RL.DQNReplay.targetQ (obs : TorchLean.Tensor.T Float ObsShape) : TorchLean.Tensor.T Float (Spec.Shape.dim NActions Spec.Shape.scalar)

Compact target Q-function used by the example.

def NN.Examples.Models.RL.DQNReplay.run : IO Unit

Build a replay buffer, sample a minibatch, and compute DQN losses.

def NN.Examples.Models.RL.DQNReplay.usage : String

Command-line help for the replay-buffer mini-example.

def NN.Examples.Models.RL.DQNReplay.main (args : List String) : IO UInt32

Runner entrypoint used by lake exe torchlean dqn_replay.