boundlab.polysp.softmax#
Softmax over sparse polynomials, tightened by the simplex constraint.
Softmax outputs satisfy \(\sum_i \sigma_i = 1\) exactly, but the
propagated abstract value only satisfies it approximately. The residual
polynomial \(E = \big(\sum_i \sigma_i\big) - 1\) is therefore known to
be zero, so any multiple of it may be added to the output without changing
the represented function. softmax_opt() exploits this: it picks, per
output element, the linear combination of the constraint equations that
minimizes the resulting interval width (least squares on the error rows,
rescaled by the exact L1-optimal step), and adds it. A sound rescaling of
the error symbols (restrict_errors(), justified by the bounds from
bounding_error_terms()) first shrinks symbols the constraint pins down.
Functions
Add the optimal multiple of the zero-valued constraint \(\sum_i \sigma_i - 1 = 0\) to each element. |
|
Given a set of equations, return the estimated bound [c - hw, c + hw] for each error term. |
|
Per-column step |
|
Return updated generator with old_error = hw * new_error range. |
|
Add the optimal multiple of the zero-valued constraint \(\sum_i \sigma_i - 1 = 0\) to each element. |
Classes
Run the domain's softmax decomposition, then apply the sum-to-one constraint optimization ( |