Numerical certificate enclosures #
Foundational source-range validation, real and IEEE enclosure semantics, replay checks, and
pointwise error traces for graph numerical certificates. Most users should import
NN.Proofs.RuntimeApprox.Graph.NumericalCertificate.
Raw and checked source assumptions #
A binary32 range supplied for an input, constant, or explicit random source node.
- nodeId : ℕ
- enclosure : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32
Instances For
Instances For
A source range after the checker has established finite, ordered endpoints.
Instances For
Bitwise equality for executable binary32 intervals.
Bitwise equality is intentional: it distinguishes signed zero and preserves the exact endpoints
written in a certificate. NaNs are rejected separately by Interval32.Valid.
Instances For
Executable counterpart of Interval32.Valid.
Instances For
Interval32.leB decides the proposition-level IEEE non-strict order.
IEEE comparison between finite values implies the corresponding order on their real
interpretations. This lemma is intentionally finite: IEEE comparisons involving NaN are unordered,
and toReal is not the semantic interface for infinities.
Negation of a finite executable binary32 value decodes to real negation.
Flipping the sign bit preserves finiteness.
The executable validity test accepts exactly finite, ordered intervals.
Real semantics of the arithmetic transfers #
The executable checker propagates binary32 endpoints, while the graph specification is normally
read over real scalars. RealEncloses is the bridge between those views. Runtime rounding error is
then composed separately by FwdGraph.eval_approx and RevGraph.backprop_approx; keeping these two
claims separate prevents an interval enclosure from silently standing in for a floating-point
error theorem.
A real scalar lies between the real interpretations of an executable interval's endpoints.
Instances For
Convert the extended-real endpoint form used by the interval soundness library into an ordinary real interval when the output endpoints are finite.
Sound real enclosure for the canonical addition transfer.
Sound real enclosure for the canonical subtraction transfer.
Sound real enclosure for the canonical multiplication transfer.
Sound real enclosure for the canonical reciprocal transfer.
Every scalar entry of a shape-indexed real tensor lies in one interval.
Instances For
The exact executable interval [0,1].
Instances For
The exact executable interval [-1,1].
Instances For
Executable test for a finite endpoint's nonnegative IEEE sign. Both signed zeros are accepted; all other accepted values have a clear sign bit. Finiteness is supplied by interval validity.
Instances For
The stable real vector softmax is enclosed by the certificate transfer [0,1].
Sound real enclosure for the canonical ReLU interval transfer.
Sound real enclosure for the canonical absolute-value interval transfer.
A directed lower square-root endpoint lies below the exact real square root. FloatLib's nonnegative-input theorem includes both signed zeros.
Upper counterpart of toReal_sqrtDown_le.
Sound real enclosure for directed interval square root.
Lift a sound unary scalar transfer to tensors of arbitrary rank.
Tensor-level soundness of the ReLU interval transfer.
Tensor-level soundness of the absolute-value interval transfer.
Tensor-level soundness of directed interval square root.
Lift a sound binary scalar transfer to tensors of arbitrary rank.
Tensor-level soundness of outward-rounded interval addition.
Tensor-level soundness of outward-rounded interval subtraction.
Tensor-level soundness of outward-rounded interval multiplication.
Replay against bit-level graph execution #
Executable check that every binary32 tensor entry lies in an interval.
Instances For
Proposition expressed by tensorWithinRange.
Instances For
The executable tensor range check is exact for the IEEE comparison semantics.
From checked ranges to explicit error bounds #
Decode an executable tensor entrywise and state that the resulting real tensor lies in an
interval. Unlike IEEETensorEnclosed, this predicate talks directly about the real values used by
the approximation layer.
Instances For
A successful IEEE range check decodes to an ordinary real enclosure. Finiteness is an explicit
part of IEEETensorEnclosed, so this theorem never assigns a real meaning to NaN or infinity.
Pointwise absolute error between a real specification tensor and an executable binary32 tensor. The shape index is shared, so no runtime shape cast is hidden in the relation.
Instances For
Width of a finite executable interval, interpreted in the reals.
Instances For
A valid interval has nonnegative real width.
Two tensors enclosed by the same interval differ entrywise by at most its width.
This is the elementary bridge from range analysis to approximation analysis. It is deliberately
pointwise; a later norm theorem can package the same statement as an L∞ bound without changing
the checker or its certificate format.
A successful executable range check and a real enclosure proof yield a concrete pointwise error bound. This theorem is the tensor-level core used by graph-wide numerical certificates.
Check source ranges once, rejecting malformed intervals and duplicate node ids.
Instances For
Find the checked assumption for a source node.
Instances For
Whether a graph node obtains its enclosure directly from a certificate source assumption.
Instances For
Reject source assumptions that do not name a source-like node in the checked graph.
Unused assumptions do not make interval propagation unsound, but they make artifacts ambiguous: an exporter may have attached a valid range to the wrong node id without noticing. Requiring every row to be consumed gives source arrays one canonical interpretation and catches that error before range propagation begins.