Training

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

TorchLean’s core runtime and specs are purely mathematical; "training loops" are just repeated application of an update rule. In practice, the first thing you want when debugging training is:

• 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.

This module provides a pure log viewer (no JS): inline SVG sparklines + HTML tables.

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: quick classifier diagnostics.

Implementation notes

• Inline SVG sparklines are lightweight and render quickly in the infoview.
• We intentionally avoid custom JavaScript so widget files stay easy to import and review.
• For saved logs, we render an error panel instead of throwing hard failures; this keeps viewer files robust even when artifacts are missing.

References

• ProofWidgets
• scikit-learn confusion matrix terminology
• Lean community documentation style

Tags

training, logs, metrics, confusion-matrix, proofwidgets

Curves

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

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

Confusion Matrix

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.

Commands

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.

def NN.Widgets.«command#train_log_view_» : Lean.ParserDescr

TrainLog is pure data, but many executables write logs to disk.

This command reads a saved JSON log (written by Runtime.Training.TrainLog.writeJson) and renders it using the same viewer as #train_log_view.

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.

def NN.Widgets.«command#train_log_file_view_» : Lean.ParserDescr

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.

def NN.Widgets.«command#confusion_view_,_» : Lean.ParserDescr