Directed evaluation of backward affine bounds

The returned affine functions have a real interpretation. Their executable interval evaluator rounds each product, sum, and final constant outwards before returning a scalar box.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.affineBoundsEval_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (bounds : FlatAffineBounds α) (box : FlatBox α) (x y : ℕ → ℝ) (hx : RowEncloses box bounds.inDim x) (hy : AffineRowsEnclose bounds x y) : RowEncloses { dim := bounds.outDim, lo := (bounds.evalOnFlatBox box ⋯).lo, hi := (bounds.evalOnFlatBox box ⋯).hi } bounds.outDim y

Evaluating a pair of real affine enclosures on an enclosing input box retains enclosure.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.evalBackwardObjectiveBox_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (bounds : FlatAffineBounds α) (xB : FlatBox α) (inputDim : ℕ) (x y : ℕ → ℝ) (hx : RowEncloses xB bounds.inDim x) (hy : AffineRowsEnclose bounds x y) {result : FlatBox α} (hresult : evalBackwardObjectiveBox? bounds xB inputDim = Except.ok result) : RowEncloses result 1 y

The public scalar-box evaluator encloses every point enclosed by its affine argument.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.backwardObjectiveBox_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (hrounded : BoundOps.supportsExactAffineReassociation α = false) {g : Graph} {ps : ParamStore α} {ibp : Array (Option (FlatBox α))} {ctx : AffineCtx} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (point : GraphPoint g.nodes ps ibp ctx dims v) (xB : FlatBox α) (hx : RowEncloses xB ctx.inputDim (v ctx.inputId)) (output : ℕ) (houtput : output < g.nodes.size) (obj : FlatTensor α) (hdim : obj.n = dims output) {result : FlatBox α} (hresult : g.backwardObjectiveBox? ps ctx ibp xB output obj = Except.ok result) : RowEncloses result 1 fun (x : ℕ) => dot (dims output) (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) (v output)

The rounded objective workflow returns an interval containing its real output objective, including all directed arithmetic in both propagation and final evaluation, provided the forward IBP boxes in point are sound. backwardObjectiveBox_encloses_runIBP_all derives those enclosures from the input boxes and the real node equations.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.backwardObjectiveBox_encloses_runIBP {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] (hrounded : BoundOps.supportsExactAffineReassociation α = false) {g : Graph} {ps : ParamStore α} {ctx : AffineCtx} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (input_lt : ctx.inputId < g.nodes.size) (input_dim : dims ctx.inputId = ctx.inputDim) (input_kind : g.nodes[ctx.inputId]!.kind = IR.OpKind.input) (node_id : ∀ id < g.nodes.size, g.nodes[id]!.id = id) (parent_lt : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id) (hsupported : ibpForwardSupported g.nodes = true) (hinputs : InputsInBoxes g.nodes ps dims v) (equation : ∀ id < g.nodes.size, NodeEquation g.nodes ps (g.runIBP ps) dims v id) (xB : FlatBox α) (hx : RowEncloses xB ctx.inputDim (v ctx.inputId)) (output : ℕ) (houtput : output < g.nodes.size) (obj : FlatTensor α) (hdim : obj.n = dims output) {result : FlatBox α} (hresult : g.backwardObjectiveBox? ps ctx (g.runIBP ps) xB output obj = Except.ok result) : RowEncloses result 1 fun (x : ℕ) => dot (dims output) (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) (v output)

The rounded objective workflow, run on the boxes of runIBP, returns an interval containing its real output objective. Forward IBP, the backward sweep, and the final evaluation are all covered, for graphs whose node kinds pass ibpForwardSupported.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.backwardObjectiveBox_encloses_runIBP_all {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] [LawfulMinBoundOps α] (hrounded : BoundOps.supportsExactAffineReassociation α = false) {g : Graph} {ps : ParamStore α} {ctx : AffineCtx} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (input_lt : ctx.inputId < g.nodes.size) (input_dim : dims ctx.inputId = ctx.inputDim) (input_kind : g.nodes[ctx.inputId]!.kind = IR.OpKind.input) (node_id : ∀ id < g.nodes.size, g.nodes[id]!.id = id) (parent_lt : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id) (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) (hinputs : InputsInBoxes g.nodes ps dims v) (equation : ∀ id < g.nodes.size, RealNodeEquation g.nodes ps (g.runIBP ps) dims v id) (xB : FlatBox α) (hx : RowEncloses xB ctx.inputDim (v ctx.inputId)) (output : ℕ) (houtput : output < g.nodes.size) (obj : FlatTensor α) (hdim : obj.n = dims output) {result : FlatBox α} (hresult : g.backwardObjectiveBox? ps ctx (g.runIBP ps) xB output obj = Except.ok result) : RowEncloses result 1 fun (x : ℕ) => dot (dims output) (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) (v output)

Forward IBP, rounded backward propagation, and final interval evaluation enclose the real objective for every graph operation. Intermediate bounds are proved from the input boxes.