Autograd

Autograd widgets (tapes + gradients).

This module provides infoview panels for TorchLean’s eager-mode autograd tape:

• #tape_view t renders the tape nodes, showing parents, stored forward values, and a DOT snippet.
• #tape_grads_view t, outId runs reverse-mode from a scalar output (outId) and shows which node ids received gradients, plus small previews.

Main definitions

• tapeHtml: inspect a tape's nodes and edge structure.
• tapeGradsHtml: run scalar reverse-mode and show gradient coverage/results.
• tapeTraceHtml: step-by-step reverse-pass trace with per-parent VJP contributions.
• #tape_view, #tape_grads_view, #tape_trace_view: command frontends.

Implementation notes

• These widgets are intended for debugging and teaching, not proof scripts.
• DOT output is clipped for large tapes to keep infoview rendering responsive.
• Reverse traces use seed = 1 at the output node, matching loss.backward() intuition.

References

• Backpropagation and reverse-mode AD
• GraphViz DOT language
• ProofWidgets
• Lean community documentation style

Tags

autograd, reverse-mode, gradients, tape, widgets

def NN.Widgets.tapeHtml {α : Type} [ToString α] (t : Runtime.Autograd.Tape α) (maxDotChars : ℕ := 6000) : ProofWidgets.Html

Render a tape as an HTML panel (nodes + DOT).

def NN.Widgets.tapeGradsHtml {α : Type} [ToString α] [Add α] [One α] [DecidableEq Spec.Shape] (t : Runtime.Autograd.Tape α) (outId : ℕ) : ProofWidgets.Html

Render gradients from a scalar output id (like loss.backward()).

Reverse-Pass Trace

#tape_grads_view answers "which nodes received a gradient?".

When you need to understand why a gradient was produced (or why it is missing), it is useful to see the reverse traversal itself:

• the upstream cotangent at each node, and
• the per-parent contributions returned by the node’s local VJP rule.

This viewer runs reverse-mode and renders a step-by-step trace in reverse id order.

def NN.Widgets.tapeTraceHtml {α : Type} [ToString α] [Add α] [One α] [DecidableEq Spec.Shape] (t : Runtime.Autograd.Tape α) (outId : ℕ) : ProofWidgets.Html

Render a reverse-pass trace for a tape, starting from a scalar output node outId.

Commands

def NN.Widgets.tapeViewCmd : Lean.ParserDescr

def NN.Widgets.tapeGradsViewCmd : Lean.ParserDescr

def NN.Widgets.tapeTraceViewCmd : Lean.ParserDescr

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

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

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