NF Elementwise Bounds: Safe Division and Sigmoid #
Forward error bounds for clamped division safeDiv, ordinary division on a certified positive
denominator domain (divPosErrorBound), and the elementwise sigmoid.
The division budget divPosErrorBound η epsx epsy xhat yhat requires |ŷ - y| ≤ epsy and a
positive lower bound η ≤ y. Its conditioning factor is 1 / (η - epsy).
Sigmoid chooses between 1 / (1 + exp (-x)) and exp x / (1 + exp x). Each sequence has its own
numerator and denominator budget, assembled from the operations it actually evaluates. The branch
is selected by the rounded input, while both real expressions equal the same logistic function.
The input approximation may therefore cross zero without requiring a separate sign hypothesis.
When a denominator budget is below 1, the division certificate applies; otherwise the bound is
|σ̂| + 1, using the range of the exact sigmoid.
The reciprocalSigmoid declarations retain the first sequence and its half-margin regressions.
They describe that sequence even on negative inputs. sigmoidBoundScalar and
approxTensor_sigmoid_spec describe the branch-selected public operation.
Spec-side safe division with a clamped denominator.
Instances For
Runtime implementation of safeDiv as a single rounded primitive.
Instances For
Forward approximation bound for safeDiv in NF.
safeDiv ε x y = x / max y ε clamps the denominator away from 0. For ε > 0, this yields an
unconditional bound with explicit (1/ε) and (1/ε^2) sensitivity terms plus one rounding-ULP
term.
Error budget for division with exact denominator lower bound η and denominator approximation
error epsy. The caller must separately establish epsy < η; otherwise the rounded denominator
may cross zero and no finite perturbation bound follows.
Instances For
Forward error for ordinary division when the exact denominator stays positively separated from zero and its approximation budget is smaller than that separation.
The effective runtime margin is η - epsy: from η ≤ y and |ŷ - y| ≤ epsy we obtain
η - epsy ≤ ŷ. The result is proved through the shared clamped-division analysis, after showing
that neither the exact nor rounded denominator activates the clamp. This is the form needed by
stable softmax and normalization, where a mathematical lower bound on a reduction must survive
rounding before division is allowed.
Under the half-margin certificate epsy ≤ η / 2, the division budget is controlled by the
numerator error, the denominator error, and one output rounding, with constants that do not depend
on the format. This is the shared regression lemma for sigmoid, logistic, and mean bounds.
Per-entry bound tensor for safeDiv.
This is the elementwise lifting of approx_safeDiv_nf's bound (with a max-clamped denominator).
Instances For
Per-entry budget for ordinary division on a certified positive denominator domain.
Unlike safeDivBoundTensor, this definition does not change the operation by clamping its
denominator. The accompanying theorem therefore requires epsy < η, ensuring that an exact lower
bound η ≤ y remains positive after the denominator is rounded.
Instances For
Shape-generic forward error for ordinary elementwise division by positive denominators.
The domain condition is stated over the exact tensor, while epsy < η certifies that every
runtime denominator remains separated from zero. This is the reusable division rule for softmax,
normalization, and positive quantization scales; callers do not need a rank-specific theorem.
approxTensor bound for safeDiv lifted to arbitrary tensor shapes.
This is the tensor-level wrapper around approx_safeDiv_nf, built via
approxTensor_map2_spec_of_scalar_bound.
The rounded constant 1 : NF is within oneEps of the real 1.
oneEps is a half ulp, hence nonnegative.
expErrorBound is nonnegative whenever the propagated input error is.
Sigmoid evaluated as 1 / (1 + exp (-x)) for every input.
This sequence is retained for its NF rounding certificate. The public sigmoid chooses another sequence on nonpositive inputs, so the two rounded results need not agree. Both approximate the same real logistic function.
Instances For
Rounded denominator of reciprocalSigmoidR.
Instances For
Error budget of the rounded sigmoid denominator 1 + exp(-x) given input error eps.
The summands pay for the rounded constant 1, the rounded exponential of the rounded negation
(whose input error is eps plus one negation rounding), and the final addition rounding.
Instances For
reciprocalSigmoidDenomError is nonnegative for nonnegative input error.
Scalar forward bound for reciprocalSigmoidR at input error eps.
sigmoid(x) = 1 / (1 + exp(-x)) has exact denominator at least 1. When the rounded denominator
budget reciprocalSigmoidDenomError eps xR is below 1, the rounded denominator stays positive.
The bound then uses divPosErrorBound with margin 1 - reciprocalSigmoidDenomError.
Otherwise the certificate fails and the bound falls back to |σ̂| + 1, which is always valid
because the exact sigmoid lies in (0, 1].
Instances For
Per-entry bound tensor for reciprocalSigmoidR; eps is the per-entry input error.
Instances For
The reciprocal sequence's denominator approximates 1 + exp(-x) within its composed budget.
With denominator error at most 1/2, the reciprocal sequence's bound is linear in the
rounding budget of the constant 1, the denominator error, and one output rounding.
In particular it tends to the output half ulp as the format is refined.
For a format whose half ulp at 1 is at most 1/16, whose output half ulp is at most 1/4,
and whose rounded denominator error is at most 1/16, the reciprocal sequence's bound is at
most 1.
approxTensor bound for the reciprocal sigmoid sequence at arbitrary tensor shapes.
The scalar certificate for reciprocalSigmoidBoundScalar lifts componentwise through linfNorm.
There is no side condition: the per-entry bound already switches to its fallback branch when the
denominator certificate fails.
The negative-input sigmoid sequence, with a shared rounded exponential in the numerator and denominator. It is defined for every NF input so its certificate can be stated independently of the comparison that selects the public sigmoid branch.
Instances For
Rounded denominator of expRatioSigmoidR.
Instances For
Error in the negative-input sequence's denominator. The exponential has input error eps;
the other two terms account for representing 1 and adding it to that exponential.
Instances For
Forward-error budget for the exponential-ratio sequence. Both occurrences of exp x share
the same rounded value, but the division estimate only needs separate numerator and denominator
error bounds. The exact denominator is at least 1.
Instances For
The exponential-ratio denominator approximates 1 + exp x within its composed budget.
The exponential-ratio sequence approximates the real sigmoid, with no sign or format restriction beyond the NF rounding model.
NF error budget for the public sigmoid, selecting the certificate for its actual evaluation
branch. The comparison is made on xR, exactly as it is in Activation.Math.sigmoidSpec.
Instances For
Per-entry forward-error budgets for the public sigmoid.
Instances For
Scalar approximation certificate for the branch-stable sigmoid.
Either rounded branch approximates the same real function, so the proof does not assume that the approximate input and the exact input have the same sign.
Shape-generic approximation certificate for the public sigmoid. Its per-entry budgets cover both selected evaluation branches and use the range fallback only if the corresponding denominator certificate fails.