Soundness of affine relaxations (CROWN / LiRPA)

This file proves basic inequalities and compositional lemmas used by affine-relaxation bound propagation (LiRPA) methods, in particular the CROWN/DeepPoly family.

The main result in this file is an end-to-end soundness statement for a small MLP, assembled from:

• soundness of affine images of scalar intervals,
• soundness of the ReLU triangular upper relaxation,
• soundness of affine composition through linear layers,
• an IBP-style fallback used by bound_affine (so the end-to-end theorem is sound but not tight).

For certificate-checking theorems over the graph dialect (the form used by TorchLean verification examples), see:

• NN.MLTheory.CROWN.Proofs.GraphCrownCertSoundness
• NN.MLTheory.CROWN.Proofs.GraphAlphaCrownTransferSoundness

References

• CROWN: Zhang et al., Efficient Neural Network Robustness Certification with General Activation Functions, NeurIPS 2018. (arXiv:1811.00866)
• β-CROWN / α/β-CROWN: Wang et al., Beta-CROWN: Efficient Bound Propagation with Provable Guarantees, NeurIPS 2021. (arXiv:2103.06624)
• auto_LiRPA: https://github.com/Verified-Intelligence/auto_LiRPA
• alpha-beta-CROWN: https://github.com/Verified-Intelligence/alpha-beta-CROWN

theorem NN.MLTheory.CROWN.Soundness.affine_scalar_interval_sound (a b x lo hi : ℝ) (hx : lo ≤ x ∧ x ≤ hi) : min (a * lo + b) (a * hi + b) ≤ a * x + b ∧ a * x + b ≤ max (a * lo + b) (a * hi + b)

If $x\in[\ell,h]$, then the affine function $f(x)=ax+b$ satisfies

$$ f(x)\in[\min(a\ell+b,ah+b),\max(a\ell+b,ah+b)]. $$

theorem NN.MLTheory.CROWN.Soundness.relu_affine_upper_bound_sound (z l u : ℝ) (hz : l ≤ z ∧ z ≤ u) : have relu_z := max 0 z; have slope := if l ≥ 0 then 1 else if u ≤ 0 then 0 else u / (u - l); have bias := if l ≥ 0 then 0 else if u ≤ 0 then 0 else -l * u / (u - l); relu_z ≤ slope * z + bias

The ReLU upper affine bound is sound. For $\operatorname{ReLU}(z)$ with $z\in[l,u]$, the triangular relaxation provides an upper bound.

The CROWN relaxation uses:

• If $l\ge 0$: slope $=1$, bias $=0$; ReLU is the identity.
• If $u\le 0$: slope $=0$, bias $=0$; ReLU is zero.
• If $l<0<u$: slope $=\frac{u}{u-l}$ and bias $=-\frac{lu}{u-l}$, the linear upper envelope.

theorem NN.MLTheory.CROWN.Soundness.crown_affine_twoLayerMlp_sound {inDim hidDim outDim : ℕ} (net : TwoLayerMLP ℝ inDim hidDim outDim) (xB : Box ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (x : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (hx : xB.contains x) : (boundAffine net xB).contains (forward net x)

Main theorem: CROWN affine bounds are sound for two-layer MLPs. If $x\in x_B$, then $\operatorname{forward}(\mathrm{net},x)\in\operatorname{boundAffine}(\mathrm{net},x_B)$.

This is the key soundness theorem for CROWN: it shows that the affine relaxation computed by bound_affine is indeed an overapproximation of the true network output.