Exact rational reflection for algebraic certificates #

These lemmas connect executable rational tensor arithmetic to the existing real-valued tensor semantics. No floating-point rounding or transcendental approximation is involved.

source

@[instance_reducible]

def Spec.RationalAlgebraic.instBoundOpsRat :

NN.MLTheory.CROWN.BoundOps ℚ

Rational certificate arithmetic is exact, including affine reassociation.

Instances For

source

@[instance_reducible]

noncomputable def Spec.RationalAlgebraic.instLawfulBoundOpsRat :

NN.MLTheory.CROWN.LawfulBoundOps ℚ

The rational arithmetic dictionary satisfies the real enclosure laws.

Instances For

source

noncomputable def NN.Verification.Cert.RationalReflection.realTensor {s : Spec.Shape} (t : TorchLean.Tensor ℚ s) :

TorchLean.Tensor ℝ s

Interpret each rational tensor entry as a real number.

Instances For

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_get {n : ℕ} {s : Spec.Shape} (t : TorchLean.Tensor ℚ (Spec.Shape.dim n s)) (i : Fin n) :

Spec.get (realTensor t) i = realTensor (Spec.get t i)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_getScalar {n : ℕ} (t : TorchLean.Tensor ℚ [n]) (i : Fin n) :

(realTensor t).getScalar i = ↑(t.getScalar i)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_get2 {m n : ℕ} (t : TorchLean.Tensor ℚ [m, n]) (i : Fin m) (j : Fin n) :

Spec.get2 (realTensor t) i j = ↑(Spec.get2 t i j)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_fill {s : Spec.Shape} (q : ℚ) :

realTensor (TorchLean.Tensor.full s q) = TorchLean.Tensor.full s ↑q

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_add {s : Spec.Shape} (a b : TorchLean.Tensor ℚ s) :

realTensor (a.addSpec b) = (realTensor a).addSpec (realTensor b)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_matVecMul {m n : ℕ} (a : TorchLean.Tensor ℚ [m, n]) (b : TorchLean.Tensor ℚ [n]) :

realTensor (Spec.matVecMulSpec a b) = Spec.matVecMulSpec (realTensor a) (realTensor b)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_matMul {m n p : ℕ} (a : TorchLean.Tensor ℚ [m, n]) (b : TorchLean.Tensor ℚ [n, p]) :

realTensor (Spec.matMulSpec a b) = Spec.matMulSpec (realTensor a) (realTensor b)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_matPos {m n : ℕ} (w : TorchLean.Tensor ℚ [m, n]) :

realTensor (MLTheory.CROWN.IBP.matPos w) = MLTheory.CROWN.IBP.matPos (realTensor w)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_matNeg {m n : ℕ} (w : TorchLean.Tensor ℚ [m, n]) :

realTensor (MLTheory.CROWN.IBP.matNeg w) = MLTheory.CROWN.IBP.matNeg (realTensor w)

source

noncomputable def NN.Verification.Cert.RationalReflection.realBox {s : Spec.Shape} (b : MLTheory.CROWN.Box ℚ s) :

MLTheory.CROWN.Box ℝ s

Interpret both endpoints of a rational box over the reals.

Instances For

source

noncomputable def NN.Verification.Cert.RationalReflection.realFlatBox (b : MLTheory.CROWN.FlatBox ℚ) :

MLTheory.CROWN.FlatBox ℝ

Interpret a dimension-carrying rational box over the reals.

Instances For

source

noncomputable def NN.Verification.Cert.RationalReflection.realAffine {n m : ℕ} (a : MLTheory.CROWN.AffineVec ℚ n m) :

MLTheory.CROWN.AffineVec ℝ n m

Interpret the coefficients of an exact affine form.

Instances For

source

noncomputable def NN.Verification.Cert.RationalReflection.realAffineBounds (b : MLTheory.CROWN.Graph.FlatAffineBounds ℚ) :

MLTheory.CROWN.Graph.FlatAffineBounds ℝ

