Training #

Training/testing loop visualizations (logs, curves, and small reports).

When debugging a training loop, it helps to inspect the values recorded after each update:

a loss curve (did it decrease? did it blow up?),
a few scalar metrics (accuracy, learning rate, gradient norm),
a compact “last N steps” table.

The log viewer uses inline SVG sparklines and HTML tables, with no custom JavaScript.

Main command:

#train_log_view log renders a TrainLog.

Optional testing command:

#confusion_view labels, cm renders a confusion matrix for classification eval.

Main definitions #

trainLogHtml: render scalar metric series and recent-step tables.
confusionHtml: render confusion matrix + per-class precision/recall.
#train_log_view / #train_log_file_view: in-memory and file-backed entry points.
#confusion_view: classifier diagnostics for a label/confusion-matrix pair.

Curves #

source

def NN.Widgets.trainLogHtml (log : Runtime.Training.TrainLog) (maxRows : ℕ := 20) :

ProofWidgets.Html

Render a TrainLog (metric series + recent steps) as an infoview HTML panel.

Instances For

Confusion Matrix #

source

def NN.Widgets.confusionHtml (labels : Array String) (cm : Runtime.Training.ConfusionMatrix) (maxLabels : ℕ := 40) :

ProofWidgets.Html

Render a ConfusionMatrix (with optional label clipping) as an infoview HTML panel.

Instances For

Commands #

source

def NN.Widgets.trainLogViewCmd :

Lean.ParserDescr

Render a Runtime.Training.TrainLog value directly in the infoview.

This is the in-memory (non-IO) variant. For executables that write JSON logs to disk, see #train_log_file_view.

Instances For

source

def NN.Widgets.«command#train_log_view_» :

Lean.ParserDescr

Instances For

source

def NN.Widgets.trainLogFileViewCmd :

Lean.ParserDescr

Read a saved Runtime.Training.TrainLog JSON file and render it in the infoview.

The expected JSON schema is the one produced by Runtime.Training.TrainLog.writeJson and TorchLean's executable training examples (for example PPO examples under NN/Examples/Models/*).

When the file is missing or malformed, this command renders an error panel instead of failing the build, so widget-view files stay safe to import.

Instances For

source

def NN.Widgets.«command#train_log_file_view_» :

Lean.ParserDescr

Instances For

source

def NN.Widgets.confusionViewCmd :

Lean.ParserDescr

Render a confusion matrix report in the infoview.

This is a small viewer for Runtime.Training.ConfusionMatrix plus an aligned array of class labels.

Instances For