RL Boundary Rollout Viewer #

This widget is the “trust boundary debugger” for TorchLean RL.

It reads a Gymnasium-style rollout JSON file (typically produced by scripts/rl/export_gymnasium_rollout.py), validates every transition against a Lean-side Runtime.RL.Boundary.Contract, and renders a compact report:

number of transitions,
number of valid/invalid transitions,
the first few error messages (with indices).

This is intentionally separate from PPO-specific viewers: exported rollouts do not contain actor log-probabilities or value predictions, so PPO loss inspection belongs in the training examples.

source

def NN.Widgets.RL.Boundary.rolloutBoundaryReportHtml {obsShape : Spec.Shape} {nActions : ℕ} (path : System.FilePath) (c : Runtime.RL.Boundary.Contract obsShape nActions) (maxErrors : ℕ := 8) :

IO ProofWidgets.Html

Render a small HTML report for a rollout JSON file under a given contract.

Instances For

source

def NN.Widgets.RL.Boundary.rlBoundaryRolloutFileViewCmd :

Lean.ParserDescr

Instances For

source

def NN.Widgets.RL.Boundary.«command#rl_boundary_rollout_file_view_,_,_» :

Lean.ParserDescr

Instances For