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 derivatives are evaluated only when the scalar instance declares their algebra exact. LayerNorm derivatives remain unresolved: the rowwise rule with stored affine parameters and epsilon has not yet been connected to this interval pass. A missing box is reported as a propagation failure by the certificate consumers.

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

Propagate first-derivative intervals from a scalar 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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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} [TorchLean.Storage α] [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.runScalarSecondDerivative {α : Type} [TorchLean.Storage α] [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.