FP32 CROWN/IBP Integration

The CROWN/IBP development (NN/MLTheory/CROWN/*) proves real-valued enclosure theorems of the form “the network output lies in this box”.

This module combines those real enclosures with float32 forward-error bounds (expressed using approxTensor) to obtain a float32-sound enclosure: we inflate the real box by the explicit forward error budget.

This is the key separation of concerns:

• CROWN/IBP proves a real-valued semantic enclosure.
• RuntimeApprox/FP32 proves the rounded runtime output is close to that real-valued output.
• This file composes the two by uniformly widening the box.

"Float32" and the _fp32 suffix here mean the rounded-real model TorchLean.Floats.FP32 := NF binaryRadix fexp32 rnd32. These theorems say nothing about Lean's Float32 type or the bit-level ExecFloat.Binary 8 23 model. Finite binary32 add/mul refinements are in NN/Floats/IEEEExec/Bridge/Finite.lean; further arithmetic refinements are in NN/Proofs/RuntimeApprox/IEEE32/Arithmetic.lean.

Scalar Margin Lemmas

theorem NN.Proofs.RuntimeApprox.FP32.interval_contains_inflate_of_abs_error {l u y : ℝ} {yR : R} {eps : ℝ} (hy : l ≤ y ∧ y ≤ u) (happrox : |toSpec yR - y| ≤ eps) : l - eps ≤ toSpec yR ∧ toSpec yR ≤ u + eps

If a real value y lies in [l, u] and a runtime value yR is within eps of y, then the interpreted runtime value lies in the widened interval [l - eps, u + eps].

This is the scalar heart of the FP32/CROWN bridge.

theorem NN.Proofs.RuntimeApprox.FP32.fp32_le_of_real_le_sub_margin {y t : ℝ} {yR : R} {eps : ℝ} (h : y ≤ t - eps) (happrox : |toSpec yR - y| ≤ eps) : toSpec yR ≤ t

One-sided upper-margin rule.

If the real value is at least eps below threshold t, then any FP32 value within eps is still below t.

theorem NN.Proofs.RuntimeApprox.FP32.fp32_ge_of_real_ge_add_margin {y t : ℝ} {yR : R} {eps : ℝ} (h : y ≥ t + eps) (happrox : |toSpec yR - y| ≤ eps) : toSpec yR ≥ t

One-sided lower-margin rule.

If the real value is at least eps above threshold t, then any FP32 value within eps is still above t.

Inflating Real Boxes To Cover FP32 Execution

noncomputable def NN.Proofs.RuntimeApprox.FP32.inflateBoxUniform {s : Spec.Shape} (B : MLTheory.CROWN.Box ℝ s) (eps : ℝ) : MLTheory.CROWN.Box ℝ s

Uniformly widen a real-valued CROWN.Box by eps in every component.

The lower face moves down by eps; the upper face moves up by eps. This is kept simple and conservative, matching an L∞-style output error bound.

theorem NN.Proofs.RuntimeApprox.FP32.box_contains_inflateUniform_of_approx {s : Spec.Shape} {B : MLTheory.CROWN.Box ℝ s} {yS : TorchLean.Tensor ℝ s} {yR : TorchLean.Tensor R s} {eps : ℝ} (hy : B.contains yS) (happrox : Proofs.RuntimeApprox.approxTensor toSpec yS yR eps) : (inflateBoxUniform B eps).contains (Proofs.RuntimeApprox.tensorToSpec toSpec yR)

Tensor version of interval_contains_inflate_of_abs_error.

If the real-spec output yS is inside a real CROWN/IBP box B, and the FP32 runtime output yR approximates yS within uniform eps, then the interpreted FP32 output is inside the uniformly widened box.

noncomputable def NN.Proofs.RuntimeApprox.FP32.ibpReluTwoLayerErrorBudget {inDim hidDim outDim : ℕ} (netR : MLTheory.CROWN.TwoLayerMLP R inDim hidDim outDim) (xR : TorchLean.Tensor R [inDim]) (eW1 eb1 eW2 eb2 ex : ℝ) : ℝ

Forward-error budget used to inflate the real IBP box for a two-layer ReLU network.

theorem NN.Proofs.RuntimeApprox.FP32.ibpBound_contains_reluTwoLayerMlp_fp32 {inDim hidDim outDim : ℕ} (netS : MLTheory.CROWN.TwoLayerMLP ℝ inDim hidDim outDim) (netR : MLTheory.CROWN.TwoLayerMLP R inDim hidDim outDim) (xB : MLTheory.CROWN.Box ℝ (Spec.Shape.dim inDim Spec.Shape.scalar)) (xS : TorchLean.Tensor ℝ [inDim]) (xR : TorchLean.Tensor R [inDim]) {eW1 eb1 eW2 eb2 ex : ℝ} (hW1 : Proofs.RuntimeApprox.approxTensor toSpec netS.hiddenWeight netR.hiddenWeight eW1) (hb1 : Proofs.RuntimeApprox.approxTensor toSpec netS.hiddenBias netR.hiddenBias eb1) (hW2 : Proofs.RuntimeApprox.approxTensor toSpec netS.outputWeight netR.outputWeight eW2) (hb2 : Proofs.RuntimeApprox.approxTensor toSpec netS.outputBias netR.outputBias eb2) (hx : Proofs.RuntimeApprox.approxTensor toSpec xS xR ex) (hxB : xB.contains xS) : (inflateBoxUniform (MLTheory.CROWN.boundIbp netS xB) (ibpReluTwoLayerErrorBudget netR xR eW1 eb1 eW2 eb2 ex)).contains (Proofs.RuntimeApprox.tensorToSpec toSpec (have l1R := { weights := netR.hiddenWeight, bias := netR.hiddenBias }; have l2R := { weights := netR.outputWeight, bias := netR.outputBias }; have z1R := Spec.linearSpec l1R xR; have a1R := TorchLean.Tensor.mapSpec Proofs.RuntimeApprox.NFBackend.reluR z1R; Spec.linearSpec l2R a1R))

Float32-sound IBP for a 2-layer ReLU MLP, via uniform output-box inflation:

1. Use the real-spec IBP theorem NN.MLTheory.CROWN.Theorems.bound_ibp_sound.
2. Use approxTensor to bound FP32 forward error (approxTensor_reluTwoLayerMlp_fp32).
3. Inflate the real IBP box by that error bound.

The result is a real-valued interval that is guaranteed to contain the FP32 execution result.