多様な浮動小数点計算をLeanで検証するFloatLib
FloatLib: Verified Floating-Point Arithmetic in Lean
この論文をやさしく読む
ひとことで言うと
さまざまな数値形式の浮動小数点演算を、仕様通り動くことの機械的な証明とともに提供するライブラリです。
何に役立つ？
考えられる用途は、計算の丸めや例外値の扱いまで正確さが必要な数値ソフトウェアの基盤です。利用者定義の形式や丸め規則も同じ枠組みで扱えます。
この研究の面白いところ
単なるテストだけでなく、実装と完全な仕様の一致を証明し、数値誤差の定理にもつなげています。小形式の表と検証済み計算カーネルを使い分け、実行効率も追求しています。
どこまで分かった？
最大116倍という速度差は比較対象と処理条件に依存し、MPFRより遅い条件も明記されています。TestFloatで差異ゼロなのは試験した比較関係の下での結果です。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
Lean 4で検証された任意精度浮動小数点演算ライブラリFloatLibを提示する。幅広い形式への対応、機械で検査された正しさ、効率的で認証された実行を組み合わせる。著者らの知る限り、FloatLibは、IEEEの2進・10進演算、任意ビット幅のposit、P3109、利用者定義の形式と丸め規則を、交換可能で認証済みのソフトウェアバックエンドの下に統合する初めてのLeanライブラリである。 認証されたすべてのバックエンドは、符号付きゼロと例外値を保持しつつ、完全に符号化された仕様と一致することが証明される。また、数値に関する定理が、実行を実数の丸め、誤差限界、厳密性と結びつける。FloatLibは、小さな形式向けの網羅的で認証された表と、ガードビット・スティッキービットの不変条件および独立に検査された商の候補に基づく、検証済みのワード単位・多倍長リム単位のカーネルを組み合わせる。positの実装ではさらに、標準的な丸めの閾値と、任意ビット幅に対して容量内で正確に動作するquire累積を証明する。 条件をそろえた処理負荷では、FloatLibはFLoPSに対して最大1.46倍、Universalに対して最大116倍の高速化を達成する。一方、MPFRとの2進演算の比較など、一部の条件では遅い。独立した適合性試験には1億200万回を超えるTestFloat評価が含まれ、試験した比較関係の下で差異はゼロだった。ライブラリ、証明、ベンチマーク、評価データ、ガイドをオープンソースとして公開する。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-16（UTC）
- 最新改訂
- 2026-09-16 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-16 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
著者のコメント
30 pages, 7 figures, 6 tables. Software and evaluation artifacts available at https://github.com/lean-dojo/FloatLib
arXiv ID: 2609.19352 ／ 要約の誤りについて