NF End-To-End GraphData Bridge #
End-to-end runtime→spec bridge for NF graphs executed as GraphData.
NN.Proofs.RuntimeApprox.NF provides per-op NF approximation lemmas and composes them over
RevGraph via RevGraph.eval_approx and NFBackend.backprop_approx.
This file links those results to the executable SSA/DAG form used by typed graph execution:
Proofs.Autograd.Algebra.GraphData. A GraphData stores forward, JVP, and VJP functions; it does
not carry the derivative laws required by the proof-carrying Graph type.
In other words, this is where the abstract approximation graph model meets the executable graph interpreter used elsewhere in TorchLean.
Executable forward-pass soundness for an NF RevGraph erased to GraphData.
The theorem says that evaluating the executable GraphData forward interpreter gives the same
runtime context covered by RevGraph.eval_approx, so the abstract graph approximation theorem
applies to the executable representation.
Executable backward-pass soundness for an NF RevGraph erased to GraphData.
Given approximate inputs and approximate seed cotangents, executable GraphData.backpropCtx
approximates the real-spec reverse-mode result with the bound computed by the NF backend.
Extract one typed gradient and its numerical error from executable reverse mode.
This is the common bridge used by every optimizer theorem below. Keeping the projection here avoids
repeating a proof that the ith entry of an approximated heterogeneous context is itself
approximated.
A typed backward-and-update step #
The seed context represents the cotangent supplied by a loss. The theorem below takes one gradient
from the executable reverse pass and applies an arbitrary proved numerical optimizer contract to
the corresponding parameter tensor. It is deliberately indexed by i: models with many parameter
tensors apply the same theorem to each entry of the typed parameter context.
Executable reverse mode followed by any valid numerical optimizer contract is sound.
The theorem is shape-polymorphic and optimizer-polymorphic. assumptionsHold is trivial for
globally sound updates such as SGD and records domain conditions for updates such as AdamW whose
square root and division must stay away from singularities. No optimizer needs a separate graph
theorem. Models with several parameter tensors instantiate this theorem at each typed index.
Architecture-independent reporting #
Proof-free numerical summary of one forward/backward/update step.
The arrays retain typed-context order. A UI may attach architecture-specific display names after lowering, but propagation itself does not inspect whether the graph came from an MLP, CNN, transformer, or another model family.
Instances For
Compute the report consumed by CLI, file, or InfoView front ends.
This function is intentionally proof-free: backprop_optimizer_update_approx_graphData is the
theorem establishing its interpretation when the input, seed, parameter, optimizer-state, and
step assumptions hold.