Inspection Workflow🔗

For an unexpected output, the graph and its evaluation trace expose intermediate values. For an inconclusive verification result, node-by-node interval widths help locate precision loss. A stalled training run may instead call for comparing the tape, accumulated gradients, and metric log.

The same named object can be evaluated, viewed, and checked:

1. Keep the value that matters as a named Lean definition or as an artifact at an explicit path.

2. Run the evaluator or checker whose semantics the eventual claim uses.

3. Put the corresponding widget beside that value and find the first surprising node, field, or step.

4. Change the definition or producer, elaborate again, and let the checker close the argument instead of trusting the picture.

Read-only views such as #tensor_view format a value without changing it. Trace views execute a specific Lean computation: #ir_exec_trace_view steps through NN.IR.Semantics, while #tape_trace_view follows the autograd engine's reverse pass. The interpretation is therefore explicit. A theorem about that same interpretation is still a separate proof.

The available views expose different parts of these objects:

Choose the view by the question being asked. If a tensor contains the wrong entries, changing a plot's scale cannot explain where those entries came from; follow its parents in the graph or tape. If the entries are plausible but a bound is wide, inspect the verifier state instead of rerunning ordinary evaluation at one input. The two computations answer different questions: one produces a value at a chosen point, while the other represents a range of possible values. Keeping the named input object beside its view makes that distinction concrete.

Application Workflows🔗

Some values live only while a file elaborates; others are written by a command and inspected later. A graph or tape definition can sit immediately above its view. A GPT or PPO run instead writes a named artifact, which a later Lean file reads:

-- Inspect the saved artifacts at the same paths used by
-- their producer commands.
#train_log_file_view "data/examples/cnn_trainlog.json"
#train_log_file_view "data/examples/gpt2_trainlog.json"
#rl_boundary_rollout_file_view "data/rl/cartpole_rollout.json", contract, 12
#pytorch_translate_file "NN/Examples/Interop/PyTorch/MLP/train_mlp.py"

Keep the producer command beside a file-backed view in a comment or experiment note. The renderer can tell you what the file says, but it cannot recover where the file came from. When the artifact has a checker, check it first and then inspect the accepted object.

Tensor Viewer🔗

I encode the three indices of rankThreeGrid in the hundreds, tens, and units places so we can recognize an axis change in the entries themselves. The floating-point vectors address a separate inspection problem: decimal printing can hide differences in scalar representation.

Tensor.generate passes the coordinate list to its callback. For shape [2, 3, 4], the three lookups give the indices that rankThreeGrid encodes; sampleMatrix uses the first two coordinates of its rank-two shape.

Those definitions are the widget inputs. In an editor, each #tensor_view line renders the value beside the cursor:

The commands above are elaborated when this page is built. Interactive panels require the Infoview; the same tensor can also be inspected through its printed entries:

[[[0, 1, 2, 3], [10, 11, 12, 13], [20, 21, 22, 23]], [[100, 101, 102, 103], [110, 111, 112, 113], [120, 121, 122, 123]]]

Entry 112 sits at (1,1,2). Moving the first axis would move the hundreds digit's variation to a different nesting level, making the layout change visible across the whole grid.

floatTensor and ieeeTensor use different scalar types. Comparing their decimal renderings does not reveal every difference introduced by binary32 conversion:

binary64 1.000000  binary32 1.000000  bits 0x3f800000
binary64 0.100000  binary32 0.100000  bits 0x3dcccccd
binary64 0.333333  binary32 0.333333  bits 0x3eaaaaab

Each row uses the same decimal rendering for its binary64 and binary32 values; the final column shows the binary32 bits. One is exact in both formats. One tenth is not a binary fraction, so neither format holds it exactly, and the two formats do not hold the same approximation of it (Goldberg, 1991). This comparison explicitly converts each binary32 result to the native decimal display. The configured tensor's own printer can show its exact dyadic value; #float32_view further down exposes the encoding and exceptional-value fields.

The coordinate-coded grid is useful because a transposition can preserve both the number of entries and their minimum and maximum. A summary might therefore look unchanged while the model reads the wrong axis as channels or time. Here the hundreds digit identifies the first coordinate, the tens digit the second, and the units digit the third. Reading the nesting and the digits together checks their correspondence. The precision example tests another kind of lost information: decimal formatting can preserve the visual pattern while hiding different stored numbers.

