TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.CROWN.Proofs.DirectedConvSemantics

The scalar semantics of the convolution affine map #

Positive dilation makes each matrix coefficient a stored weight or zero. Consequently scalar interpretation commutes with the matrix converter, even when ordinary scalar addition rounds. The real spatial convolution then satisfies the affine equation used by backward CROWN.

source
def NN.MLTheory.CROWN.Graph.DirectedBackward.realConvSpec {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {d inC outC : ℕ} {kernel stride padding : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding α) :
Spec.ConvSpec d inC outC kernel stride padding ℝ

Interpret the stored kernel and bias without performing scalar arithmetic.

Instances For
    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.convLinearMatrix_map_value {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding α) (dilation paddingAfter : TorchLean.Tensor ℕ [d]) (groups : ℕ) (leading : Spec.Shape) (hdil : ∀ d_1 ∈ dilation.to (List ℕ), 0 < d_1) :
    convLinearMatrix (realConvSpec layer) dilation paddingAfter groups leading = TorchLean.Tensor.map LawfulBoundOps.toReal (convLinearMatrix layer dilation paddingAfter groups leading)

    For positive dilation, the scalar convolution matrix denotes its exact real counterpart.

    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.convBiasBroadcast_map_value {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {d outC : ℕ} {outSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor α [outC]) (leading : Spec.Shape) :
    convBiasBroadcast (TorchLean.Tensor.map LawfulBoundOps.toReal bias) leading = TorchLean.Tensor.map LawfulBoundOps.toReal (convBiasBroadcast bias leading)

    Bias broadcasting only copies stored values, so it commutes with scalar interpretation.

    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.convolutionPoint_eq_affine {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (parameters : IR.ConvParams α) (leading : Spec.Shape) (f : ℕ → ℝ) (hdil : ∀ d ∈ parameters.dilation.to (List ℕ), 0 < d) :
    convolutionPoint parameters leading f = (Spec.matVecMulSpec (TorchLean.Tensor.map LawfulBoundOps.toReal (affOfConv parameters leading).A) (pointVector (parameters.input leading).size f)).addSpec (TorchLean.Tensor.map LawfulBoundOps.toReal (affOfConv parameters leading).c)

    The exact spatial convolution is the real affine map of the stored scalar coefficients.

    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.planConvTransfer?_dilation_pos {α : Type} [TorchLean.Storage α] {configuration : IR.ConvConfig} {parameters : IR.ConvParams α} {parentShape outShape leading : Spec.Shape} (h : planConvTransfer? configuration parameters parentShape outShape = some leading) (d : ℕ) :
    d ∈ parameters.dilation.to (List ℕ) → 0 < d

    Every accepted convolution plan has positive stored dilation on each spatial axis.

    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ConvolutionNodeEquation.nodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {nodes : Array Node} {ps : ParamStore α} {ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} {configuration : IR.ConvConfig} (heq : ConvolutionNodeEquation nodes ps dims v id configuration) (hkind : nodes[id]!.kind = IR.OpKind.conv configuration) :
    NodeEquation nodes ps ibp dims v id

    The actual real convolution equation implies the affine equation used by backward CROWN.

    All geometry assumptions follow from the same successful plan that the graph engine consumes.