BugZoo: constant normalization slices

Normalization layers should have a boring answer on a constant slice. If every value in the slice being normalized is the same finite value x, then the slice mean is x, the variance is zero, and the normalized activations are zero.

For affine normalization layers this gives the contract:

$$ \operatorname{normalize}([x,x,\ldots])=\beta. $$

The scale/weight gradient for that slice is also zero, because it is multiplied by the normalized activation. This applies to the mathematical core behind LayerNorm, GroupNorm, InstanceNorm, and BatchNorm; those layers differ mainly in which axes define the slice.

Run python3 scripts/verification/normalization_contract_probe.py --device cpu to measure forward and backward residuals from PyTorch normalization kernels on constant tensors.

The theorems use real arithmetic with totalized division and square root. They assume the supplied mean and variance already equal x and zero; they do not prove that a floating-point statistics kernel computes those values exactly on a constant slice.

theorem NN.Examples.BugZoo.ConstantNormalizationSlice.constant_slice_normalizeCore_outputs_bias (x gamma beta epsilon : ℝ) : Spec.normalizeCore [] [] [] [] [] epsilon (TorchLean.Tensor.full [] x) (TorchLean.Tensor.full [] x) (TorchLean.Tensor.full [] 0) (TorchLean.Tensor.full [] gamma) (TorchLean.Tensor.full [] beta) ⋯ ⋯ ⋯ ⋯ = TorchLean.Tensor.full [] beta

TorchLean's scalar normalization core sends a constant normalized slice to the affine bias.

This is the pointwise representative of the GroupNorm/InstanceNorm/BatchNorm constant-slice contract: once the slice statistics are $\mathrm{mean}=x$ and $\mathrm{variance}=0$, the normalized contribution is zero and only beta remains.

theorem NN.Examples.BugZoo.ConstantNormalizationSlice.constant_slice_scale_grad_zero (dy x epsilon : ℝ) : dy * ((x - x) / MathFunctions.sqrt (max (0 + epsilon) 0)) = 0

The scale gradient contribution from a constant normalized slice is zero.