Interpret a pair of exact affine bounds.

Instances For

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.castAffineOut_self {α : Type} [Context α] {n m : ℕ} (a : MLTheory.CROWN.AffineVec α n m) (h : m = m) :

MLTheory.CROWN.Graph.castAffineOut h a = a

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realAffineBounds_linear {n m : ℕ} (w : TorchLean.Tensor ℚ [m, n]) (bias : TorchLean.Tensor ℚ [m]) (b : MLTheory.CROWN.Graph.FlatAffineBounds ℚ) (h : b.outDim = n) :

realAffineBounds (MLTheory.CROWN.Cert.linearBoundsFromAffine w bias b h ⋯) = MLTheory.CROWN.Cert.linearBoundsFromAffine (realTensor w) (realTensor bias) (realAffineBounds b) h ⋯

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realAffineBounds_const (n m : ℕ) (lo hi : TorchLean.Tensor ℚ [m]) :

realAffineBounds (MLTheory.CROWN.Cert.boundsConst n m lo hi) = MLTheory.CROWN.Cert.boundsConst n m (realTensor lo) (realTensor hi)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realAffineBounds_identity (n : ℕ) :

realAffineBounds (MLTheory.CROWN.Cert.boundsIdentity n) = MLTheory.CROWN.Cert.boundsIdentity n

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realTensor_relu {s : Spec.Shape} (t : TorchLean.Tensor ℚ s) :

realTensor (Activation.reluSpec t) = Activation.reluSpec (realTensor t)

source

noncomputable def NN.Verification.Cert.RationalReflection.realRelax (r : MLTheory.CROWN.Runtime.Ops.ReLURelax ℚ) :

MLTheory.CROWN.Runtime.Ops.ReLURelax ℝ

Interpret the slope and offset of a ReLU relaxation exactly.

Instances For

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realRelax_upper (l u : ℚ) :

realRelax (MLTheory.CROWN.Runtime.Ops.ReLU.relaxScalar l u) = MLTheory.CROWN.Runtime.Ops.ReLU.relaxScalar ↑l ↑u

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realRelax_lower (l u a : ℚ) :

realRelax (MLTheory.CROWN.Cert.alphaRelaxLowerScalar l u a) = MLTheory.CROWN.Cert.alphaRelaxLowerScalar ↑l ↑u ↑a

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realRelax_upperVec {n : ℕ} (lo hi : TorchLean.Tensor ℚ [n]) :

TorchLean.Tensor.map realRelax (MLTheory.CROWN.Runtime.Ops.ReLU.relaxVector lo hi) = MLTheory.CROWN.Runtime.Ops.ReLU.relaxVector (realTensor lo) (realTensor hi)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realRelax_lowerVec {n : ℕ} (lo hi alpha : TorchLean.Tensor ℚ [n]) :

TorchLean.Tensor.map realRelax (MLTheory.CROWN.Cert.alphaRelaxLowerVec lo hi alpha) = MLTheory.CROWN.Cert.alphaRelaxLowerVec (realTensor lo) (realTensor hi) (realTensor alpha)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realAffine_propagate {n m : ℕ} (r : TorchLean.Tensor (MLTheory.CROWN.Runtime.Ops.ReLURelax ℚ) [m]) (a : MLTheory.CROWN.AffineVec ℚ n m) :

realAffine (MLTheory.CROWN.Runtime.Ops.ReLU.propagateAffine r a) = MLTheory.CROWN.Runtime.Ops.ReLU.propagateAffine (TorchLean.Tensor.map realRelax r) (realAffine a)

source

@[simp]

theorem NN.Verification.Cert.RationalReflection.realBox_linear {m n : ℕ} (w : TorchLean.Tensor ℚ [m, n]) (x : MLTheory.CROWN.Box ℚ [n]) (bias : MLTheory.CROWN.Box ℚ [m]) :

realBox (MLTheory.CROWN.IBP.linear w x bias) = MLTheory.CROWN.IBP.linear (realTensor w) (realBox x) (realBox bias)