FLoPS：P3109浮点表示的语义、操作与性质
FLoPS: Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean
AI总结：
本文研究P3109低精度浮点运算标准的语义、操作及性质，通过Lean形式化方法构建了该标准的完整形式化模型，验证了FastTwoSum在饱和运算下的新特性，并揭示了ExtractScalar算法在单比特精度格式中的失效问题。
摘要：
即将到来的IEEE-P3109标准低精度浮点运算标准可能成为未来机器学习硬件和软件的基础。与IEEE-754不同，P3109引入了一个由位宽、精度、符号性和领域定义的参数框架。这种灵活性导致了庞大的组合格式空间——某些格式的精度仅有一位——以及新的特性如随机舍入和饱和运算。这些偏差创造了一个独特的验证缺口，本文旨在解决。本文提出了FLoPS，即P3109标准在Lean中的形式化，这是P3109在Lean中的完整形式化模型。我们的工作为该标准提供了严谨的机器验证规范，有助于深入分析该标准。我们通过验证基础属性并分析P3109环境中的关键算法来展示模型的实用性。具体而言，我们揭示了FastTwoSum在使用任何舍入模式下计算精确的“溢出错误”这一新特性，而之前建立的ExtractScalar算法属性在单比特精度格式中失效。本文的工作为P3109的推理提供了验证基础，并使未来数值软件的形式验证成为可能。我们的Lean开发是开源且公开可用的。
英文摘要：
The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike IEEE-754, P3109 introduces a parametric framework defined by bitwidth, precision, signedness, and domain. This flexibility results in a vast combinatorial space of formats -- some with as little as one bit of precision -- alongside novel features such as stochastic rounding and saturation arithmetic. These deviations create a unique verification gap that this paper intends to address. This paper presents FLoPS, Formalization in Lean of the P3109 Standard, which is a comprehensive formal model of P3109 in Lean. Our work serves as a rigorous, machine-checked specification that facilitates deep analysis of the standard. We demonstrate the model's utility by verifying foundational properties and analyzing key algorithms within the P3109 context. Specifically, we reveal that FastTwoSum exhibits a novel property of computing exact "overflow error" under saturation using any rounding mode, whereas previously established properties of the ExtractScalar algorithm fail for formats with one bit of precision. This work provides a verified foundation for reasoning about P3109 and enables formal verification of future numerical software. Our Lean development is open source and publicly available.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
