Float32 Interval Diagnostics for RL #
This module uses FloatLib's outward-rounded binary32 intervals for return, GAE, TD-residual, and PPO scalar formulas used by the checked binary32 runtime. These intervals are executable diagnostics: they do not replace the exact RL specs, but they flag overflow, invalid endpoints, and unstable recurrences in examples and regression tests.
References: IEEE 1788-2015 for interval arithmetic semantics; Sutton and Barto for return and TD recurrences; Schulman et al. for GAE and PPO.
Interval Enclosures (configured binary32 endpoint intervals) #
Outward-rounded interval enclosure for the one-step discounted backup:
reward + γ * (1-done) * bootstrap.
This is the interval analogue of discountedBackupChecked (but purely functional, and
returning an enclosure rather than failing).
Reference:
- Sutton and Barto, Reinforcement Learning: An Introduction (discounted backups / returns).
Instances For
Outward-rounded interval enclosure for the TD residual:
reward + γ * (1-done) * nextValue - value.
This is the interval analogue of tdResidualChecked.
Reference:
- Sutton and Barto, Reinforcement Learning: An Introduction (TD error / Bellman error).
Instances For
Outward-rounded interval enclosure for the PPO clipped surrogate objective from a precomputed ratio.
The clipping thresholds 1 - clipEps and 1 + clipEps are themselves outward-rounded intervals,
so the clipped ratio is enclosed even when the exact real threshold is not a binary32 value.
Clipping is monotone in the ratio and in both thresholds, so its range over the threshold
intervals is exact at the endpoints. The result is the hull of the enclosures of ratio * A and
clip ratio * A, which contains the minimum PPO takes. A NaN input yields whole.
Reference:
- Schulman et al., "Proximal Policy Optimization Algorithms" (2017): https://arxiv.org/abs/1707.06347
Instances For
Outward-rounded interval enclosure for fixed-horizon discounted returns.
If you pass point intervals at the leaves (Binary.Interval.point), the output is a conservative
enclosure for the exact real return recursion (interpreting leaves via Model.toReal after
decoding).
This is an executable diagnostic: you can run it alongside discountedReturnsChecked
to detect blow-ups (endpoints becoming ±Inf or Valid failing).
Reference:
- Sutton and Barto, Reinforcement Learning: An Introduction (returns / bootstrapping).
Instances For
Outward-rounded interval enclosure for fixed-horizon $\operatorname{GAE}(\lambda)$.
This is useful as a coarse numerical diagnostic alongside
generalizedAdvantageEstimationChecked.
Reference:
- Schulman et al., "High-Dimensional Continuous Control Using Generalized Advantage Estimation" (2015): https://arxiv.org/abs/1506.02438
Instances For
Executable check: every returns[i] lies inside intervals[i] in the configured scalar order.
This is an executable regression check for examples and tests; formal enclosure theorems live in
NN/Floats/Interval/*.