Floats integration for CROWN (optional) #
This module bridges the CROWN bound-propagation development with the Floats infrastructure. It provides rounded-arithmetic variants of a few bound-propagation helpers, intended for experiments where you want the CROWN computations themselves to follow an explicit rounding model.
This is not required for the core CROWN proof layer and is grouped under
NN/MLTheory/CROWN/Extras/.
noncomputable def
NN.MLTheory.CROWN.Float.rFMA
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
(a b acc : ℝ)
:
Rounded multiply-add helper: round(a*b) then round(acc + ·).
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.rAdd
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
(x y : ℝ)
:
Rounded add
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.rMul
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
(x y : ℝ)
:
Rounded mul
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.rMax
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
(x y : ℝ)
:
Rounded max of two reals (stable under rounding by evaluating in ℝ, then rounding).
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.rMin
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
(x y : ℝ)
:
Rounded min of two reals (stable under rounding by evaluating in ℝ, then rounding).
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.ibpLinearFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{m n : ℕ}
(W : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(xB : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar))
(bB : Box ℝ (Spec.Shape.dim m Spec.Shape.scalar))
:
Interval (IBP) linear layer with rounded arithmetic.
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.ibpReluFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{n : ℕ}
(xB : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar))
:
Interval ReLU with float rounding: computes min/max of relu over bounds then rounds.
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.matVecMulFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{m n : ℕ}
(W : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(v : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar))
:
Rounded matrix-vector multiplication (m×n by n)
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.matMulFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{m n p : ℕ}
(A : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(B : Spec.Tensor ℝ (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar)))
:
Rounded matrix-matrix multiplication (m×n by n×p)
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.matColScaleFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{m n : ℕ}
(A : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(v : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar))
:
Rounded column scaling: multiply each column j by v[j].
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.reluRelaxSlopeVec
{n : ℕ}
(relax : Spec.Tensor (ReLURelax ℝ) (Spec.Shape.dim n Spec.Shape.scalar))
:
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.reluRelaxBiasVec
{n : ℕ}
(relax : Spec.Tensor (ReLURelax ℝ) (Spec.Shape.dim n Spec.Shape.scalar))
:
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.vecAddFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{n : ℕ}
(x y : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar))
:
Rounded elementwise add and mul on vectors
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.vecMulFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{n : ℕ}
(x y : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar))
:
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.affineEvalOnBoxFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{inDim outDim : ℕ}
(A : Spec.Tensor ℝ (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar)))
(c : Spec.Tensor ℝ (Spec.Shape.dim outDim Spec.Shape.scalar))
(B : Box ℝ (Spec.Shape.dim inDim Spec.Shape.scalar))
:
Box ℝ (Spec.Shape.dim outDim Spec.Shape.scalar)
Evaluate affine on a box with rounding (vector case).
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.boundAffineFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{inDim hidDim outDim : ℕ}
(net : MLP2 ℝ inDim hidDim outDim)
(xB : Box ℝ (Spec.Shape.dim inDim Spec.Shape.scalar))
:
Box ℝ (Spec.Shape.dim outDim Spec.Shape.scalar)
Affine (CROWN) bounds with rounding for a 2-layer MLP
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.boundIbpFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{inDim hidDim outDim : ℕ}
(net : MLP2 ℝ inDim hidDim outDim)
(xB : Box ℝ (Spec.Shape.dim inDim Spec.Shape.scalar))
:
Box ℝ (Spec.Shape.dim outDim Spec.Shape.scalar)
End-to-end rounded IBP for 2-layer MLP (mirrors CROWN.bound_ibp).
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.crownMlp2BoundsFloat
{inDim hidDim outDim : ℕ}
(l1 : Spec.LinearSpec ℝ inDim hidDim)
(l2 : Spec.LinearSpec ℝ hidDim outDim)
(x_center : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar))
(eps : ℝ)
(β : TorchLean.Floats.NeuralRadix := TorchLean.Floats.binaryRadix)
(fexp : ℤ → ℤ := fun (k : ℤ) => k)
(rnd : ℝ → ℤ := TorchLean.Floats.neuralNearestEven)
[TorchLean.Floats.NeuralValidExp fexp]
[TorchLean.Floats.NeuralValidRnd rnd]
:
Box ℝ (Spec.Shape.dim outDim Spec.Shape.scalar)
Public API: float-rounded CROWN IBP bounds wrapper with default config.
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.crownMlp2BoundsFloatFull
{inDim hidDim outDim : ℕ}
(l1 : Spec.LinearSpec ℝ inDim hidDim)
(l2 : Spec.LinearSpec ℝ hidDim outDim)
(x_center : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar))
(eps : ℝ)
(β : TorchLean.Floats.NeuralRadix := TorchLean.Floats.binaryRadix)
(fexp : ℤ → ℤ := fun (k : ℤ) => k)
(rnd : ℝ → ℤ := TorchLean.Floats.neuralNearestEven)
[TorchLean.Floats.NeuralValidExp fexp]
[TorchLean.Floats.NeuralValidRnd rnd]
:
Public API: float-rounded (IBP, Affine) bounds wrapper, mirroring CROWN.Examples.
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.reluVecFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{n : ℕ}
(x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar))
:
Rounded vector ReLU.
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.forwardFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{inDim hidDim outDim : ℕ}
(net : MLP2 ℝ inDim hidDim outDim)
(x : Spec.Tensor ℝ (Spec.Shape.dim inDim Spec.Shape.scalar))
:
Spec.Tensor ℝ (Spec.Shape.dim outDim Spec.Shape.scalar)
Rounded forward pass for a 2-layer MLP (linear → ReLU → linear).
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.roundVecFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{n : ℕ}
(v : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar))
:
Round every scalar in a vector tensor to the target float grid.
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.roundMatFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{m n : ℕ}
(A : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
:
Round every scalar in a matrix tensor to the target float grid.
Instances For
noncomputable def
NN.MLTheory.CROWN.Float.quantizeParamsFloat
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
(rnd : ℝ → ℤ)
[TorchLean.Floats.NeuralValidExp fexp]
{inDim hidDim outDim : ℕ}
(net : MLP2 ℝ inDim hidDim outDim)
:
Pre-quantize an MLP2's parameters (W1, b1, W2, b2) onto the float grid.