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. This is the executable enclosure algorithm; its regression tests compare the result with directed IBP. An end-to-end theorem for the rounded backward pass remains separate work, as does any claim relating a host runtime's evaluation order to the reassociated backward expression.

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

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.

def NN.MLTheory.CROWN.Graph.runCROWNBackwardObjective {α : Type} [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (outputId : ℕ) (obj : FlatVec α) : 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} [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} [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (xB : FlatBox α) (outputId : ℕ) (obj : FlatVec α) : 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, with lo[0] and hi[0] bounding objᵀ * output over xB.

def NN.MLTheory.CROWN.Graph.runCROWNBackwardObjectiveLowerWithReluAlpha {α : Type} [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ctx : AffineCtx) (ibp : Array (Option (FlatBox α))) (outputId : ℕ) (obj : FlatVec α) (reluAlpha : Array (Option (FlatVec α))) : 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 currently refine the exact scalar path. Rounded scalar backends use the directed coefficient pass; until imported slopes carry their own rounding contract, nonlinear nodes are discharged against directed IBP boxes.