Objective-Dependent Backward CROWN

Forward CROWN gives nodewise bounds. This module handles the complementary use case: start from a linear objective on an output node and propagate that objective backward through the graph, choosing local relaxations from the sign of the downstream coefficients.

For exact scalar backends, the coefficient transformations are ordinary algebraic identities. For rounded scalar backends, TorchLean carries intervals for the coefficients and evaluates every coefficient product and sum outwards through BoundOps. The DirectedBackward proof modules establish enclosure for the reverse sweep, its public fallback, and final interval evaluation, under lawful directed arithmetic, real stored-parameter graph equations, and enclosing IBP boxes. Relating a separate host runtime's evaluation order to this real graph requires an additional runtime-approximation theorem.

The backward pass covers the same verifier dialect as runCROWN where objective-dependent relaxations are available. Unsupported nodes consume already-computed IBP boxes conservatively.

inductive NN.MLTheory.CROWN.Graph.Internal.BackwardDir : Type

Which end of the objective enclosure a backward sweep is computing.

Every relaxation choice below branches on this, because a lower bound wants the pessimistic endpoint of each local relaxation and an upper bound the optimistic one.

• lower : BackwardDir

  Compute a lower bound on the objective.

• upper : BackwardDir

  Compute an upper bound on the objective.

def NN.MLTheory.CROWN.Graph.Internal.consumeObjectiveFromBox {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (dir : BackwardDir) (aY : FlatTensor α) (B : FlatBox α) : Option α

Discharge an active objective against a node's IBP box.

Coordinatewise, the endpoint of the box that extremizes aY i * y i is selected from the sign of the coefficient, and the products are accumulated with directed rounding. The result is therefore sound even though the objective is not pushed any further back.

def NN.MLTheory.CROWN.Graph.Internal.constantObjectiveAffine {α : Type} [TorchLean.Storage α] [Context α] (inputDim : ℕ) (c : α) : AffineVec α inputDim 1

Regard a scalar objective enclosure as an affine form with zero input coefficients.

def NN.MLTheory.CROWN.Graph.Internal.objectiveFromOutputBox {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (dir : BackwardDir) (ibp : Array (Option (FlatBox α))) (outputId inputDim : ℕ) (obj : FlatTensor α) : Option (AffineVec α inputDim 1)

Bound an objective directly from the output box, without affine reassociation.

Directed affine propagation

An interval coefficient [a₋, a₊] records all values that a mathematically exact backward coefficient may take after the verifier has evaluated its arithmetic with outward rounding. Linear and structural nodes preserve these coefficients. At a node without a directed affine rule, the active objective is discharged against that node's directed IBP box.

The final conversion chooses one endpoint of each coefficient interval according to the sign of the corresponding input interval. When an input interval crosses zero, a directed constant correction accounts for the coefficient endpoint that was not selected.

structure NN.MLTheory.CROWN.Graph.Internal.DirectedBackwardState (α : Type) [TorchLean.Storage α] [Context α] : Type

Accumulator for the directed sweep: an interval coefficient per node and a two-sided constant.

• coeffs : Array (Option (FlatBox α))

  Interval coefficients per node; none for nodes the objective has not reached yet.

• cstLo : α

  Lower end of the accumulated constant term.

• cstHi : α

  Upper end of the accumulated constant term.

• failed : Bool

  Set once an active objective could not be propagated safely.

def NN.MLTheory.CROWN.Graph.Internal.DirectedBackwardState.fail {α : Type} [TorchLean.Storage α] [Context α] (st : DirectedBackwardState α) : DirectedBackwardState α

Mark the directed sweep as failed.

def NN.MLTheory.CROWN.Graph.Internal.addDirectedCoeff {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (st : DirectedBackwardState α) (pid : ℕ) (v : FlatBox α) : DirectedBackwardState α

Accumulate an interval coefficient into node pid, adding outwards on both ends.

def NN.MLTheory.CROWN.Graph.Internal.negateDirectedCoeff {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (v : FlatBox α) : FlatBox α

Negate an interval coefficient, which swaps its two endpoints.

def NN.MLTheory.CROWN.Graph.Internal.directedDotBox {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (a b : FlatBox α) : Option (α × α)

Outward-rounded interval inner product, or none on a length mismatch.

def NN.MLTheory.CROWN.Graph.Internal.addDirectedConstant {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (st : DirectedBackwardState α) (cLo cHi : α) : DirectedBackwardState α

Accumulate a two-sided constant contribution, rounding each end outwards.

def NN.MLTheory.CROWN.Graph.Internal.consumeDirectedObjective {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (st : DirectedBackwardState α) (aY By : FlatBox α) : DirectedBackwardState α

Discharge an active interval objective against a node's directed IBP box.

def NN.MLTheory.CROWN.Graph.Internal.directedBackwardLinear {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] {m n : ℕ} (aY : FlatBox α) (W : TorchLean.Tensor α [m, n]) (b : TorchLean.Tensor α [m]) : Option (FlatBox α × α × α)

Push an interval objective back through y = W x + b.

The coefficient for input j is the interval sum of the products aY i * W i j, and the bias contributes a two-sided constant.

def NN.MLTheory.CROWN.Graph.Internal.splitDirectedCoeff {α : Type} [TorchLean.Storage α] [Context α] (layout : ConcatLayout) (aY : FlatBox α) : Option (Array (FlatBox α))

Split interval coefficients into parent occurrences using the concat coordinate map.

def NN.MLTheory.CROWN.Graph.Internal.concatBackwardLayout? {α : Type} [TorchLean.Storage α] [Context α] (nodes : Array Node) (ibp : Array (Option (FlatBox α))) (node : Node) (axis : ℕ) : Option ConcatLayout

Check parent boxes as well as graph geometry before routing a concat objective.

def NN.MLTheory.CROWN.Graph.Internal.backwardPermuteVec {α : Type} [TorchLean.Storage α] {n : ℕ} (perm : Fin n → Fin n) (v : TorchLean.Tensor α [n]) : TorchLean.Tensor α [n]

Reindex a flat vector by a permutation of its coordinates.

def NN.MLTheory.CROWN.Graph.Internal.directedAxisPermutation? {α : Type} [TorchLean.Storage α] [Context α] (outputShape : Spec.Shape) (forwardPerm : Array ℕ) (aY : FlatBox α) : Option (FlatBox α)

Pull interval coefficients back through a permutation without scalar arithmetic.

def NN.MLTheory.CROWN.Graph.Internal.runBackwardObjectiveDir {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (dir : BackwardDir) (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (outputId : ℕ) (obj : FlatTensor α) : Option (AffineVec α ctx.inputDim 1)

Run a complete backward sweep in one direction and return the objective as an affine form in the graph input, or none when some node along the way could not be handled.

def NN.MLTheory.CROWN.Graph.Internal.directedBackwardNode {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (nodes : Array Node) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (ctx : AffineCtx) (st : DirectedBackwardState α) (id : ℕ) : DirectedBackwardState α

One step of the directed sweep, carrying interval coefficients instead of exact ones.

def NN.MLTheory.CROWN.Graph.Internal.directedCoeffAffine {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (l u al au : α) : (α × α) × α × α

Select affine endpoints for one interval coefficient, including the crossing-zero correction.

def NN.MLTheory.CROWN.Graph.Internal.directedInputAffines {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (inputDim : ℕ) (xB aIn : FlatBox α) (cLo cHi : α) : Option (AffineVec α inputDim 1 × AffineVec α inputDim 1)

Turn the interval coefficients that reached the input into a lower and an upper affine form.

Each coefficient endpoint is selected from the sign of the corresponding input interval. When that interval straddles zero, no single endpoint is valid throughout, and the one that was not selected becomes a directed constant correction.

def NN.MLTheory.CROWN.Graph.Internal.runDirectedBackwardObjective {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (outputId : ℕ) (obj : FlatTensor α) : Option (AffineVec α ctx.inputDim 1 × AffineVec α ctx.inputDim 1)

Run the directed backward sweep and return the lower and upper affine forms of the objective.

def NN.MLTheory.CROWN.Graph.directedNodeBounds? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (outputId : ℕ) : Option (FlatAffineBounds α)

Nodewise affine bounds obtained by directed backward propagation of the coordinate objectives.

The rows share the checked node intervals. Coefficients are rounded outwards throughout each sweep, including cancellation and sign changes; rounding only the final affine evaluation would not enclose errors introduced while composing coefficients. A node without a directed transfer retains its IBP enclosure as constant affine forms.

These bounds target the real-arithmetic graph described by the stored parameters, under the backend's directed-arithmetic contract. They do not establish an error bound for a separate floating-point execution schedule.

def NN.MLTheory.CROWN.Graph.runCROWNBackwardObjective {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (outputId : ℕ) (obj : FlatTensor α) : Option (FlatAffineBounds α)

Objective-dependent backward CROWN bound for a scalar objective.

Given a linear objective objᵀ * output, this runs a backward pass that propagates the objective coefficients through the graph, selects the relaxation attached to each node, and returns a pair of affine bounds on the objective with respect to ctx.inputId.

The returned FlatAffineBounds always has outDim = 1 (a scalar objective).

def NN.MLTheory.CROWN.Graph.evalBackwardObjectiveBox? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (bounds : FlatAffineBounds α) (xB : FlatBox α) (inputDim : ℕ) : Except String (FlatBox α)

Evaluate already-computed backward-CROWN objective bounds on an input box.

def NN.MLTheory.CROWN.Graph.backwardObjectiveBox? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (xB : FlatBox α) (outputId : ℕ) (obj : FlatTensor α) : Except String (FlatBox α)

Run objective-dependent backward CROWN and evaluate the scalar objective bounds on the input box.

The result is a FlatBox of dimension 1. Under the backend and graph soundness hypotheses, lo[0] and hi[0] enclose objᵀ * output for evaluations whose designated input lies in xB and whose node values satisfy the supplied ibp boxes.

For a claim over all of xB, those boxes must be valid throughout the claimed input region. When ibp is obtained from runIBP g ps, the seeded input boxes in ps must cover the input valuations in that claim. This function does not check compatibility between xB and those seeds.

def NN.MLTheory.CROWN.Graph.runCROWNBackwardObjectiveLowerWithReluAlpha {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (outputId : ℕ) (obj : FlatTensor α) (reluAlpha : Array (Option (FlatTensor α))) : Option (AffineVec α ctx.inputDim 1)

Backward CROWN objective lower bound with externally provided ReLU alpha slopes.

This is an integration hook for alpha-CROWN style workflows where ReLU slopes are optimized outside TorchLean and then imported as a per-node vector in reluAlpha. Imported slopes are used only on the exact scalar path. The directed coefficient pass of a rounded backend has no ReLU relaxation (it discharges every ReLU against its IBP box), so on such a backend this returns none whenever some entry of reluAlpha is present, rather than silently computing a bound without the slopes. With no slopes it returns the directed lower bound.