Semantics, Operations, and Properties of P3109 Floating-Point Formats in Lean (github.com)

The FLoPS framework has formalized the upcoming IEEE P3109 standard for low-precision floating-point arithmetic in Lean, a proof assistant. This standard is poised to significantly impact the AI and machine learning community by providing a flexible parametric framework that accommodates variations in bitwidth, precision, signedness, and domain. This flexibility creates a vast range of potential formats, including some with minimal precision, enabling new features like stochastic rounding and saturation arithmetic. The formalization tackles a verification gap that arises from these innovations, ensuring the reliability of this critical standard. Key contributions of the FLoPS framework include a machine-checked specification that allows for deep analysis and verification of foundational properties related to the P3109 standard. Notably, the research identifies that the FastTwoSum algorithm can compute exact overflow errors under saturation for any rounding mode, while revealing limitations of the ExtractScalar algorithm in low precision formats. By establishing this formal verification methodology, the work not only provides a rigorous basis for understanding P3109 but also lays the groundwork for ensuring the accuracy and reliability of future numerical software aimed at low-precision floating-point operations in machine learning applications.