The chapter-net graphs and their printers (chapters 1–4) #
The whole-net forward (and, for the MLP and the MNIST CNN, backward) SHlo graphs of the
book's small nets, and the renderModule printers that write the committed
verified_mlir/ forwards from them (ChapterArtifacts' #evals):
| net | graph | printer |
|---|---|---|
| linear (ch 1) | fwdGraph, backGraph, lossCotGraph (in StableHLO) | linearFwdModuleV, linearBackModuleV, linearTrainStepModuleV |
| MLP (ch 2) | mlpFwdGraph, mlpBackGraph | mlpFwdModuleV |
| MNIST CNN (ch 3) | cnnFwdGraph, cnnBackGraph | cnnFwdModuleV |
| CIFAR CNN (ch 4) | cifarFwdGraph, cifar8FwdGraph, cifar8BnFwdGraph | cifarFwdModuleV, cifar8FwdModuleV, cifar8BnFwdModuleV |
The MLP graphs' faithfulness theorems are here; that the chapter 3–4 graphs denote their nets is
ChapterGraphTies, since the IR imports no net. The op vocabulary, den, pretty
and renderModule are StableHLO / StableHLO.Pretty, which the batched ImageNet nets share,
so an edit to a chapter net stays out of their rebuild.
Whole-MLP forward graph dense W₂ ∘ relu ∘ dense W₁ ∘ relu ∘ dense W₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whole-MLP backward (input-VJP) graph: dotOut W₀ ∘ select(p₀) ∘ dotOut W₁ ∘ select(p₁) ∘ dotOut W₂, pᵢ the ReLU pre-activations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
MLP backward faithfulness (smooth point). The backward graph denotes
the proven mlpHasVJPAt.backward — the per-op dot_general/select
ops assembled into the proven whole-network VJP (cf. IR.mlp_whole_bridge).
Whole MNIST-CNN forward graph:
dense ∘ relu ∘ dense ∘ relu ∘ dense ∘ maxPool ∘ relu ∘ conv ∘ relu ∘ conv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whole CIFAR-CNN forward graph (Chapter 4): two conv→relu→conv→relu→maxPool
stages (channels ic→c1→c1, then c1→c2→c2) then dense→relu→dense→relu→dense.
The Chapter-4 peer of cnnFwdGraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whole deeper (8-conv) CIFAR-CNN forward graph: four conv→relu→conv→relu→maxPool
stages (channels ic→c1→c1, c1→c2→c2, c2→c3→c3, c3→c4→c4) then
dense→relu→dense→relu→dense. The 4-stage peer of cifarFwdGraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whole deeper (8-conv) BN-CIFAR forward graph: each of the eight convs is followed
by a per-channel bnPerChannelF before its ReLU. epsStr is the shared ε literal; the
eight BN layers carry per-channel γ/β inputs %g{i}/%bt{i}. The BN peer of
cifar8FwdGraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whole MNIST-CNN backward (input-VJP) graph, reversing cnnFwdGraph:
convBack W₁ ∘ select(a₁) ∘ convBack W₂ ∘ select(a₂) ∘ maxPoolBack ∘ dotOut W₃ ∘ select(a₃) ∘ dotOut W₄ ∘ select(a₄) ∘ dotOut W₅, with aᵢ the
ReLU pre-activations and the conv/maxpool saved inputs threaded by name.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The full @linear_train_step rendered from the verified AST: forward +
softmax-CE cotangent come from pretty (lossCotGraph …) (the %onehot
operand value is pretty-irrelevant, so any placeholder renders the same
text — at runtime %onehot is a graph input); the weight grad
(dot_general over the batch axis), bias grad (reduce), and the SGD
multiply/subtract updates are appended. Returns the two updated params.
The verified-AST peer of IRPrint.linearTrainStepModule.
Instances For
@mlp_fwd rendered from the verified forward AST mlpFwdGraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@cnn_fwd rendered from the verified CNN forward AST cnnFwdGraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@cifar_fwd rendered from the verified CIFAR forward AST cifarFwdGraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@cifar8_fwd rendered from the verified 8-conv CIFAR forward AST cifar8FwdGraph
(cifar8FwdGraph_faithful proves it denotes cifarCnn8Forward). The 4-stage peer of
cifarFwdModuleV — the committed verified_mlir/cifar8_fwd.mlir is
renderModule(provenGraph).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@cifar8_bn_fwd rendered from the verified 8-conv per-channel-BN CIFAR forward AST
cifar8BnFwdGraph (cifar8BnFwdGraph_faithful proves it denotes cifarCnnBn8Forward).
The BN peer of cifar8FwdModuleV.
Equations
- One or more equations did not get rendered due to their size.