MLP render half — the train-step text as a name-threaded render of proven graphs #
The linear renderModuleN rendered ONE shared cotangent subgraph (%dy). The MLP
train step is a DAG with several shared intermediates: the backward selects read the
forward pre-activations (%h0,%h1); the parameter gradients read the activations
(%a0,%a1) and the per-layer cotangents. So the renderer threads names: render each
forward piece from its proven SHlo graph (via pretty, capturing the fresh result
SSA), then emit the backward / param-grad / SGD ops referencing the captured names.
The forward pieces (denseF/reluF, lossCotGraph) are denotable and proven faithful
(denseF_faithful/reluF_faithful/lossCotGraph_isCEgrad); the backward + param-grad +
SGD ops are GPU-validated op templates, assembled around proof-rendered forward SSA. The
result is a valid MLP train-step module generated from the proven forward graphs — the
multi-intermediate generalization of the linear render half (cf.
planning/archive/verified_train_step.md, Crux B).
Structured MLP train-step renderer: forward pre-acts/activations/logits/cotangent
from proven SHlo graphs (name-threaded), then backward + param-grad + SGD ops
referencing the captured names. Produces @mlp_train_step.
Equations
- One or more equations did not get rendered due to their size.
Instances For
MLP train step rendered ENTIRELY from the verified AST. Like
mlpTrainStepStructured for the forward, but the backward chain
(dotOut/selectPos) and the six parameter SGD updates (weightSgd/biasSgd)
are now pretty of denoted SHlo nodes too — so every emitted line is
pretty(provenNode), and MlpFold proves each output's den = the
certified loss-descent step. Cotangents %dy/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.