NeuralFloat Conv2D Bias/Kernel Backward Bounds #
This file proves pointwise NeuralFloat approximation bounds for the Conv2D bias and kernel gradients. The proofs replay the same summation structure used by the runtime backward pass and accumulate an explicit error budget for each output coordinate.
noncomputable def
Proofs.RuntimeApprox.NFBackend.conv2dBiasPointBound
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
{outC kH kW stride padding inH inW : ℕ}
(δR :
Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding)
(TorchLean.Floats.NF β fexp rnd))
(epsδ : ℝ)
(out_ch : Fin outC)
:
Pointwise error bound for the Conv2D bias gradient (NF runtime vs spec).
This bound is a replay of the bias-gradient summation with per-term error epsδ coming from the
grad_output approximation hypothesis.
Instances For
theorem
Proofs.RuntimeApprox.NFBackend.approx_conv2d_bias_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)}
{δS : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) ℝ}
{δR :
Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding)
(TorchLean.Floats.NF β fexp rnd)}
{epsδ : ℝ}
(hδ : approxT toSpec δS δR epsδ)
(out_ch : Fin outC)
:
have layerS := { kernel := kernelS, bias := biasS };
have layerR := { kernel := kernelR, bias := biasR };
|toSpec (Spec.getAtOrZero (Spec.conv2dBiasDerivSpec layerR inputR δR) [↑out_ch]) - Spec.getAtOrZero (Spec.conv2dBiasDerivSpec layerS inputS δS) [↑out_ch]| ≤ conv2dBiasPointBound δR epsδ out_ch
Soundness of the Conv2D bias-gradient pointwise bound.
Given approxT for grad_output, this shows the spec bias-gradient entry is approximated by the
NF runtime entry within conv2dBiasPointBound.
noncomputable def
Proofs.RuntimeApprox.NFBackend.conv2dBiasBoundTensor
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
{outC kH kW stride padding inH inW : ℕ}
(δR :
Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding)
(TorchLean.Floats.NF β fexp rnd))
(epsδ : ℝ)
:
Tensor-shaped bias-gradient bound.
This packages conv2dBiasPointBound into a Tensor so later approxT statements can use
linfNorm to obtain a single scalar error bound.
Instances For
noncomputable def
Proofs.RuntimeApprox.NFBackend.conv2dKernelPointBound
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
{inC outC kH kW stride padding inH inW : ℕ}
(inputR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd))
(δR :
Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding)
(TorchLean.Floats.NF β fexp rnd))
(epsX epsδ : ℝ)
(out_ch : Fin outC)
(in_ch : Fin inC)
(di : Fin kH)
(dj : Fin kW)
:
Pointwise error bound for the Conv2D kernel gradient (NF runtime vs spec).
The kernel-gradient entry accumulates products of padded input values and upstream gradients.
The bound is a replay of this accumulation with per-term errors derived from epsX and epsδ.
Instances For
theorem
Proofs.RuntimeApprox.NFBackend.approx_conv2d_kernel_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)}
{δS : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) ℝ}
{δR :
Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding)
(TorchLean.Floats.NF β fexp rnd)}
{epsX epsδ : ℝ}
(hX : approxT toSpec inputS inputR epsX)
(hδ : approxT toSpec δS δR epsδ)
(out_ch : Fin outC)
(in_ch : Fin inC)
(di : Fin kH)
(dj : Fin kW)
:
have layerS := { kernel := kernelS, bias := biasS };
have layerR := { kernel := kernelR, bias := biasR };
|toSpec (Spec.getAtOrZero (Spec.conv2dKernelDerivSpec layerR inputR δR) [↑out_ch, ↑in_ch, ↑di, ↑dj]) - Spec.getAtOrZero (Spec.conv2dKernelDerivSpec layerS inputS δS) [↑out_ch, ↑in_ch, ↑di, ↑dj]| ≤ conv2dKernelPointBound inputR δR epsX epsδ out_ch in_ch di dj
Soundness of the Conv2D kernel-gradient pointwise bound.
Given approxT hypotheses for the input and upstream gradient (grad_output), this shows the spec
kernel-gradient entry is approximated by the NF runtime entry within conv2dKernelPointBound.
noncomputable def
Proofs.RuntimeApprox.NFBackend.conv2dKernelBoundTensor
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
{inC outC kH kW stride padding inH inW : ℕ}
(inputR : Spec.MultiChannelImage inC inH inW (TorchLean.Floats.NF β fexp rnd))
(δR :
Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding)
(TorchLean.Floats.NF β fexp rnd))
(epsX epsδ : ℝ)
:
Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))
Tensor-shaped kernel-gradient bound.
This packages conv2dKernelPointBound into the full 4D kernel-tensor shape so later approxT
lemmas can use a single global bound via linfNorm.
Instances For
theorem
Proofs.RuntimeApprox.NFBackend.approxT_conv2d_bias_deriv_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)}
{δS : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) ℝ}
{δR :
Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding)
(TorchLean.Floats.NF β fexp rnd)}
{epsδ : ℝ}
(hδ : approxT toSpec δS δR epsδ)
:
have layerS := { kernel := kernelS, bias := biasS };
have layerR := { kernel := kernelR, bias := biasR };
have outS := Spec.conv2dBiasDerivSpec layerS inputS δS;
have outR := Spec.conv2dBiasDerivSpec layerR inputR δR;
have bT := conv2dBiasBoundTensor δR epsδ;
approxT toSpec outS outR (linfNorm bT)
Tensor-level approxT bound for the Conv2D bias gradient.
This lifts approx_conv2d_bias_point entrywise and packages the error into
linfNorm (conv2dBiasBoundTensor ...).
theorem
Proofs.RuntimeApprox.NFBackend.approxT_conv2d_kernel_deriv_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)}
{δS : Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding) ℝ}
{δR :
Spec.MultiChannelImage outC (conv2dOutH inH kH stride padding) (conv2dOutW inW kW stride padding)
(TorchLean.Floats.NF β fexp rnd)}
{epsX epsδ : ℝ}
(hX : approxT toSpec inputS inputR epsX)
(hδ : approxT toSpec δS δR epsδ)
:
have layerS := { kernel := kernelS, bias := biasS };
have layerR := { kernel := kernelR, bias := biasR };
have outS := Spec.conv2dKernelDerivSpec layerS inputS δS;
have outR := Spec.conv2dKernelDerivSpec layerR inputR δR;
have bT := conv2dKernelBoundTensor inputR δR epsX epsδ;
approxT toSpec outS outR (linfNorm bT)
Tensor-level approxT bound for the Conv2D kernel gradient.
This lifts approx_conv2d_kernel_point entrywise and packages the error into
linfNorm (conv2dKernelBoundTensor ...).