精度保証付き数値計算

精度保証付き数値計算山本哲朗によって発案された用語である（せいどほしょうつきすうちけいさん、Validated Numerics, Rigorous Computation, Reliable Computation, Verified Computation, Numerical Verification, ）とは数学的に厳密な誤差（前進誤差、後退誤差、丸め誤差、打切り誤差、離散化誤差）の評価を伴う数値計算のことであり、数値解析の一分野である。演算では区間演算を使用し、結果はすべて区間で出力する。精度保証付き数値計算はウォリック・タッカーによって14番目のスメイルの問題を解くのにも活用されており（を参照）、力学系の研究では重要なツールとして位置づけられているD. Michelucci (2000), "Reliable computations for dynamic systems". Proc. SCAN 2000 / Interval 2000 — 9th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic, and Validated Numerics。

精度保証付き数値計算の必要性 精度保証付き数値計算ではない通常の数値計算だと誤差によって不都合な事象が生じてしまう。いくつかのその例を挙げる。 Rumpの例題 1980年代にRumpは次のような例を提示した（を参照）。

という関数を考え、この関数にという値を与えて数値計算をしたときにどういう結果が得られるか実験した。計算機はIBMのメインフレームS/370を使用して、単精度、倍精度、拡張精度で実験を行い、それぞれ 単精度（10進約8桁）: 倍精度（10進約17桁）: 拡張精度（10進約34桁）: の結果を得た。この結果を見ると、それぞれの精度に応じて途中の桁まで正しい値が得られているように思えたが、実は真の値はであり、真の値とは符号さえ合わないような結果が得られていた。これは、「ある演算精度で計算してそれよりも高い演算精度で計算したときに双方の結果が近ければある程度は結果の正しさを確認できる」とは限らないことを示す例であるLoh, E., & Walster, G. W. (2002). Rump's example revisited. Reliable Computing, 8(3), 245-248.。

幻影解 Breuer-Plum-McKennaはEmden方程式の境界値問題をスペクトル法によって離散化して解き、非対称な近似解が得られると報告した。しかしGidas-Ni-Nirenbergの理論的な解析手法によって非対称な解が存在しないことが証明されていた。つまりBreuer-Plum-McKennaが得た近似解は離散化誤差による幻影解だったのだ。これは珍しい例だが、微分方程式の解の存在を厳密に検討するには数値解法によって得られた近似解を検証しなければいけないことが分かる。

商用ソフトウェアの限界 ローレンツ方程式を精度保証付き数値計算とMATLABのode45（ODEソルバ）において最高精度を指定した場合で比較を行うと、ある程度時刻が進むと得られる解が違ってくるという実験例がある精度保証付き数値計算の必要性。

数値計算の誤差による事故 数値計算の誤差によって生じた事故として次の3つが挙げられる。 湾岸戦争でのミサイル迎撃失敗（1991年） アリアン5ロケットの発射失敗（1996年） 選挙結果の間違いRounding error changes Parliament makeup

主な研究分野 精度保証付き数値計算は主に以下の分野に分かれて研究がなされている大石進一：「精度保証付き数値計算」、コロナ社、（1999年）。 数値線形代数 (en) における精度保証（行列積、連立一次方程式、固有値問題を扱う） 初等関数、特殊関数の精度保証 ガンマ関数Yamanaka, N., Okayama, T., & Oishi, S. I. (2015, November). Verified Error Bounds for the Real Gamma Function Using Double Exponential Formula over Semi-infinite Interval. In International Conference on Mathematical Aspects of Computer and Information Sciences (pp. 224-228). Springer, Cham.Rump, S. M. (2014). Verified sharp bounds for the real gamma function over the entire floating-point range. Nonlinear Theory and Its Applications, IEICE, 5(3), 339-348. ベッセル関数大石進一(2008): 電子情報通信学会技術研究報告. NLP, 非線形問題, 108, 55-57.N. Yamamoto and N. Matsuda (2005): Trans. Jap. Soc. Indust. Appl. Math., 15, 347-359. 楕円関数Johansson, F. (2019). Numerical Evaluation of Elliptic Functions, Elliptic Integrals and Modular Forms. In Elliptic Integrals, Elliptic Functions and Modular Forms in Quantum Field Theory (pp. 269-293). Springer, Cham. 超幾何級数Johansson, F. (2019). Computing Hypergeometric Functions Rigorously. ACM Transactions on Mathematical Software (TOMS), 45(3), 30. フルヴィッツのゼータ函数Johansson, F. (2015). Rigorous high-precision computation of the Hurwitz zeta function and its derivatives. Numerical Algorithms, 69(2), 253-270. 数値積分の精度保証Johansson, F. (2017). Arb: efficient arbitrary-precision midpoint-radius interval arithmetic. IEEE Transactions on Computers, 66(8), 1281-1292.Johansson, F. (2018, July). Numerical integration in arbitrary-precision ball arithmetic. In International Congress on Mathematical Software (pp. 255-263). Springer, Cham.Johansson, F., & Mezzarobba, M. (2018). Fast and Rigorous Arbitrary-Precision Computation of Gauss--Legendre Quadrature Nodes and Weights. :en:SIAM Journal on Scientific Computing, 40(6), C726-C747. （ガウス求積、二重指数関数型数値積分公式などの数値積分公式の誤差評価を行う） 非線形方程式の精度保証付き数値解法（Newton-Kantorovichの定理Zeidler, E., Nonlinear Functional Analysis and Its Applications I-V. :en:Springer Science & Business Media.杉原正顯, & 室田一雄. (1994). 数値計算法の数理. 岩波書店.、Krawczyk法、区間ニュートン法、Durand-Kerner-Aberth法に関する研究が含まれる） ODE・PDEの精度保証付き数値解法（PDEでは有限要素法、関数解析の知識を駆使する中尾充宏, & 山本野人. (1998). 精度保証付き数値計算 チュートリアル: 応用数理最前線.中尾充宏, & 渡部善隆. (2011). 実例で学ぶ精度保証付き数値計算, サイエンス社.Xuefeng Liu: Guaranteed Computational Methods for Self-Adjoint Differential Eigenvalue Problems, Springer, eISBN978-981-97-3577-8（2024).） 積分方程式の精度保証付き数値解法 線形計画法の精度保証Oishi, S., & Tanabe, K. (2009). Numerical Inclusion of Optimum Point for Linear Programming. JSIAM Letters, 1, 5-8. 計算幾何学における精度保証 HPC環境における精度保証