IR Graph Viewer🔗

For the next graph, we can inspect three things separately:

1. Structure: which nodes, parents, and shapes are present?

2. Invariants: do declared node shapes match what the ops infer from parent shapes?

3. Semantics: when the graph is evaluated, which node fails first and what are the intermediate values?

The trace command calls the internal IR evaluator directly, so its input uses Spec.SomeTensor to carry a runtime shape. Model code continues to accept and return Tensor α shape.

parents := #[0, 1] stores the input and constant node ids in an Array Nat. The constant's value lives in samplePayload; the graph records its shape and the operation that reads it.

The four views then attach to those definitions:

The graph view shows node 2 depending on the input and constant. The shape view compares all three declared length-two shapes with inference. The trace view repeatedly calls Graph.evalAt, retaining the values computed before a failure. The following Graph.denoteAll call evaluates the complete graph through the same node semantics and prints the successful result in node order:

node 0: [0.600000, -0.200000]
node 1: [0.250000, 0.250000]
node 2: [0.850000, 0.050000]

Node 2 adds [0.25, 0.25] to [0.60, -0.20], producing [0.85, 0.05] to the precision shown. If that result were unexpected, the two parent rows would distinguish incorrect inputs from an incorrect addition. Shape checking addresses failures that prevent this evaluation from succeeding.

The addition/subtraction comparison is a display example, not a justified graph rewrite. sampleGraphSub changes the mathematical operation, so seeing both graphs side by side helps locate the change but cannot establish that they compute the same result. For an optimizer rewrite, the corresponding correctness statement must relate the source and destination semantics under its hypotheses. A structural diff remains useful even then: it lets the reader check which nodes and payloads that statement is supposed to cover.

