TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.CROWN.Proofs.DirectedBackwardFallback

Soundness of the output-box fallback #

The public objective API can return a constant enclosure when its directed sweep fails. This file proves the sign-selected directed dot product used on that path.

source
def NN.MLTheory.CROWN.Graph.DirectedBackward.DirectionBound {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dir : Internal.BackwardDir) (bound : α) (z : ℝ) :
Prop

Interpret which side of a real objective a directed scalar bounds.

Instances For
    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.consumeObjectiveFromBox_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dir : Internal.BackwardDir) (obj : FlatTensor α) (box : FlatBox α) (x : ℕ → ℝ) (hx : RowEncloses box obj.n x) {bound : α} (hresult : Internal.consumeObjectiveFromBox dir obj box = some bound) :
    DirectionBound dir bound (dot obj.n (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) x)

    The executable sign-selected box dot product bounds its real objective.

    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.constantObjectiveAffine_value {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (n : ℕ) (c : α) (x : Fin n → ℝ) :
    affineValue (Internal.constantObjectiveAffine n c) x = LawfulBoundOps.toReal c

    Constant objective forms have exactly their stored real constant as value.

    source
    theorem NN.MLTheory.CROWN.Graph.DirectedBackward.objectiveFromOutputBox_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dir : Internal.BackwardDir) (ibp : Array (Option (FlatBox α))) (output n : ℕ) (obj : FlatTensor α) (y : ℕ → ℝ) (hbox : ∀ (box : FlatBox α), ibp[output]! = some box → RowEncloses box obj.n y) {aff : AffineVec α n 1} (hresult : Internal.objectiveFromOutputBox dir ibp output n obj = some aff) (x : Fin n → ℝ) :
    match dir, hresult with | Internal.BackwardDir.lower, hresult => affineValue aff x ≤ dot obj.n (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) y | Internal.BackwardDir.upper, hresult => dot obj.n (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) y ≤ affineValue aff x

    A successful output-box fallback returns an affine bound in the requested direction.