Anima 发布 FloatLib:Lean 验证的高精度浮点运算库

AnimaAnandkumar · x · 2026-09-21

Caltech 教授 Anima Anandkumar 团队发布 FloatLib,一个用 Lean 形式化验证的任意精度浮点运算库,目标是让「可证明正确」与「高效执行」兼得,服务于可信机器学习与科学计算——这些场景中舍入、溢出与累加误差可能改变结果。特性:支持 IEEE 二进制/十进制、任意宽度 posits、P3109 及小型 ML 格式,可自定义格式与舍入规则;每个认证软件后端附带 Lean 正确性证明(含带符号零与异常值);性能优化包括 tiny 格式查找表、机器字 kernel、宽位宽的 limb 算法。