Configured binary scalars for TorchLean specifications #
FloatLib owns the binary formats, representations, arithmetic, and elementary-function class.
This module supplies the Context dictionary used by TorchLean's tensors and models. Select a
format directly with FloatLib.Floats.ExecFloat.Binary, including formats wider than binary64.
The descriptor carries proofs that the exponent width is at least two, the fraction width and bias
are positive, and the bias is at most the encoding's largest finite exponent field. Concrete valid
widths discharge these requirements automatically; parameterized formats must provide the proofs.
Integer and rational casts round their exact value once in the destination format. The pow
field lifts FloatLib's model operation without converting through a native Float. FloatLib's
transcendentals are deterministic approximations; this dictionary adds no general accuracy or
correct-rounding theorem for them.
Dimension roots use the ordinary cast-then-root schedule unless the count overflows. That branch rounds the exact rational square root directly, so a representable root is not lost with the cast.
The operations in this instance use FloatLib's CPU software arithmetic. Custom computations
can select configured GPU arithmetic through NN.Kernel; this dictionary alone supplies
neither that execution path nor a LawfulContext or trainer/checkpoint encoding.
The pointwise operators of Spec.PointwiseOp use FloatLib's correctly rounded division and
square root, its integral rounding and IEEE remainder, its power function and its tanh.
Flooring division and the tanh GELU follow PyTorch's CPU kernels operation by operation, the GELU
as they run at the AVX2 and AVX-512 capability levels, measured on x86-64. FloatLib has no error
function, so erf and the exact GELU are unsupported here.
Compare configured scalar encodings in saved reverse programs. Numerical equality is not enough here: signed zeros and NaNs must keep their distinct storage representations.
A count whose cast overflows can still have a representable square root.
Keep the ordinary cast-then-root schedule otherwise. FloatLib rounds the exact rational root directly in the exceptional branch, including custom exponent biases and finite encodings.
Instances For
FloatLib's power function, the dictionary's pow.
Instances For
C's fmod: the remainder of truncating division, with the sign of the dividend.
The IEEE remainder rounds the quotient to the nearest integer instead. Both remainders are exact.
When their signs differ, fmod is the IEEE remainder plus the divisor's magnitude with the
dividend's sign; that sum is the exact remainder, so the rounded addition returns it unchanged.
Instances For
PyTorch's flooring division, c10::div_floor_floating, one FloatLib operation per step.
A zero divisor returns the IEEE quotient. Otherwise the exact remainder corrects the rounded
quotient, as Python's // does; 1 // 0.1 is 9, while the floor of the rounded quotient
1 / 0.1 = 10 would be 10. A zero result takes the sign of the IEEE quotient.
Instances For
PyTorch's tanh GELU, 0.5 * x * (1 + tanh (β * (x + κ * (x * x * x)))), one FloatLib operation
per step in the order of PyTorch's kernel, with x + κ x³ rounded once as a fused multiply-add.
One PyTorch binary runs each CPU kernel at the DEFAULT, AVX2 or AVX-512 capability level, chosen at
run time from the processor or ATEN_CPU_CAPABILITY. On x86-64 (a Xeon Platinum 8275CL), both of
its loops compute that sum so at the AVX2 and AVX-512 levels, and round κ x³ and the sum
separately at DEFAULT. PyTorch on aarch64, on Apple processors and on CUDA was not measured.
β and κ are PyTorch's binary64 constants kGeluBeta and kGeluKappa, the binary64 values
nearest √(2 / π) and 0.044715, each rounded once to the format as the kernel's conversion to its
computation type does.
Instances For
FloatLib meanings of the pointwise operators that depend on the scalar type.
Instances For
Use any configured binary format as a tensor/model scalar.
The default safeguard is 1e-6, rounded once. If a coarse format rounds it to zero, use its
smallest positive subnormal (encoding word 1) instead. For example, exponent width 3 and
fraction width 2 use 1/16; the minimal default-bias format with widths 2 and 1 uses 1/2.
Such a large safeguard can materially change a guarded formula. This is a nonzero default, not
machine epsilon or an error bound; callers should choose tolerances for their format and problem.