Derivative Interval Passes

These passes propagate interval bounds for first and second derivatives through the same flat graph used by IBP. Derivative propagation has its own chain-rule state but reuses FlatBox for every intermediate enclosure.

Linear operations, pointwise arithmetic, supported activations, and selected structural operations have explicit rules. Coupled softmax and layer-normalization derivatives are evaluated only when the scalar instance declares their algebra exact. Finite-precision instances otherwise leave those nodes unresolved instead of running the real-arithmetic formulas with rounded operations.

def NN.MLTheory.CROWN.Graph.runFirstDerivative1D {α : Type} [Context α] [BoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) : Array (Option (FlatBox α))

Propagate first-derivative intervals from a one-dimensional input.

The input derivative is the all-ones vector. The pass uses value-IBP boxes to bound activation derivatives and leaves an entry empty when it encounters an unsupported local derivative.

def NN.MLTheory.CROWN.Graph.runDirectionalDerivative {α : Type} [Context α] [BoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (seed : FlatBox α) : Array (Option (FlatBox α))

Propagate a directional first-derivative enclosure from a caller-supplied input seed.

A seed whose dimension differs from an input box leaves that input unresolved. Point seeds such as coordinate vectors recover partial derivatives; interval seeds propagate a family of directions through the same local derivative rules.

def NN.MLTheory.CROWN.Graph.runMixedSecondDerivative {α : Type} [Context α] [BoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : ParamStore α) (ibp dLeft dRight : Array (Option (FlatBox α))) : Array (Option (FlatBox α))

Propagate an enclosure of the mixed second derivative D²f[u, v].

dLeft and dRight are first-derivative passes seeded by directions u and v. The input mixed derivative is zero, while every nonlinear rule applies the bilinear second-order chain rule. Taking the two arrays equal recovers the second directional derivative D²f[v, v]; coordinate seeds can be paired with a fixed direction to recover the entries of a Hessian-vector product.

def NN.MLTheory.CROWN.Graph.runSecondDirectionalDerivative {α : Type} [Context α] [BoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : ParamStore α) (ibp dDirection : Array (Option (FlatBox α))) : Array (Option (FlatBox α))

Propagate the second directional derivative D²f[v, v] from one first-derivative pass.

def NN.MLTheory.CROWN.Graph.runHessianVectorProduct {α : Type} [Context α] [BoundOps α] [NonlinearBoundOps α] {inputDim : ℕ} (g : Graph) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (coordinateDerivatives : Fin inputDim → Array (Option (FlatBox α))) (directionalDerivative : Array (Option (FlatBox α))) : Fin inputDim → Array (Option (FlatBox α))

Compute an interval enclosure for each component of a Hessian-vector product.

coordinateDerivatives i is the first-derivative pass seeded by the ith coordinate vector; directionalDerivative is seeded by the vector being multiplied by the Hessian. The result at i is the mixed derivative D²f[eᵢ, v], i.e. the ith Hessian-vector component for scalar outputs.

def NN.MLTheory.CROWN.Graph.runSecondDerivative1D {α : Type} [Context α] [BoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : ParamStore α) (ibp d1 : Array (Option (FlatBox α))) : Array (Option (FlatBox α))

One-dimensional second derivatives are the all-ones directional special case.