Soundness of the rounded forward IBP pass

runIBP computes one interval box per node with directed endpoint arithmetic. This file proves that, for any backend with LawfulBoundOps and LawfulNonlinearBoundOps, every box it returns encloses the real value of its node, provided the real point satisfies the node equations of NodeEquation and lies in the seeded input boxes.

The proof covers the node kinds accepted by ibpForwardSupportedNode: inputs, constants, copies, add, sub, mulElem, relu, linear, unary matmul, sum, and the pointwise exp, log, sqrt, inv, tanh, sigmoid, silu, sin, and cos. On such graphs GraphPoint.ofRunIBP builds the GraphPoint that the backward theorems take, so their IBP hypothesis is discharged. The corollaries runCROWNBackwardObjective_encloses_runIBP and directedNodeBounds_encloses_runIBP state the resulting end-to-end guarantees.

The original core-family interface is retained here. DirectedIBPFullSoundness extends the forward proof to every graph operation using RealNodeEquation and runIBP_encloses_all.

def NN.MLTheory.CROWN.Graph.DirectedBackward.ibpForwardSupportedNode (node : Node) : Bool

Node kinds whose forward IBP transfer is proved sound in this file. Binary matmul is not included because NodeEquation gives it no equation.

def NN.MLTheory.CROWN.Graph.DirectedBackward.ibpForwardSupported (nodes : Array Node) : Bool

Every node of the graph has a kind covered by the forward IBP soundness theorem.

def NN.MLTheory.CROWN.Graph.DirectedBackward.InputsInBoxes {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (nodes : Array Node) (ps : ParamStore α) (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) : Prop

The real point lies in every seeded input box.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpStepNodeAt?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {nodes : Array Node} {ps : ParamStore α} {boxes ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} (hsupported : ibpForwardSupportedNode nodes[id]! = true) (hinput : nodes[id]!.kind = IR.OpKind.input → ∀ (box : FlatBox α), ps.inputBoxes[id]? = some box → RowEncloses box (dims id) (v id)) (heq : NodeEquation nodes ps ibp dims v id) (hagree : ∀ p ∈ nodes[id]!.parents, boxes[p]?.join = ibp[p]!) (henc : ∀ p ∈ nodes[id]!.parents, ∀ (box : FlatBox α), ibp[p]! = some box → RowEncloses box (dims p) (v p)) {box : FlatBox α} (hstep : ibpStepNodeAt? nodes ps boxes id nodes[id]! = some box) : RowEncloses box (dims id) (v id)

One IBP transfer is sound: if the parent boxes enclose the parent values, the box computed for a supported node encloses its value.

boxes is the array the transfer reads and ibp the array named by the node equations; they agree at every parent.

The whole pass

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.runIBP_encloses_of_step {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : ParamStore α) {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (hparent : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id) (htransfer : ∀ id < g.nodes.size, ∀ (boxes : Array (Option (FlatBox α))), (∀ p ∈ g.nodes[id]!.parents, boxes[p]?.join = (g.runIBP ps)[p]!) → (∀ p ∈ g.nodes[id]!.parents, ∀ (box : FlatBox α), (g.runIBP ps)[p]! = some box → RowEncloses box (dims p) (v p)) → ∀ (box : FlatBox α), ibpStepNodeAt? g.nodes ps boxes id g.nodes[id]! = some box → RowEncloses box (dims id) (v id)) (id : ℕ) : id < g.nodes.size → ∀ (box : FlatBox α), (g.runIBP ps)[id]! = some box → RowEncloses box (dims id) (v id)

A sound node transfer lifts to the complete topologically ordered forward pass.

The array read by a transfer is only a prefix. Its parent entries agree with the final pass because later iterations do not overwrite earlier nodes.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.runIBP_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] (g : Graph) (ps : ParamStore α) {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (hparent : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id) (hsupported : ibpForwardSupported g.nodes = true) (hinputs : InputsInBoxes g.nodes ps dims v) (hequation : ∀ id < g.nodes.size, NodeEquation g.nodes ps (g.runIBP ps) dims v id) (id : ℕ) : id < g.nodes.size → ∀ (box : FlatBox α), (g.runIBP ps)[id]! = some box → RowEncloses box (dims id) (v id)

Soundness of the rounded forward IBP pass. Every box that runIBP returns encloses the value of its node, when the parents precede their consumers, every node kind is covered by ibpForwardSupportedNode, the input boxes contain the real inputs, and the real point satisfies the node equations.

If the semantic guard of runIBP rejects the graph, no box is produced and the statement holds trivially.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.GraphPoint.ofRunIBP {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {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) : GraphPoint g.nodes ps (g.runIBP ps) ctx dims v

The GraphPoint of a rounded runIBP pass. Its ibp_encloses field is runIBP_encloses.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.runCROWNBackwardObjective_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) (output : ℕ) (houtput : output < g.nodes.size) (obj : FlatTensor α) (hdim : obj.n = dims output) {bounds : FlatAffineBounds α} (hresult : g.runCROWNBackwardObjective ps ctx (g.runIBP ps) output obj = some bounds) : bounds.inDim = ctx.inputDim ∧ bounds.outDim = 1 ∧ AffineRowsEnclose bounds (v ctx.inputId) fun (x : ℕ) => dot (dims output) (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) (v output)

The public rounded objective, run on the boxes of runIBP, encloses the real objective. No IBP soundness is assumed: it comes from runIBP_encloses.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.directedNodeBounds_encloses_runIBP {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {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) (output : ℕ) (houtput : output < g.nodes.size) (hdim : dims output = g.nodes[output]!.outShape.size) {bounds : FlatAffineBounds α} (hresult : g.directedNodeBounds? ps ctx (g.runIBP ps) output = some bounds) : bounds.inDim = ctx.inputDim ∧ bounds.outDim = dims output ∧ AffineRowsEnclose bounds (v ctx.inputId) (v output)

The nodewise rounded CROWN bounds, run on the boxes of runIBP, enclose every coordinate of the output node. No IBP soundness is assumed.