MLP render half — the train-step text as pretty of proven graphs #
mlpTrainStepText renders the MLP train step (verified_mlir/mlp_train_step.mlir).
Every line that feeds a returned parameter is pretty of a denoted SHlo node: the forward
(denseF/reluF), the loss cotangent (sub (softmaxDiv (expe …)) onehot), the backward chain
(dotOut/selectPos) and the six SGD updates (weightSgd/biasSgd). The appended report-only
%loss block is hand-written and feeds nothing; the signature is hand-written too. The step is a
DAG with shared intermediates — the backward selects read the forward pre-activations, the
parameter gradients read the activations and per-layer cotangents — so the renderer threads
names: each piece is rendered once via pretty, capturing its fresh result SSA, and later pieces
reference the captured names. MlpFold proves the output weight's node denotes
W₂ − lr·∂CE/∂W₂ (mlp_W2_tied_totalloss) and each of the other five denotes
θ − lr·(certified layer Jacobian · the rendered chain cotangent)
(mlp_train_step_tied_certified). The artifact's #eval writer is MlpArtifacts.lean.
MLP train step rendered from the verified AST. The forward, the backward chain
(dotOut/selectPos) and the six parameter SGD updates (weightSgd/biasSgd) are all
pretty of denoted SHlo nodes, so every line that feeds a returned parameter is pretty
of a denoted node; the appended report-only %loss block is hand-written and feeds nothing.
What MlpFold proves of the six update nodes: see the module docstring. The cotangents
(ndy/nc1/nc0) are rendered once and shared (operand leaves); operand/lr/weight
VALUES are skel-erased, so these placeholders print identically to the live graphs the
den theorems use.
Equations
- One or more equations did not get rendered due to their size.