BackwardScale

Backward (reverse-mode) scale propagation.

This optional module mirrors NN.Proofs.RuntimeApprox.Graph.BackwardApprox, but for scale bounds (nonnegative bounds on linf_norm) rather than eps error bounds.

Use it alongside the backward approximation graph when you want to derive abs+rel tolerances for gradients/cotangents from both an eps error bound and a propagated magnitude bound.

def Proofs.RuntimeApprox.AddScaleSound {α : Type} (toSpec : α → Spec.SpecScalar) [Add α] (addBound : {Δ : List Spec.Shape} → BList Δ → BList Δ → TList α Δ → TList α Δ → BList Δ) : Prop

Soundness condition for accumulating scale bounds under addition in a context.

structure Proofs.RuntimeApprox.RevNodeScale {α : Type} (toSpec : α → Spec.SpecScalar) (Γ : List Spec.Shape) (τ : Spec.Shape) extends Proofs.RuntimeApprox.RevNode toSpec Γ τ : Type

A reverse node augmented with forward+VJP scale bounds.

• forwardSpec : TList Spec.SpecScalar Γ → Spec.SpecTensor τ
• forwardRuntime : TList α Γ → Spec.Tensor α τ
• bound : EList Γ → TList α Γ → Spec.SpecScalar
• sound (xS : TList Spec.SpecScalar Γ) (xR : TList α Γ) (eps : EList Γ) : approxCtx toSpec xS xR eps → approxT toSpec (self.forwardSpec xS) (self.forwardRuntime xR) (self.bound eps xR)
• vjpSpec : TList Spec.SpecScalar Γ → Spec.SpecTensor τ → TList Spec.SpecScalar Γ
• vjpRuntime : TList α Γ → Spec.Tensor α τ → TList α Γ
• vjpBound : EList Γ → TList α Γ → Spec.SpecScalar → Spec.Tensor α τ → EList Γ
• vjpSound (ctxS : TList Spec.SpecScalar Γ) (ctxR : TList α Γ) (epsCtx : EList Γ) (δS : Spec.SpecTensor τ) (δR : Spec.Tensor α τ) (epsδ : Spec.SpecScalar) : approxCtx toSpec ctxS ctxR epsCtx → approxT toSpec δS δR epsδ → approxCtx toSpec (self.vjpSpec ctxS δS) (self.vjpRuntime ctxR δR) (self.vjpBound epsCtx ctxR epsδ δR)
• fwdScaleBound : BList Γ → TList α Γ → NNReal
• fwdScaleSound (ctxS : TList Spec.SpecScalar Γ) (ctxR : TList α Γ) (epsCtx : EList Γ) (bCtx : BList Γ) : approxCtx toSpec ctxS ctxR epsCtx → scaleCtx toSpec ctxS ctxR bCtx → scaleT toSpec (self.forwardSpec ctxS) (self.forwardRuntime ctxR) (self.fwdScaleBound bCtx ctxR)
• vjpScaleBound : BList Γ → TList α Γ → NNReal → Spec.Tensor α τ → BList Γ
• vjpScaleSound (ctxS : TList Spec.SpecScalar Γ) (ctxR : TList α Γ) (epsCtx : EList Γ) (bCtx : BList Γ) (δS : Spec.SpecTensor τ) (δR : Spec.Tensor α τ) (bδ : NNReal) : approxCtx toSpec ctxS ctxR epsCtx → scaleCtx toSpec ctxS ctxR bCtx → scaleT toSpec δS δR bδ → scaleCtx toSpec (self.vjpSpec ctxS δS) (self.vjpRuntime ctxR δR) (self.vjpScaleBound bCtx ctxR bδ δR)

inductive Proofs.RuntimeApprox.RevGraphScale {α : Type} (toSpec : α → Spec.SpecScalar) (Γ : List Spec.Shape) : List Spec.Shape → Type

Reverse-mode graph with scale-aware nodes.

• nil {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} : RevGraphScale toSpec Γ []
• snoc {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} {τ : Spec.Shape} : RevGraphScale toSpec Γ ss → RevNodeScale toSpec (Γ ++ ss) τ → RevGraphScale toSpec Γ (ss ++ [τ])