主な精度保証付き数値計算ライブラリ INTLAB: MATLAB/GNU Octaveを使用するライブラリであるS.M. Rump: INTLAB - INTerval LABoratory. In Tibor Csendes, editor, Developments in Reliable Computing, pages 77-104. Kluwer Academic Publishers, Dordrecht, 1999.。 VERSOFT (MATLAB/INTLABで開発されたライブラリ)Rohn, J. (2009). VERSOFT: verification software in MATLAB/INTLAB. INTSOLVER (大域最適化問題を解くためのライブラリ、INTLABを使用して開発された)Montanher, T. M. (2009). Intsolver: An interval based toolbox for global optimization. Version 1.0. kv (C++によるライブラリである)Overview of kv – a C++ library for verified numerical computation, Masahide Kashiwagi, SCAN 2018.

Arb C言語によるライブラリであり、様々な特殊関数の精度保証に対応しているJohansson, F. (2013). Arb: a C library for ball arithmetic. ACM Comm. Computer Algebra, 47(3/4), 166-169.。

(Juliaによるライブラリ)Sanders, D. P., Benet, L., & Kryukov, N. (2016). The julia package ValidatedNumerics. jl and its application to the rigorous characterization of open billiard models. SCAN 2016, 124.ValidatedNumerics.jl: a new framework in Julia, David P. Sanders and Luis Benet, SCAN 2018.

その他、様々なライブラリが開発されているInterval and Verified Software。

関連する研究集会 日本数学会・応用数学分科会 日本応用数理学会・計算の品質研究部会 日本シミュレーション学会・精度保証付シミュレーション技術研究委員会 数値解析シンポジウム (NAS) International Symposium on Scientific Computing, Computer Arithmetics and Validated Numerics (SCAN)

関連項目 浮動小数点数 数値計算における誤差解析 誤差#計算誤差の種類 任意精度演算 関連分野 計算機援用証明 区間演算 アフィン演算 自動微分 数値積分 数値線形代数

研究者 日本 占部実 (ニュートン法に対する収束定理・誤差評価で知られる) 伊理正夫（日本応用数理学会・計算の品質研究部会の初代主査） 大石進一（精度保証付き数値計算の研究者） 海外 ゲッツ・アールフェルト ウルリヒ・クリッシュ ウォリック・タッカー(精度保証付き数値計算について著書がある) :en:Vladik Kreinovich

定理 ニュートン＝カントロビッチの定理 ゲルシュゴリンの定理

出典

参考文献 洋書

Tucker, W. (2011). Validated Numerics: A Short Introduction to Rigorous Computations. :en:Princeton University Press. Moore, R. E., Kearfott, R. B., & Cloud, M. J. (2009). Introduction to Interval Analysis. SIAM. （区間演算に詳しい）

Rump, S. M. (2010). Verification methods: Rigorous results using floating-point arithmetic. :en:Acta Numerica, 19, 287-449. 和書 大石進一 ：「非線形解析入門」、コロナ社（1997年4月）、ISBN 978-4-339-02600-9。（PDEの精度保証付き数値解法で用いる関数解析の知識を詳述している） 中尾充宏、山本野人：「精度保証付き数値計算：コンピュータによる無限への挑戦」、技術評論社 (1998年6月15日)、ISBN 4-535-78258-X。 大石進一：「数値計算」、裳華房 (1999年3月25日)、ISBN 4-7853-1514-8。 大石進一：「精度保証付き数値計算」、コロナ社 (2000年1月5日)、ISBN 4-339-02605-0。 中尾充宏、渡部善隆：「実例で学ぶ精度保証付き数値計算」、サイエンス社（SGCライブラリ 85）(2011年10月25日)。

外部リンク

INTLAB 精度保証付き数値計算学の確立 無限次元精度保証付き数値計算の新展開に向けての基礎的研究

解説記事 精度保証ノート

Reproducing Rump's example