IBP at conv depth — a compositional interval-bound engine #

IntervalBound.lean proves the L∞ certificate for exactly one shape: dense ∘ relu ∘ dense, dense-only, hard-wired at two layers (ibp2_certified_at_eps). That is the shape the 784→16→10 scorecards use, and it is the reason the IBP tier stops at one hidden layer.

This file removes both restrictions. The soundness argument for IBP is compositional — "the box propagates" is a property of one layer, and depth is just ∘ — so the engine here is:

• InBox3 / InBox — a point lies in an axis-aligned box (tensor / the head's logits);
• BoxSound3 f Flo Fhi — (Flo, Fhi) is a sound interval transformer for f;
• BoxSound3.comp — depth: sound transformers compose exactly as the layers do, so an n-layer net's transformer is n compositions and no new proof;
• per-layer instances — relu (endpoint max), conv2d (sign-split over the padded taps), maxPool2 (max is monotone, so pool the endpoints), and the dense head denseT (sign-split);
• ibp3_certified_of_boxSound — the capstone: a sound tensor body and dense head whose output boxes separate on x ∓ ε certify x at L∞ radius ε, at any depth.

The conv transformer is stated against the repo's own conv2d (CNN.lean, SAME padding, the definition the VJP suite and the codegen use) — not a re-modelled convolution. Padding contributes 0 to both endpoints, which is why the sign-split can sit outside the pad test (convTap is monotone, and constant 0 where the window falls off the image).

convLo_uniform / convHi_uniform are the conv peers of denseLo_uniform/denseHi_uniform: on the first layer's uniform box x ∓ ε the interval image collapses to conv2d W b x ∓ ε · conv2d |W| 0 𝟙, i.e. one extra convolution by the absolute kernel against the all-ones image. That keeps the generated per-image data at "one forward pass + one |W| pass" instead of two full sign-split sums — the conv analogue of the ⟨w,x⟩ ∓ ε‖w‖₁ collapse the 784-dim files already exploit.

Nonlinearity note: as in IntervalBound.lean, unstable (sign-crossing) ReLUs and tied max-pool windows are handled soundly, not assumed away — the box simply contains both branches. The certificate is sound and incomplete; counts derived from it are lower bounds only.

Everything is elementary and closes under propext / Classical.choice / Quot.sound.

References #

• Gowal et al. 2018, On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. https://arxiv.org/abs/1810.12715
• Mirman, Gehr, Vechev 2018, Differentiable Abstract Interpretation for Provably Robust Neural Networks. https://proceedings.mlr.press/v80/mirman18b.html

A conv classifier is Tensor3 → Vec k: a tensor body then a dense head that reads the activation directly. Stating the certificate there keeps flatten out of every per-image proof (it is an Equiv computation, and paying for it at each of the head's inputs is the difference between a cheap instance and an unaffordable one).