Directed forward interval transfers #
Scalar, box, and parent-lookup lemmas shared by the rounded forward IBP proofs.
Scalar and box transfers #
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.affineEvalOnBox_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{n m : ℕ}
(aff : AffineVec α n m)
(box : Box α (Spec.Shape.dim n Spec.Shape.scalar))
(x : Fin n → ℝ)
(hx :
∀ (j : Fin n), LawfulBoundOps.toReal (box.lo.getScalar j) ≤ x j ∧ x j ≤ LawfulBoundOps.toReal (box.hi.getScalar j))
(i : Fin m)
:
LawfulBoundOps.toReal ((aff.evalOnBox box).lo.getScalar i) ≤ ∑ j : Fin n, LawfulBoundOps.toReal (Spec.get2 aff.A i j) * x j + LawfulBoundOps.toReal (aff.c.getScalar i) ∧ ∑ j : Fin n, LawfulBoundOps.toReal (Spec.get2 aff.A i j) * x j + LawfulBoundOps.toReal (aff.c.getScalar i) ≤ LawfulBoundOps.toReal ((aff.evalOnBox box).hi.getScalar i)
Directed affine interval evaluation encloses each real affine row.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.value_relu
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
(a : α)
:
The ReLU of an endpoint denotes the real ReLU of its value.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.rowEncloses_iff
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{d : ℕ}
{lo hi : TorchLean.Tensor α [d]}
{f : ℕ → ℝ}
:
RowEncloses { dim := d, lo := lo, hi := hi } d f ↔ ∀ (i : Fin d), LawfulBoundOps.toReal (lo.getScalar i) ≤ f ↑i ∧ f ↑i ≤ LawfulBoundOps.toReal (hi.getScalar i)
Coordinate bounds of a flat box, read through the typed accessor.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.boxAdd_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{x y : FlatBox α}
{n : ℕ}
{f g : ℕ → ℝ}
(hx : RowEncloses x n f)
(hy : RowEncloses y n g)
:
RowEncloses (boxAdd x y) n fun (i : ℕ) => f i + g i
Interval addition encloses the sum of enclosed coordinates.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.boxSub_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{x y : FlatBox α}
{n : ℕ}
{f g : ℕ → ℝ}
(hx : RowEncloses x n f)
(hy : RowEncloses y n g)
:
RowEncloses (boxSub x y) n fun (i : ℕ) => f i - g i
Interval subtraction encloses the difference of enclosed coordinates.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.boxMulElem_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{x y box : FlatBox α}
{n : ℕ}
{f g : ℕ → ℝ}
(hx : RowEncloses x n f)
(hy : RowEncloses y n g)
(hbox : boxMulElem x y = some box)
:
RowEncloses box n fun (i : ℕ) => f i * g i
The four-corner product box encloses the product of enclosed coordinates.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.boxRelu_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{x : FlatBox α}
{n : ℕ}
{f : ℕ → ℝ}
(hx : RowEncloses x n f)
:
RowEncloses (boxRelu x) n fun (i : ℕ) => max (f i) 0
Endpoint ReLU encloses the real ReLU of enclosed coordinates.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.boxUnaryEnclosure?_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
[NonlinearBoundOps α]
{F : ℝ → ℝ}
{enclose : α → α → Option (α × α)}
(hF : UnaryEnclosure F enclose)
{x box : FlatBox α}
{n : ℕ}
{f : ℕ → ℝ}
(hx : RowEncloses x n f)
(hbox : boxUnaryEnclosure? enclose x = some box)
:
RowEncloses box n fun (i : ℕ) => F (f i)
A lawful scalar enclosure, applied coordinatewise, encloses the pointwise image.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.ibpSilu?_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
[NonlinearBoundOps α]
[LawfulNonlinearBoundOps α]
{x box : FlatBox α}
{n : ℕ}
{f : ℕ → ℝ}
(hx : RowEncloses x n f)
(hbox : ibpSilu? x = some box)
:
The input-times-sigmoid transfer encloses real SiLU, without a monotonicity assumption.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.unaryEnclosure_inv
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
[NonlinearBoundOps α]
[LawfulNonlinearBoundOps α]
:
UnaryEnclosure (fun (x : ℝ) => x⁻¹) fun (lo hi : α) => NonlinearBoundOps.divBounds 1 1 lo hi
Reciprocal bounds are the division law with numerator 1.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.boxSum_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{x : FlatBox α}
{f : ℕ → ℝ}
(hx : RowEncloses x x.dim f)
{g : ℕ → ℝ}
(hg : g 0 = ∑ i : Fin x.dim, f ↑i)
:
RowEncloses (boxSum x) 1 g
Directed summation of all coordinates encloses the real sum.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.ibpLinearParams_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{p : LinParams α}
{x box : FlatBox α}
{f g : ℕ → ℝ}
(hx : RowEncloses x p.n f)
(hg :
∀ (i : Fin p.m),
g ↑i = ∑ j : Fin p.n, LawfulBoundOps.toReal (Spec.get2 p.w i j) * f ↑j + LawfulBoundOps.toReal (p.b.getScalar i))
(hbox : ibpLinearParams p x = some box)
:
RowEncloses box p.m g
The linear transfer encloses the real affine image of an enclosed input.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.ibpMatmul_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{id : ℕ}
{ps : ParamStore α}
{config : MatParams α}
(hconfig : ps.matmulW[id]? = some config)
{x box : FlatBox α}
{f g : ℕ → ℝ}
(hx : RowEncloses x config.n f)
(hg :
∀ (i : Fin config.m),
g ↑i = ∑ j : Fin config.n, LawfulBoundOps.toReal (Spec.get2 config.w i j) * f ↑j + LawfulBoundOps.toReal ((TorchLean.Tensor.full (Spec.Shape.dim config.m Spec.Shape.scalar) 0).getScalar i))
(hbox : ibpMatmul id ps x = some box)
:
RowEncloses box config.m g
The bias-free matmul transfer encloses the real matrix-vector product.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.RowEncloses.congr
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{box : FlatBox α}
{n : ℕ}
{f g : ℕ → ℝ}
(h : RowEncloses box n f)
(hfg : ∀ (i : Fin n), g ↑i = f ↑i)
:
RowEncloses box n g
Enclosure depends only on the coordinates below the box width.
One forward step #
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.unary_step
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{dims : ℕ → ℕ}
{v : ℕ → ℕ → ℝ}
{id p : ℕ}
{F : ℝ → ℝ}
{transfer : FlatBox α → Option (FlatBox α)}
(htransfer :
∀ {B box : FlatBox α} {n : ℕ} {f : ℕ → ℝ},
RowEncloses B n f → transfer B = some box → RowEncloses box n fun (i : ℕ) => F (f i))
(heq : UnaryEquation dims v id p F)
{B box : FlatBox α}
(hB : RowEncloses B (dims p) (v p))
(hbox : transfer B = some box)
:
RowEncloses box (dims id) (v id)
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.unary_lookup
{α : Type}
[TorchLean.Storage α]
[Context α]
{parents : Array ℕ}
{boxes : Array (Option (FlatBox α))}
{k : FlatBox α → Option (FlatBox α)}
{box : FlatBox α}
(h :
(do
let p ← IR.unaryParent? parents
let __do_lift ← boxes[p]?.join
k __do_lift) = some box)
:
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.binary_lookup
{α : Type}
[TorchLean.Storage α]
[Context α]
{parents : Array ℕ}
{boxes : Array (Option (FlatBox α))}
{k : FlatBox α → FlatBox α → Option (FlatBox α)}
{box : FlatBox α}
(h :
(do
let __x ← IR.binaryParents? parents
match __x with
| (p, q) => do
let x ← boxes[p]?.join
let y ← boxes[q]?.join
k x y) = some box)
: