AI 中文总结
FloatLib是Lean 4中首个统一多种浮点格式的验证库，通过认证后端和形式化证明确保正确性，性能最高比FLoPS快1.46倍、比Universal快116倍，并通过超1亿次测试验证。
AI 中文摘要
我们提出了FloatLib，一个在Lean 4中验证的任意精度浮点运算库，它结合了广泛的格式覆盖、机器检查的正确性和高效的认证执行。据我们所知，FloatLib是第一个将IEEE二进制和十进制运算、任意宽度的posits、P3109以及用户自定义格式和舍入规则统一在可互换的认证软件后端之后的Lean库。每个认证后端都被证明等同于一个完整的编码规范，保留了有符号零和异常值，而数值定理将执行与真实舍入、误差界和精确性联系起来。FloatLib将针对小格式的详尽认证表与基于guard-and-sticky不变量和独立检查的商候选的验证字和肢体内核相结合。其posit开发还额外证明了标准舍入阈值和任意宽度容量内的精确quire累加。在匹配的工作负载中，FloatLib相对于FLoPS实现了高达1.46倍的加速，相对于Universal实现了116倍的加速，而在某些领域（如针对MPFR的二进制运算）则较慢。独立的符合性测试包括超过1.02亿次TestFloat评估，在测试关系下零差异。我们将该库、证明、基准、评估数据和指南作为开源发布。
英文摘要
We present FloatLib, a verified arbitrary-precision floating-point arithmetic library in Lean 4 that combines broad format coverage, machine-checked correctness, and efficient certified execution. To our knowledge, FloatLib is the first Lean library to unify IEEE binary and decimal arithmetic, arbitrary-width posits, P3109, and user-defined formats and rounding rules behind interchangeable certified software backends. Every certified backend is proved equal to a complete encoded specification, preserving signed zeros and exceptional values, while numerical theorems connect execution to real rounding, error bounds, and exactness. FloatLib combines exhaustive certified tables for small formats with verified word and limb kernels based on guard-and-sticky invariants and independently checked quotient candidates. Its posit development additionally proves standard rounding thresholds and exact quire accumulation within capacity for arbitrary widths. Across matched workloads, FloatLib achieves speedups of up to 1.46x over FLoPS and 116x over Universal, while remaining slower in some regimes such as binary arithmetic against MPFR. Independent conformance testing includes more than 102 million TestFloat evaluations with zero differences under the tested relation. We release the library, proofs, benchmarks, evaluation data, and guide as open source.
Comments30 pages, 7 figures, 6 tables. Software and evaluation artifacts available at https://github.com/lean-dojo/FloatLib
