Checked Float32 Discounted Returns #

This module contains the value-learning recurrences that need explicit finite-intermediate checks: discounted backups and fixed-horizon discounted returns. The public names stay in Runtime.RL.Numerics.Float32; this file only separates the implementation so the runtime tree is easier to audit.

Reference: Sutton and Barto, Reinforcement Learning: An Introduction.

Checked RL core transforms (configured binary32) #

source

def Runtime.RL.Numerics.Float32.requireFinite (label : String) (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) requireFinite._proof_1 requireFinite._proof_2 requireFinite._proof_3 requireFinite._proof_4) :

Except String Unit

Require that an Binary 8 23 value is finite, producing a tagged error on failure.

Instances For

Checked configured binary32 primitives #

The checked RL helpers below are intentionally written in terms of a few small “checked primitive” combinators (checkedAdd, checkedMul, …). Larger routines (GAE, PPO objectives, …) remain readable while still producing precise error locations when non-finite values occur.

Exponential uses FloatLib's configured deterministic approximation. Its check rejects nonfinite results; it does not certify correct rounding or a real-error bound.

source

Checked version of the one-step discounted backup

reward + γ * (1-done) * bootstrap

specialized to Binary 8 23.

The runtime return type is Except String … so training code can choose to:

fail fast, or
fall back to a safer scalar backend (interval/oracle), or
log and skip a bad sample.

Instances For

Checked preconditions → proof hypotheses #

The NN/Proofs/RL/Floats/* bridge theorems for Binary 8 23 are usually stated with explicit isFinite … = true hypotheses for each intermediate.

The lemma below is the glue between runtime safety checks and those proof hypotheses:

If the checked routine returns .ok, then all the finiteness side-conditions needed by the semantic bridge theorems hold automatically.

source

theorem Runtime.RL.Numerics.Float32.discountedBackup_eq_ok (reward gamma bootstrap : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) requireFinite._proof_1 requireFinite._proof_2 requireFinite._proof_3 requireFinite._proof_4) (done : Bool) (out : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) requireFinite._proof_1 requireFinite._proof_2 requireFinite._proof_3 requireFinite._proof_4) (h : discountedBackupChecked reward gamma bootstrap done = Except.ok out) :

FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)) = true ∧ FloatLib.Floats.ExecFloat.Binary.isFinite ((FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)).mul bootstrap) = true ∧ FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add reward ((FloatLib.Floats.ExecFloat.mul gamma (Spec.RL.continueMask done)).mul bootstrap)) = true ∧ out = Spec.RL.discountedBackup reward gamma bootstrap done

If discountedBackupChecked returns .ok out, then:

every configured binary32 intermediate used by the refinement theorem is finite, and
out agrees with the spec-layer discountedBackup formula.

source

Except String (TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) requireFinite._proof_1 requireFinite._proof_2 requireFinite._proof_3 requireFinite._proof_4) [n])

Checked fixed-horizon discounted returns (no done flags), specialized to Binary 8 23.

This is the checked/finite counterpart to Runtime.RL.Core.discountedReturns.

Instances For

TorchLean API

NN.Runtime.RL.Numerics.Float32.Returns

Checked Float32 Discounted Returns #

Checked RL core transforms (configured binary32) #

Checked configured binary32 primitives #

Checked preconditions → proof hypotheses #