Conv2D Forward Approximation #
NF (rounded) backend: Conv2D forward runtime→spec approximation.
This file proves soundness of the NFBackend.conv2dPointBound/conv2dBoundTensor bounds and
packages Conv2D as a FwdNode so it composes via FwdGraph.eval_approx.
PyTorch analogue: a forward Conv2D op (typically torch.nn.functional.conv2d) plus the standard
“stack over channels/spatial positions” tensor semantics.
https://pytorch.org/docs/stable/generated/torch.nn.functional.conv2d.html
Map of this file #
- Small fold/indexing lemmas (
foldl_flatMap,entry_eq_scalar_get_at_or_zero3) used to align the spec definition of convolution with the bound-generating replay in the runtime proof. approx_conv2d_point: elementwise forward error bound for a single(out_ch, i, j)output.approxT_conv2d_spec: tensor-levelapproxTstatement obtained by lifting the pointwise bound.conv2dNode: packaging as aFwdNodeso it composes inside larger graphs.
References #
- Dumoulin & Visin, A guide to convolution arithmetic for deep learning (indexing/stride/padding conventions).
- Goodfellow, Bengio, Courville, Deep Learning (MIT Press, 2016), Chapter on convolutional networks.
theorem
Proofs.RuntimeApprox.NFBackend.foldl_flatMap
{α β γ : Type}
(l : List α)
(g : α → List β)
(f : γ → β → γ)
(init : γ)
:
List.foldl f init (List.flatMap g l) = List.foldl (fun (acc : γ) (a : α) => List.foldl f acc (g a)) init l
theorem
Proofs.RuntimeApprox.NFBackend.entry_eq_scalar_get_at_or_zero3
{α : Type}
[Zero α]
{n1 n2 n3 : ℕ}
(t : Spec.Tensor α (Spec.Shape.dim n1 (Spec.Shape.dim n2 (Spec.Shape.dim n3 Spec.Shape.scalar))))
(i1 : Fin n1)
(i2 : Fin n2)
(i3 : Fin n3)
:
(match
match
match t with
| Spec.Tensor.dim f => f i1 with
| Spec.Tensor.dim f => f i2 with
| Spec.Tensor.dim f => f i3) = Spec.Tensor.scalar (Spec.getAtOrZero t [↑i1, ↑i2, ↑i3])
theorem
Proofs.RuntimeApprox.NFBackend.approx_conv2d_point
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{inC outC kH kW stride padding inH inW : ℕ}
{h1 : inC ≠ 0}
{h2 : kH ≠ 0}
{h3 : kW ≠ 0}
{kernelS :
Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))}
{kernelR :
Spec.Tensor (TorchLean.Floats.NF β fexp rnd)
(Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))}
{biasS : Spec.Tensor ℝ (Spec.Shape.dim outC Spec.Shape.scalar)}
{biasR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim outC Spec.Shape.scalar)}
{inputS : Spec.MultiChannelImage inC inH inW ℝ}
{inputR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd)}
{epsK epsB epsX : ℝ}
(hK : approxT toSpec kernelS kernelR epsK)
(hB : approxT toSpec biasS biasR epsB)
(hX : approxT toSpec inputS inputR epsX)
(out_ch : Fin outC)
(i : Fin (conv2dOutH inH kH stride padding))
(j : Fin (conv2dOutW inW kW stride padding))
:
have layerS := { kernel := kernelS, bias := biasS };
have layerR := { kernel := kernelR, bias := biasR };
|toSpec (Spec.getAtOrZero (Spec.conv2dSpec layerR inputR) [↑out_ch, ↑i, ↑j]) - Spec.getAtOrZero (Spec.conv2dSpec layerS inputS) [↑out_ch, ↑i, ↑j]| ≤ conv2dPointBound layerR inputR epsK epsB epsX out_ch i j
Pointwise forward soundness for Conv2D in the rounded NF backend.
Given spec/runtime approximations for the kernel, bias, and input, this bounds the absolute error
of a single output entry of Spec.conv2dSpec by conv2dPointBound (a replay-style bound
constructed from local per-term bounds).
theorem
Proofs.RuntimeApprox.NFBackend.approxT_conv2d_spec
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{inC outC kH kW stride padding inH inW : ℕ}
{h1 : inC ≠ 0}
{h2 : kH ≠ 0}
{h3 : kW ≠ 0}
{kernelS :
Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))}
{kernelR :
Spec.Tensor (TorchLean.Floats.NF β fexp rnd)
(Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))}
{biasS : Spec.Tensor ℝ (Spec.Shape.dim outC Spec.Shape.scalar)}
{biasR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim outC Spec.Shape.scalar)}
{inputS : Spec.MultiChannelImage inC inH inW ℝ}
{inputR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd)}
{epsK epsB epsX : ℝ}
(hK : approxT toSpec kernelS kernelR epsK)
(hB : approxT toSpec biasS biasR epsB)
(hX : approxT toSpec inputS inputR epsX)
:
have layerS := { kernel := kernelS, bias := biasS };
have layerR := { kernel := kernelR, bias := biasR };
have outS := Spec.conv2dSpec layerS inputS;
have outR := Spec.conv2dSpec layerR inputR;
have bT := conv2dBoundTensor layerR inputR epsK epsB epsX;
approxT toSpec outS outR (linfNorm bT)
Tensor-level forward approximation for Conv2D (approxT).
This lifts approx_conv2d_point to an approxT statement for the full output tensor, with a
global error linfNorm (conv2dBoundTensor ...) that upper-bounds all pointwise error entries.
noncomputable def
Proofs.RuntimeApprox.NFBackend.conv2dNode
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{Γ : List Spec.Shape}
{inC outC kH kW stride padding inH inW : ℕ}
{h1 : inC ≠ 0}
{h2 : kH ≠ 0}
{h3 : kW ≠ 0}
(kernelIdx : Idx Γ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar)))))
(biasIdx : Idx Γ (Spec.Shape.dim outC Spec.Shape.scalar))
(inputIdx : Idx Γ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar))))
:
FwdNode toSpec Γ
(Spec.Shape.dim outC
(Spec.Shape.dim (conv2dOutH inH kH stride padding)
(Spec.Shape.dim (conv2dOutW inW kW stride padding) Spec.Shape.scalar)))
Package Conv2D as a FwdNode for use in FwdGraph.eval_approx.
The node reads kernel/bias/input from the typed context Γ, runs the spec/runtime forward passes,
and uses approxT_conv2d_spec as its soundness proof.