Pooling operator bounds

This file provides simple interval-bound-propagation (IBP) transfer rules for 2D max/average pooling. These rules are used by the graph-level CROWN/LiRPA development when a model contains pooling operators.

References

• IBP: Gowal et al., On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models, 2018. (arXiv:1810.12715)
• CROWN: Zhang et al., Efficient Neural Network Robustness Certification with General Activation Functions, NeurIPS 2018. (arXiv:1811.00866)
• auto_LiRPA: Xu et al., Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond, NeurIPS 2020. (arXiv:2002.12920)

structure NN.MLTheory.CROWN.Operators.Pool2DConfig : Type

Configuration for 2D pooling.

This matches the common (kernel, stride, padding) parameters used by deep-learning libraries.

• kH : ℕ

  Kernel height.

• kW : ℕ

  Kernel width.

• stride : ℕ

  Stride (used for both height and width).

• padding : ℕ

  Padding (used for all sides).

def NN.MLTheory.CROWN.Operators.poolOutputSize (inSize padding kSize stride : ℕ) : ℕ

Compute output dimensions for pooling

Max Pooling IBP

For max pooling, the interval bounds are:

• Lower bound: max of all lower bounds in the window
• Upper bound: max of all upper bounds in the window

We use Numbers.neg_thousand as a practical lower bound for initialization since the Context typeclass doesn't provide negative infinity.

def NN.MLTheory.CROWN.Operators.get2D {α : Type} {h w : ℕ} (t : Spec.Tensor α (Spec.Shape.dim h (Spec.Shape.dim w Spec.Shape.scalar))) (i j : ℕ) (default : α) : α

Get element from 2D tensor with bounds checking, returns default if out of bounds

def NN.MLTheory.CROWN.Operators.ibpMaxpool2dChannel {α : Type} [Context α] {inH inW : ℕ} (cfg : Pool2DConfig) (xB : Box α (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar))) : Box α (Spec.Shape.dim (poolOutputSize inH cfg.padding cfg.kH cfg.stride) (Spec.Shape.dim (poolOutputSize inW cfg.padding cfg.kW cfg.stride) Spec.Shape.scalar))

IBP for MaxPool2D on a single channel 2D input. Input shape: (H, W), Output shape: (outH, outW)

Average Pooling IBP

For average pooling, the interval bounds are:

• Lower bound: average of all lower bounds in the window
• Upper bound: average of all upper bounds in the window

def NN.MLTheory.CROWN.Operators.ibpAvgpool2dChannel {α : Type} [Context α] {inH inW : ℕ} (cfg : Pool2DConfig) (xB : Box α (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar))) : Box α (Spec.Shape.dim (poolOutputSize inH cfg.padding cfg.kH cfg.stride) (Spec.Shape.dim (poolOutputSize inW cfg.padding cfg.kW cfg.stride) Spec.Shape.scalar))

IBP for AvgPool2D on a single channel 2D input.

Global Pooling

Global max/average pooling reduces entire spatial dimensions to a single value.

def NN.MLTheory.CROWN.Operators.get3D {α : Type} {c h w : ℕ} (t : Spec.Tensor α (Spec.Shape.dim c (Spec.Shape.dim h (Spec.Shape.dim w Spec.Shape.scalar)))) (ch i j : ℕ) (default : α) : α

Get element from 3D tensor (C, H, W)

def NN.MLTheory.CROWN.Operators.ibpGlobalAvgpool {α : Type} [Context α] {c h w : ℕ} (xB : Box α (Spec.Shape.dim c (Spec.Shape.dim h (Spec.Shape.dim w Spec.Shape.scalar)))) : Box α (Spec.Shape.dim c Spec.Shape.scalar)

IBP for Global Average Pooling

def NN.MLTheory.CROWN.Operators.ibpGlobalMaxpool {α : Type} [Context α] {c h w : ℕ} (xB : Box α (Spec.Shape.dim c (Spec.Shape.dim h (Spec.Shape.dim w Spec.Shape.scalar)))) : Box α (Spec.Shape.dim c Spec.Shape.scalar)

IBP for Global Max Pooling