TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.MLTheory.CROWN.Extras.BoundOpsIEEE32Exec

BoundOps instance for ExecFloat.Binary 8 23 #

This instance plugs FloatLib's configured binary32 directed-rounding primitives into the IBP/CROWN endpoint propagation code.

With this, IBP code written in terms of BoundOps can use α := ExecFloat.Binary 8 23 to get float32-grid, outward-rounded interval propagation (subject to the usual finiteness preconditions).

source
@[instance_reducible]
instance NN.MLTheory.CROWN.instBoundOpsBinaryOfNatNatIeeeDefaultBias :
BoundOps (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) instBoundOpsBinaryOfNatNatIeeeDefaultBias._proof_1 instBoundOpsBinaryOfNatNatIeeeDefaultBias._proof_2 instBoundOpsBinaryOfNatNatIeeeDefaultBias._proof_3 instBoundOpsBinaryOfNatNatIeeeDefaultBias._proof_4)

BoundOps for ExecFloat.Binary 8 23, using the executable directed-rounding endpoint primitives.

source
@[instance_reducible]
instance NN.MLTheory.CROWN.instNonlinearBoundOpsBinaryOfNatNatIeeeDefaultBias :
NonlinearBoundOps (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) instBoundOpsBinaryOfNatNatIeeeDefaultBias._proof_1 instBoundOpsBinaryOfNatNatIeeeDefaultBias._proof_2 instBoundOpsBinaryOfNatNatIeeeDefaultBias._proof_3 instBoundOpsBinaryOfNatNatIeeeDefaultBias._proof_4)

Nonlinear enclosures backed by the proved directed binary32 division and square-root operations.

FloatLib's ExecFloat.Binary.exp is a deterministic approximation, not yet a proved enclosure of real exponentiation, so exponential and logarithmic transfers are intentionally absent.