TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.RuntimeApprox.Graph.LinkAutogradAlgebra

Link Proofs.RuntimeApprox.RevGraph to the executable Proofs.Autograd.Algebra.GraphData #

This is a definitional/structural bridge:

Both sides use TorchLean.TensorPack directly, so the bridge does not convert between different context representations.

Only forward evaluation and reverse accumulation are preserved. The required NodeData.jvp field is filled with the forward map, independent of its tangent argument: it is not a derivative and must not be used for forward-mode differentiation. This bridge also does not establish native kernel correspondence or that the supplied reverse maps are derivatives.

Note on environments (Δ): Proofs.Autograd.Algebra.GraphData is parameterized by an extra (non-differentiable) environment Δ threaded through evaluation. The runtime-approximation graphs here do not use such an environment, so we instantiate the executable layer at Δ := Unit and pass () during evaluation/backprop.

source
def Proofs.RuntimeApprox.LinkAutogradAlgebra.RevNode.toNodeData {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {τ : Spec.Shape} (node : RevNode toSpec Γ τ) :
Autograd.Algebra.NodeData α Unit Γ τ

Erase a RuntimeApprox.RevNode into an executable Autograd.Algebra.NodeData.

We take Δ := Unit (no extra environment). The JVP field repeats the forward map as a placeholder; only forward evaluation and VJP-based backprop are supported by this conversion.

Instances For
    source
    def Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.toGraphData {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) :
    Autograd.Algebra.GraphData α Unit Γ ss

    Erase a RuntimeApprox.RevGraph into executable Autograd.Algebra.GraphData (with Δ := Unit).

    This forgets all spec/bound metadata and keeps only the runtime forward and vjp closures.

    Instances For
      source
      theorem Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.evalRuntime_of_toGraphData {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (xR : TorchLean.TensorPack α Γ) :
      (toGraphData g).eval xR () = g.evalRuntime xR

      Erasing a RevGraph into executable GraphData preserves the runtime forward semantics.

      Informally: if you forget the spec and bound metadata and keep only the runtime closures, you still evaluate to the same runtime context.

      source
      theorem Proofs.RuntimeApprox.LinkAutogradAlgebra.RevGraph.backpropRuntime_of_toGraphData {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} [Add α] {ss : List Spec.Shape} (g : RevGraph toSpec Γ ss) (xR : TorchLean.TensorPack α Γ) (seedR : TorchLean.TensorPack α (Γ ++ ss)) :
      (toGraphData g).backpropCtx xR () seedR = g.backpropRuntime xR seedR

      Erasing a RevGraph into executable GraphData preserves the runtime backward semantics.

      Informally: the executable GraphData.backpropCtx computes the same reverse-mode accumulation as RevGraph.backpropRuntime when given the same runtime input context and seed cotangents.