Public rounded backward bounds #
The public objective result encloses its real objective whether it comes from the directed
reverse sweep or from the output-box fallback. The forward IBP boxes enter through
GraphPoint.ibp_encloses; runCROWNBackwardObjective_encloses_runIBP discharges it for the boxes
of runIBP.
def
NN.MLTheory.CROWN.Graph.DirectedBackward.AffineRowsEnclose
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
(bounds : FlatAffineBounds α)
(x y : ℕ → ℝ)
:
Real coordinate enclosure by the two stored affine rows.
Instances For
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.scalarBounds_enclose
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{n : ℕ}
{lower upper : AffineVec α n 1}
{x : ℕ → ℝ}
{z : ℝ}
(h : (affineValue lower fun (i : Fin n) => x ↑i) ≤ z ∧ z ≤ affineValue upper fun (i : Fin n) => x ↑i)
:
AffineRowsEnclose { inDim := n, outDim := 1, loAff := lower, hiAff := upper } x fun (x : ℕ) => z
A scalar pair gives the corresponding one-row enclosure.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.runCROWNBackwardObjective_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
(hrounded : BoundOps.supportsExactAffineReassociation α = false)
{g : Graph}
{ps : ParamStore α}
{ibp : Array (Option (FlatBox α))}
{ctx : AffineCtx}
{dims : ℕ → ℕ}
{v : ℕ → ℕ → ℝ}
(point : GraphPoint g.nodes ps ibp ctx dims v)
(output : ℕ)
(houtput : output < g.nodes.size)
(obj : FlatTensor α)
(hdim : obj.n = dims output)
{bounds : FlatAffineBounds α}
(hresult : g.runCROWNBackwardObjective ps ctx ibp output obj = some bounds)
:
The public rounded objective API returns a sound scalar affine enclosure, including its
output-box fallback, provided the forward IBP boxes in point are sound. The exact-reassociation
branch has a separate arithmetic contract.