NF Elementwise Bounds: Scalar Logistic Node #
This file bounds the elementwise NF graph node that is registered under the public name
softmax. Despite the name, the node computes the scalar logistic sigmoid in its
exp(x) / (exp(x) + 1) form, Activation.Math.logisticSpec, entrywise. It is not axis softmax;
that operation lives in NN.Proofs.RuntimeApprox.NF.SoftmaxAxis. The public names
softmaxBoundScalar, softmaxBoundTensor, and approxTensor_softmax_spec are kept because the
NF forward and backward graph nodes refer to them; the internal names use logistic.
The bound is derived from the conditioned division budget divPosErrorBound. The exact denominator
exp(x) + 1 is at least 1; the rounded denominator error logisticDenomError is the numerator
exponential budget plus the rounded constant 1 plus one addition rounding. When that error is
below 1 the bound is the conditioned division budget; otherwise it falls back to |ℓ̂| + 1,
which is always valid because the exact logistic lies in (0, 1). The regression theorems
softmax_bound_scalar_le_of_denom_le_half and softmax_bound_scalar_le_one show the certified
branch is linear in the rounding budgets and stays below 1 for modest formats on the
nonpositive half line.
Runtime numerator exp x of the rounded logistic node.
Instances For
Runtime denominator exp x + 1 of the rounded logistic node, exactly as it appears inside
Activation.Math.logisticSpec at the NF backend.
Instances For
Numerator error budget of the logistic node: one rounded exponential at input error eps.
Instances For
Denominator error budget of the logistic node: the numerator budget, the rounded constant 1,
and one addition rounding.
Instances For
logisticNumError is nonnegative for nonnegative input error.
logisticDenomError is nonnegative for nonnegative input error.
Scalar forward bound for the scalar logistic NF node (public name softmax) at input error eps.
The node computes exp(x) / (exp(x) + 1), whose exact denominator is at least 1. When the
rounded denominator budget logisticDenomError eps xR is below 1, the bound is the conditioned
division budget divPosErrorBound with margin 1 - logisticDenomError. Otherwise the certificate
fails and the bound falls back to |ℓ̂| + 1, valid because the exact logistic lies in (0, 1).
Instances For
Per-entry bound tensor for the scalar logistic NF node; eps is the per-entry input error.
Instances For
The rounded logistic denominator approximates exp x + 1 within logisticDenomError.
Regression: under the half-margin certificate logisticDenomError eps xR ≤ 1 / 2, the logistic
bound is linear in the numerator budget, the denominator budget, and one output rounding.
Regression: when the rounded numerator exp(x̂) is at most 1 (the nonpositive half line),
the numerator and denominator budgets are at most 1/16, and the output half ulp is at most 1/4,
the logistic bound is at most 1.
approxTensor bound for the scalar logistic NF node lifted to arbitrary tensor shapes.
This is the tensor-level wrapper around the scalar certificate for softmaxBoundScalar, lifted
componentwise through linfNorm. It has no side condition: the per-entry bound already switches to
its fallback branch when the denominator certificate fails.