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.

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

def NN.MLTheory.CROWN.Graph.runCROWNBackwardObjective {α : Type} [Context α] (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 α] (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 chosen/optimized outside TorchLean and then imported as a per-node vector in reluAlpha.