def Proofs.RuntimeApprox.RevGraphScale.toRevGraph {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} : RevGraphScale toSpec Γ ss → RevGraph toSpec Γ ss

Forget the scale annotations on nodes, producing an ordinary RevGraph.

def Proofs.RuntimeApprox.RevGraphScale.toFwdGraphScale {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} : RevGraphScale toSpec Γ ss → FwdGraphScale toSpec Γ ss

Convert a RevGraphScale into a FwdGraphScale by dropping the reverse-mode payload.

theorem Proofs.RuntimeApprox.RevGraphScale.toFwdGraph_toFwdGraphScale_eq {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) : g.toFwdGraphScale.toFwdGraph = g.toRevGraph.toFwdGraph

def Proofs.RuntimeApprox.RevGraphScale.evalSpec {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) (x : TList Spec.SpecScalar Γ) : TList Spec.SpecScalar (Γ ++ ss)

Evaluate the forward pass on spec values, returning the extended context Γ ++ ss.

def Proofs.RuntimeApprox.RevGraphScale.evalRuntime {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) (x : TList α Γ) : TList α (Γ ++ ss)

Evaluate the forward pass on runtime values, returning the extended context Γ ++ ss.

@[simp]

theorem Proofs.RuntimeApprox.RevGraphScale.evalSpec_eq_rev {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) (x : TList Spec.SpecScalar Γ) : g.evalSpec x = g.toRevGraph.evalSpec x

@[simp]

theorem Proofs.RuntimeApprox.RevGraphScale.evalRuntime_eq_rev {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) (x : TList α Γ) : g.evalRuntime x = g.toRevGraph.evalRuntime x

def Proofs.RuntimeApprox.RevGraphScale.evalBounds {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) (epsIn : EList Γ) (xR : TList α Γ) : EList (Γ ++ ss)

Forward-pass error bounds for all intermediate nodes, computed from input bounds epsIn.

def Proofs.RuntimeApprox.RevGraphScale.evalScales {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) (bIn : BList Γ) (xR : TList α Γ) : BList (Γ ++ ss)

Forward-pass scale bounds for all intermediate nodes, computed from input bounds bIn.

theorem Proofs.RuntimeApprox.RevGraphScale.eval_scale {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) (xS : TList Spec.SpecScalar Γ) (xR : TList α Γ) (epsIn : EList Γ) (bIn : BList Γ) : approxCtx toSpec xS xR epsIn → scaleCtx toSpec xS xR bIn → scaleCtx toSpec (g.evalSpec xS) (g.evalRuntime xR) (g.evalScales bIn xR)

def Proofs.RuntimeApprox.RevGraphScale.backpropScales {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) [Add α] (bIn : BList Γ) (xR : TList α Γ) (bSeed : BList (Γ ++ ss)) (seedR : TList α (Γ ++ ss)) (addBound : {Δ : List Spec.Shape} → BList Δ → BList Δ → TList α Δ → TList α Δ → BList Δ) : BList Γ

Backpropagate scale bounds through a RevGraphScale, analogous to RevGraph.backpropRuntime.

theorem Proofs.RuntimeApprox.RevGraphScale.backprop_scale {α : Type} {toSpec : α → Spec.SpecScalar} {Γ ss : List Spec.Shape} (g : RevGraphScale toSpec Γ ss) [Add α] (addBound : {Δ : List Spec.Shape} → BList Δ → BList Δ → TList α Δ → TList α Δ → BList Δ) (addSound : AddScaleSound toSpec fun {Δ : List Spec.Shape} => addBound) (xS : TList Spec.SpecScalar Γ) (xR : TList α Γ) (epsIn : EList Γ) (bIn : BList Γ) (seedS : TList Spec.SpecScalar (Γ ++ ss)) (seedR : TList α (Γ ++ ss)) (bSeed : BList (Γ ++ ss)) : approxCtx toSpec xS xR epsIn → scaleCtx toSpec xS xR bIn → scaleCtx toSpec seedS seedR bSeed → scaleCtx toSpec (g.toRevGraph.backpropSpec xS seedS) (g.toRevGraph.backpropRuntime xR seedR) (g.backpropScales bIn xR bSeed seedR fun {Δ : List Spec.Shape} => addBound)