sampleGraph inferred #[[2], [2], [2]]
miscountedGraph rejected: IR graph: node 2: outShape mismatch: inferred=[2], declared=[3] (Node(id=2, kind=add, parents=#[0, 1], outShape=[3]))
crossedGraph rejected: add: shape mismatch: [2] vs [3]

Float32 Bit Layout Viewer🔗

We can print the same sign, exponent, and fraction fields that the viewer displays:

one32 : sign=0 exp=127 frac=0 nan=false
qnan32: sign=0 exp=255 frac=4194304 nan=true

one32 is sign 0, biased exponent 127, zero fraction, which is the encoding of 1.0. The quiet NaN has the all-ones exponent field 255 and a nonzero fraction, so its classification stays visible even though it has no real value to print. That distinction matters in practice: a NaN that reaches a gradient can contaminate later arithmetic. The bit view exposes that value directly; a loss curve alone may hide it, especially when later branches mask the NaN.

The round views answer a different question. When a binary64 Float crosses the scalar boundary, which binary32 pattern is chosen?

rounded value = 0.100000
exact value = some { negative := false, significand := 13421773, exponent := -27 }

The rounded float is 13421773 \cdot 2^{-27}. With the significand and exponent returned by toDyadic?, we can state its exact value in a proof even though the display rounds it to 0.100000. Flocq's treatment of IEEE-754 in Rocq also reasons from exact representations of floating-point values (Boldo and Melquiond, 2011) (Boldo et al., 2015).

The exact dyadic output also gives a way to reason about conversion error. Once the finite value is written as an integer times a power of two, its distance from the intended rational can be computed without relying on the displayed decimal digits. That is why the bit and round views are useful beside numerical proofs: they expose the data on which an exact statement can be based. For a NaN or infinity, that finite-value interpretation is unavailable, so classification must come before treating a bit pattern as a real number.

Verification (IBP/CROWN State)🔗

TorchLean's verification code includes executable bound propagation engines: IBP boxes and CROWN affine forms. When debugging a verifier, inspect which nodes have bounds and whether shapes and flattened dimensions match the intended layout.

The graph is the same sampleGraph from above, so a trace value and a bound refer to the same node id. Here samplePropState is a manually constructed display fixture, not the output of a verifier or a checked certificate. Adding the exact constant 0.25 shifts [-1,1] to [-0.75,1.25] without changing the width:

input : [[-1.000000, -1.000000], [1.000000, 1.000000]] width [2.000000, 2.000000]
const : [[0.250000, 0.250000], [0.250000, 0.250000]] width [0.000000, 0.000000]
output: [[-0.750000, -0.750000], [1.250000, 1.250000]] width [2.000000, 2.000000]

The input and output both have width two; the constant has width zero. These representable endpoints make the translation exact. Over real arithmetic, adding a point preserves interval width, while directed floating-point arithmetic may widen endpoints through rounding. In a larger graph, inspecting the first unexpected increase helps distinguish rounding from precision lost by a bound-propagation rule (Zhang et al., 2018).

The state records use flattened boxes of dimension two even though the graph keeps tensor shapes separately. Matching the node id, shape, and flattened dimension prevents a convincing plot from being attached to the wrong operation. Missing bounds also matter: a blank interval entry means no box was supplied for that node, whereas a zero-width box represents an exact point. The constant's zero width here is therefore useful information. It explains why translating the input box introduces no uncertainty in this fixture.

x      : [[-1.000000, -1.000000], [1.000000, 1.000000]] width [2.000000, 2.000000]
x - x  : [[-2.000000, -2.000000], [2.000000, 2.000000]] width [4.000000, 4.000000]
relu x : [[0.000000, 0.000000], [1.000000, 1.000000]] width [1.000000, 1.000000]

Autograd (Tape + Gradients)🔗

TorchLean's eager autograd engine records a computation graph into a Tape and can run reverse-mode to accumulate gradients. The widget below shows the recorded tape and the gradients produced by scalar backprop, corresponding to a call to loss.backward() in PyTorch (Paszke et al., 2019).

The recorded scalar is ab+b at a=2 and b=3, so \partial/\partial a = b = 3 and \partial/\partial b = a+1 = 3. Both derivatives are three by coincidence at this point, which is convenient for reading the output and worth remembering when changing the numbers. Running the same reverse pass the widget runs:

a: value 2.000000 grad 3.000000
b: value 3.000000 grad 3.000000
mul: value 6.000000 grad 1.000000
add: value 9.000000 grad 1.000000

The output is nine and both leaf gradients are three, matching the derivatives above. Node b feeds both multiplication and addition, so its gradient accumulates two contributions: a=2 from multiplication and 1 from addition. Dropping the addition's contribution would give the plausible but incorrect gradient 2.0. The reverse traversal combines these contributions using SomeTensor.add, rather than mutating a leaf's .grad field as PyTorch does (Paszke et al., 2019).

Tape.backwardScalar returns a map from node ids to gradients and an Except error if a local VJP fails, for example because of a shape mismatch. The derivatives of ab+b give a reference for inspecting this reverse trace: a missing or incorrect gradient can be traced to the step where a contribution was omitted or computed incorrectly.

The two internal gradients explain the reverse traversal as well. The final addition is seeded with one because it is the selected scalar output. Its multiplication parent receives one, and that parent sends b to a and a to b. The direct addition edge supplies the extra one to b. Looking only at the final leaf numbers would miss this route through the graph. The trace is most useful when a shared parameter has several consumers, because each consumer's contribution must arrive before the accumulated gradient is interpreted.

a: value 2.000000 grad 3.000000
b: value 3.000000 grad 3.000000
mul: value 6.000000 grad 1.000000
add: value 9.000000 grad 1.000000
c: value 5.000000 grad none

Training Dashboards🔗

Training logs and confusion matrices are also Lean values. Runtime.Training.TrainLog records steps, metric series, and notes; Runtime.Training.ConfusionMatrix stores class counts. The widget layer renders these records whether they came from a Lean training loop or an external experiment.

The following literals are display fixtures. Their values and notes are supplied directly here; no training run produced them:

The two viewer commands then take those names. They render in the Infoview, so this page can only show the invocation:

-- Render the named metric log and the separately supplied
-- confusion matrix.
#train_log_view sampleTrainLog
#confusion_view sampleLabels, sampleCM

Ordinary array operations can summarize these records without rendering a widget:

steps: 5
loss: 1.200000 -> 0.330000
val_acc: 0.300000 -> 0.790000
lr: 0.050000 -> 0.010000
correct 21 of 26

The confusion matrix contains 21 correct predictions among 26, giving 21/26 \approx 0.808. That differs from the fixture log's final val_acc of 0.79: the two literals were constructed independently. When both artifacts describe the same evaluation in a real run, this comparison can detect inconsistent metrics or mismatched files.

For logs produced by a training command, see:

• the CSV loader training example,

• the NPY loader training example,

• the CNN and ViT model commands,

• and the callback/reporting helpers exposed through Trainer reports.

The metric summary preserves units that a dashboard can make easy to overlook. Loss, accuracy, and learning rate occupy separate series even though they share step coordinates. A downward learning-rate curve is a configuration change, while a downward loss curve is an observation about the supplied metric values. Neither explains the other by itself. The confusion matrix adds a different view of the same classification task: off-diagonal entries identify which labels are confused, information that one accuracy number discards. Its class labels must agree with the matrix dimensions for that interpretation to make sense.

GPT And Text-Model Logs🔗

Text models write ordinary TrainLog artifacts. The shared viewer preserves multiline notes, including prompts and generated samples:

-- Read the text model log written by its training or
-- generation command.
#train_log_file_view "data/examples/gpt2_trainlog.json"

Run training or generation through the model's CLI, then inspect the saved log. The widget only reads and renders the artifact.

RL Boundary And Policy Views🔗

A reward curve leaves out the transitions and actions that produced it. The RL views expose:

• the checked transition boundary for Gymnasium rollouts,

• GridWorld policies and paths,

• PPO rollout curves derived from reward/value/advantage data.

The main entry files are:

• GridWorld widget source

• PPO widget source

• RL boundary widget source

These views expose the transitions received by the learner and the policy/path artifacts written by a command. MDP validity and boundary soundness are separate statements in the proof layer.

A rollout boundary report counts checked transitions and records failures with their indices. That index lets a reader inspect the offending observation, action, or reward in the original artifact. It does not supply the old policy probabilities or value estimates needed to reconstruct a PPO objective; those belong to a different record. An empty rollout deserves special attention: there are no rejected transitions, but there are also no accepted observations of the boundary. The widget reports that no checks ran rather than presenting emptiness as evidence about an episode.

PyTorch Translator Widget🔗

The PyTorch translator widget proposes a constructor sketch in the editor:

-- Ask the editor assistant for a constructor sketch of this
-- Python source.
#pytorch_translate_file "NN/Examples/Interop/PyTorch/MLP/train_mlp.py"

It helps readers see how a simple torch.nn snippet maps onto TorchLean constructors. Checked interop claims should cite the explicit PyTorch roundtrip/export examples and the artifact bridge, not the heuristic widget alone. The widget accepts scalar natural dimensions in recognized constructor arguments; symbolic sizes, tuples, duplicate keywords, and extra options are reported as unsupported. Convolution rows provide metadata and shape-boundary notes, not an executable CNN.

Widget Examples🔗

Open NN/Examples/DeepDives/Widgets.lean in VS Code with the Lean extension enabled. Put the cursor on each widget command and open the Infoview. The file is deliberately small enough to elaborate interactively.

Work through four changes:

1. Change one entry of a tensor and confirm that #tensor_view and #tensor_stats_view update from the same Lean value.

2. Give an IR node the wrong declared output shape. #shape_infer_view should identify the first disagreement; restore the shape before continuing.

3. Replace sampleGraph by sampleGraphSub in the rewrite view and inspect the changed operation tag rather than comparing raw record syntax.

4. Compare (1 : ExecFloat.Binary 8 23) with a quiet NaN. The bit viewer should expose the exponent, fraction, and classification that ordinary decimal printing hides.

The file can also be elaborated from a terminal:

# Elaborate the widget examples; interactive panels are
# displayed by the editor.
lake env lean NN/Examples/DeepDives/Widgets.lean

Terminal elaboration checks the commands and definitions, while the VS Code Infoview provides the interactive rendered panels. If a widget fails to elaborate, first distinguish a malformed Lean object from a rendering problem: replace the widget command by #check on the same object, then reintroduce the view after its type is correct.

View Data Sources🔗

Keep the definition or producer path near its view. A graph panel can then be traced to the graph record, a bound to its verifier state, and a training curve to the parsed file. This makes a surprising display traceable to the data that produced it.