精度保証付き数値計算

精度保証付き数値計算^[1]（せいどほしょうつきすうちけいさん、Validated Numerics, Rigorous Computation, Reliable Computation, Verified Computation, Numerical Verification, 独: Zuverlässiges Rechnen）とは数学的に厳密な誤差（前進誤差、後退誤差、丸め誤差、打切り誤差、離散化誤差）の評価を伴う数値計算のことであり、数値解析の一分野である^[2]。演算では区間演算を使用し、結果はすべて区間で出力する。精度保証付き数値計算はウォリック・タッカーによって14番目のスメイルの問題を解くのにも活用されており（Tucker (1999)を参照）、力学系の研究では重要なツールとして位置づけられている^[3]^[4]^[5]^[6]。

→「数値解析」および「区間演算」も参照

精度保証付き数値計算の必要性

精度保証付き数値計算ではない通常の数値計算だと誤差によって不都合な事象が生じてしまう。いくつかのその例を挙げる。

Rumpの例題

1980年代にRumpは次のような例を提示した（Rump (1988)を参照）。

f(a,b)=333.75b^{6}+a^{2}(11a^{2}b^{2}-b^{6}-121b^{4}-2)+5.5b^{8}+{\frac {a}{2b}}

という関数を考え、この関数に $a=77617.0,b=33096.0$ という値を与えて数値計算をしたときにどういう結果が得られるか実験した。計算機はIBMのメインフレームS/370を使用して、単精度、倍精度、拡張精度で実験を行い、それぞれ

単精度（10進約8桁）: $f(a,b)\sim 1.172603...$
倍精度（10進約17桁）: $f(a,b)\sim 1.1726039400531...$
拡張精度（10進約34桁）: $f(a,b)\sim 1.172603940053178...$

の結果を得た。この結果を見ると、それぞれの精度に応じて途中の桁まで正しい値が得られているように思えたが、実は真の値は $f(a,b)=-0.82739605...$ であり、真の値とは符号さえ合わないような結果が得られていた。これは、「ある演算精度で計算してそれよりも高い演算精度で計算したときに双方の結果が近ければある程度は結果の正しさを確認できる」とは限らないことを示す例である^[2]^[7]。

幻影解

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

商用ソフトウェアの限界

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

数値計算の誤差による事故

数値計算の誤差によって生じた事故として次の3つが挙げられる。

湾岸戦争でのミサイル迎撃失敗（1991年）^[9]
アリアン5ロケットの発射失敗（1996年）^[10]
選挙結果の間違い^[11]

主な研究分野

精度保証付き数値計算は主に以下の分野に分かれて研究がなされている^[2]^[12]。

数値線形代数 (en) における精度保証（行列積、連立一次方程式、固有値問題を扱う^[13]）
初等関数、特殊関数の精度保証
数値積分の精度保証^[22]^[23]^[24]

（ガウス求積、二重指数関数型数値積分公式などの数値積分公式の誤差評価を行う）

非線形方程式の精度保証付き数値解法（Newton-Kantorovichの定理^[13]^[25]^[26]^[27]、Krawczyk法^[27]、区間ニュートン法^[26]^[27]、Durand-Kerner-Aberth法^[13]^[26]に関する研究が含まれる）
ODE・PDEの精度保証付き数値解法（PDEでは有限要素法、関数解析の知識を駆使する^[25]^[28]）
積分方程式の精度保証付き数値解法
線形計画法の精度保証^[29]
計算幾何学における精度保証^[30]
HPC環境における精度保証

→「数値線形代数」、「常微分方程式の数値解法」、「偏微分方程式の数値解法」、「数値積分」、「計算幾何学」、および「高性能計算」も参照

主な精度保証付き数値計算ライブラリ

INTLAB: MATLAB/GNU Octaveを使用するライブラリである^[31]。
- VERSOFT (MATLAB/INTLABで開発されたライブラリ)^[32]
- INTSOLVER (大域最適化問題を解くためのライブラリ、INTLABを使用して開発された)^[33]
kv (C++によるライブラリである)^[34]
- kv - GitHub
Arb C言語によるライブラリであり、様々な特殊関数の精度保証に対応している^[35]。
- arb - GitHub
JuliaIntervals - GitHub (Juliaによるライブラリ)^[36]^[37]

その他、様々なライブラリが開発されている^[38]^[39]。

^ 山本哲朗によって発案された用語である
^ ^a ^b ^c 大石、他 (2018)
^ 荒井迅「精度保証付き数値計算の力学系への応用について (力学系の研究 : トポロジーと計算機による新展開 RIMS研究集会報告集)」『数理解析研究所講究録』第1485号、京都大学数理解析研究所、2006年4月、1-13頁、CRID 1050001202109463040、hdl:2433/58149、ISSN 18802818、NAID 110004541092。
^ 荒井迅「精度保証付き数値計算の応用 : カオス : 渾沌を殺さず七竅を鑿つために」『数学セミナー』第47巻第11号、日本評論社、2008年11月、31-35頁、CRID 1050001339005746048、hdl:2115/42701、ISSN 03864960、NAID 120001909638。
^ 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
^ Kühn, Wolfgang (1998). “Rigorously computed orbits of dynamical systems without the wrapping effect”. Computing (Springer) 61: 47-67. doi:10.1007/BF02684450. https://doi.org/10.1007/BF02684450.
^ Loh, E., & Walster, G. W. (2002). Rump's example revisited. Reliable Computing, 8(3), 245-248.
^ 精度保証付き数値計算の必要性
^ “スカッドミサイルの追撃・阻止の失敗による兵舎の被爆”. 失敗知識データベース. 特定非営利活動法人失敗学会 (2018年1月30日). 2019年4月20日閲覧。
^ “アリアン5型ロケットが制御不能で４０秒後に爆発”. 失敗知識データベース. 特定非営利活動法人失敗学会 (2018年1月30日). 2019年4月20日閲覧。
^ Rounding error changes Parliament makeup
^ 大石進一：「精度保証付き数値計算」、コロナ社、（1999年）
^ ^a ^b ^c 山本哲朗『数値解析入門』（増訂版）サイエンス社〈サイエンスライブラリ現代数学への入門 14〉、2003年6月。ISBN 4-7819-1038-6。
^ ガンマ関数の精度保証付き計算メモ (PDF)
^ 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.
^ ^a ^b Zeidler, E., Nonlinear Functional Analysis and Its Applications I-V. en:Springer Science & Business Media.
^ ^a ^b ^c 杉原正顯, & 室田一雄. (1994). 数値計算法の数理. 岩波書店.
^ ^a ^b ^c 非線形方程式に対する解の精度保証付き数値計算 (PDF)
^ 中尾充宏, & 山本野人. (1998). 精度保証付き数値計算チュートリアル: 応用数理最前線.
中尾充宏, & 渡部善隆. (2011). 実例で学ぶ精度保証付き数値計算, サイエンス社.
Nakao, Mitsuhiro T; Plum, Michael; Watanabe, Yoshitaka (2019). Numerical verification methods and computer-assisted proofs for partial differential equations. Springer. doi:10.1007/978-981-13-7669-6
^ Oishi, S., & Tanabe, K. (2009). Numerical Inclusion of Optimum Point for Linear Programming. JSIAM Letters, 1, 5-8.
^ 尾崎克久「誤らない計算幾何学アルゴリズム」『数学セミナー』第47巻第11号、東京 : 日本評論社、2008年11月、36-39頁、CRID 1523951030398658176、ISSN 03864960。
^ S.M. Rump: INTLAB - INTerval LABoratory. In Tibor Csendes, editor, Developments in Reliable Computing, pages 77-104. Kluwer Academic Publishers, Dordrecht, 1999.
^ Rohn, J. (2009). VERSOFT: verification software in MATLAB/INTLAB.
^ Montanher, T. M. (2009). Intsolver: An interval based toolbox for global optimization. Version 1.0.
^ Overview of kv – a C++ library for verified numerical computation, Masahide Kashiwagi, SCAN 2018.
^ Johansson, F. (2013). Arb: a C library for ball arithmetic. ACM Comm. Computer Algebra, 47(3/4), 166-169.
^ 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
^ 松田望『中心値・半径方式による精度保証付き多倍長区間演算ライブラリの開発』電気通信大学〈博士（工学）甲第851号〉、2016年。 NAID 500000971971。

参考文献

『精度保証付き数値計算の基礎』大石進一編著、コロナ社、2018年。2019年4月19日閲覧。
Warwick Tucker (1999). “The Lorenz attractor exists”. Comptes Rendus de l'Académie des Sciences - Series I - Mathematics 328 (12): 1197-1202. doi:10.1016/S0764-4442(99)80439-X 2019年4月20日閲覧。.
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. （区間演算に詳しい）
Siegfried M. Rump (1988), “Algorithms for Verified Inclusions: Theory and Practice,”, in R. E. Moore, Reliability in Computing: The Role of Interval Methods in Scientific Computing, Boston: Academic Press, pp. 109-126., doi:10.15480/882.316, https://doi.org/10.15480/882.316 2019年4月20日閲覧。
Rump, S. M. (2010). Verification methods: Rigorous results using floating-point arithmetic. en:Acta Numerica, 19, 287-449.
大石進一 (1997), 非線形解析入門, コロナ社. （PDEの精度保証付き数値解法で用いる関数解析の知識を詳述している）
中尾充宏，渡部善隆：「実例で学ぶ精度保証付き数値計算」、サイエンス社（SGCライブラリ 85）、（2011年10月25日）。

外部リンク

プロジェクト数学

ポータル数学

解説記事

[1] 山本哲朗によって発案された用語である

[大石他2018-2] 大石、他 (2018)

[3] 荒井迅「精度保証付き数値計算の力学系への応用について (力学系の研究 : トポロジーと計算機による新展開 RIMS研究集会報告集)」『数理解析研究所講究録』第1485号、京都大学数理解析研究所、2006年4月、1-13頁、CRID 1050001202109463040、hdl:2433/58149、ISSN 18802818、NAID 110004541092。

[4] 荒井迅「精度保証付き数値計算の応用 : カオス : 渾沌を殺さず七竅を鑿つために」『数学セミナー』第47巻第11号、日本評論社、2008年11月、31-35頁、CRID 1050001339005746048、hdl:2115/42701、ISSN 03864960、NAID 120001909638。

[5] 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

[6] Kühn, Wolfgang (1998). “Rigorously computed orbits of dynamical systems without the wrapping effect”. Computing (Springer) 61: 47-67. doi:10.1007/BF02684450. https://doi.org/10.1007/BF02684450.

[7] Loh, E., & Walster, G. W. (2002). Rump's example revisited. Reliable Computing, 8(3), 245-248.

[8] 精度保証付き数値計算の必要性

[9] “スカッドミサイルの追撃・阻止の失敗による兵舎の被爆”. 失敗知識データベース. 特定非営利活動法人失敗学会 (2018年1月30日). 2019年4月20日閲覧。

[10] “アリアン5型ロケットが制御不能で４０秒後に爆発”. 失敗知識データベース. 特定非営利活動法人失敗学会 (2018年1月30日). 2019年4月20日閲覧。

[11] Rounding error changes Parliament makeup

[12] 大石進一：「精度保証付き数値計算」、コロナ社、（1999年）

[Yamamoto1-13] 山本哲朗『数値解析入門』（増訂版）サイエンス社〈サイエンスライブラリ現代数学への入門 14〉、2003年6月。ISBN 4-7819-1038-6。

[14] ガンマ関数の精度保証付き計算メモ (PDF)

[15] 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.

[16] 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.

[17] 大石進一(2008): 電子情報通信学会技術研究報告. NLP, 非線形問題, 108, 55-57.

[18] N. Yamamoto and N. Matsuda (2005): Trans. Jap. Soc. Indust. Appl. Math., 15, 347-359.

[19] 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.

[20] Johansson, F. (2019). Computing Hypergeometric Functions Rigorously. ACM Transactions on Mathematical Software (TOMS), 45(3), 30.

[21] Johansson, F. (2015). Rigorous high-precision computation of the Hurwitz zeta function and its derivatives. Numerical Algorithms, 69(2), 253-270.

[22] Johansson, F. (2017). Arb: efficient arbitrary-precision midpoint-radius interval arithmetic. IEEE Transactions on Computers, 66(8), 1281-1292.

[23] Johansson, F. (2018, July). Numerical integration in arbitrary-precision ball arithmetic. In International Congress on Mathematical Software (pp. 255-263). Springer, Cham.

[24] 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.

[zeidler-25] Zeidler, E., Nonlinear Functional Analysis and Its Applications I-V. en:Springer Science & Business Media.

[sm-26] 杉原正顯, & 室田一雄. (1994). 数値計算法の数理. 岩波書店.

[takayasu-27] 非線形方程式に対する解の精度保証付き数値計算 (PDF)

[28] 中尾充宏, & 山本野人. (1998). 精度保証付き数値計算チュートリアル: 応用数理最前線.
中尾充宏, & 渡部善隆. (2011). 実例で学ぶ精度保証付き数値計算, サイエンス社.
Nakao, Mitsuhiro T; Plum, Michael; Watanabe, Yoshitaka (2019). Numerical verification methods and computer-assisted proofs for partial differential equations. Springer. doi:10.1007/978-981-13-7669-6

[29] Oishi, S., & Tanabe, K. (2009). Numerical Inclusion of Optimum Point for Linear Programming. JSIAM Letters, 1, 5-8.

[30] 尾崎克久「誤らない計算幾何学アルゴリズム」『数学セミナー』第47巻第11号、東京 : 日本評論社、2008年11月、36-39頁、CRID 1523951030398658176、ISSN 03864960。

[31] S.M. Rump: INTLAB - INTerval LABoratory. In Tibor Csendes, editor, Developments in Reliable Computing, pages 77-104. Kluwer Academic Publishers, Dordrecht, 1999.

[32] Rohn, J. (2009). VERSOFT: verification software in MATLAB/INTLAB.

[33] Montanher, T. M. (2009). Intsolver: An interval based toolbox for global optimization. Version 1.0.

[34] Overview of kv – a C++ library for verified numerical computation, Masahide Kashiwagi, SCAN 2018.

[35] Johansson, F. (2013). Arb: a C library for ball arithmetic. ACM Comm. Computer Algebra, 47(3/4), 166-169.

[36] 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.

[37] ValidatedNumerics.jl: a new framework in Julia, David P. Sanders and Luis Benet, SCAN 2018.

[38] Interval and Verified Software

[39] 松田望『中心値・半径方式による精度保証付き多倍長区間演算ライブラリの開発』電気通信大学〈博士（工学）甲第851号〉、2016年。 NAID 500000971971。

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]

[38]

[39]

表話編歴数学
主要分野	数理論理学集合論圏論代数学初等線型多重線型抽象算術/数論解析学/微分積分学関数解析学行列解析幾何学代数微分有限離散位相代数的位相表現論リー理論（英語版）微分方程式線型微分方程式複素微分方程式常微分方程式偏微分方程式積分微分方程式力学系組合せ数学数理物理学ゲーム理論グラフ理論最適化問題数理最適化計算理論確率論数理統計学（英語版）制御理論三角法
トピックス	数学史和算算道数理哲学美未解決問題算数・数学教育算数教科
主要賞	ド・モルガン・メダルコール賞フィールズ賞スティール賞ウルフ賞ショウ賞アーベル賞数学ブレイクスルー賞
応用	情報理論折紙の数学囲碁と数学数値解析精度保証付き数値計算計算機援用証明数値線形代数常微分方程式の数値解法偏微分方程式の数値解法
学会・団体	国際数学者会議国際数学連合国際産業数理・応用数理会議国際産業数理・応用数理評議会（英語版）アメリカ数学会 SIAM ヨーロッパ数学会ロンドン数学会日本応用数理学会日本数学会数学教育協議会
競技	国際数学オリンピック日本数学オリンピック日本ジュニア数学オリンピック広中杯近畿大学数学コンテスト人の最大の力を競う算数・数学の大会
研究所	京都大学数理解析研究所明治大学先端数理科学インスティテュート統計数理研究所アンリ・ポアンカレ研究所オーバーヴォルファッハ数学研究所クレイ研究所 CIMAT数学研究センターステクロフ数学研究所
一覧数学定数数関数図形数学記号数学者エポニムカテゴリポータル

表話編歴関数解析学
集合 / 部分集合のタイプ	均衡星状絶対凸凸併呑有界（英語版）放射状（英語版）対称（英語版）線型錐（部分集合）凸錐（部分集合）
線型位相空間のタイプ	バナッハ樽型界相 Brauner（英語版） F-空間有限次元フレシェ (tame) ヒルベルト LF空間局所凸マッキー（英語版）モンテル核型ノルム付き（ノルム）準ノルム付き回帰的リーススミス（英語版） Stereotype（英語版）ウェブ付き位相テンソル積（英語版）（ヒルベルト空間の（英語版））
位相	双対双対空間作用素強（極作用素） Ultrastrong（英語版）弱（作用素） Ultraweak（英語版）一様収束（英語版）
線型作用素	随伴双線型（形式）有界 / 非有界閉（英語版）連続 / 不連続コンパクトフレドホルムヒルベルト＝シュミット汎関数（正（英語版））正規核自己共役 Strictly singular（英語版）トレースクラス転置ユニタリ
集合の操作	代数的内部（核）内部ミンコフスキー和（英語版）極
バナッハ環	C-環スペクトル（C-環（英語版）半径) スペクトル理論
定理	Eberlein–Šmulian（英語版）開写像角谷の不動点ゲルファント＝マズールコーシー＝シュワルツの不等式 Goldstine（英語版）シャウダーの不動点パーセヴァルの等式ハーン–バナッハ（分離超平面）バナッハ＝アラオグル Banach–Saks（英語版） Banach–Mazur（英語版）フロイデンタールのスペクトル閉値域閉グラフベッセルの不等式マッキー＝アレンスマズールの補題リースの拡張 Lomonosov's invariant subspace（英語版）ニュートン＝カントロビッチ
解析	ボホナー空間フレシェ空間における微分（英語版）微分（フレシェガトー汎函数 holomorphic（英語版））積分（ボホナー Dunford ゲルファント＝ペティス方正弱) 汎函数計算（Borel（英語版） continuous（英語版） holomorphic（英語版））逆函数定理（Nash–Moser theorem（英語版））ベクトル測度
応用	量子力学の数学的定式化有限要素法偏微分方程式の解に対する精度保証付き数値計算
日本人研究者	加藤敏夫吉田耕作藤田宏増田久弥
海外の研究者	リース・フリジェシュステファン・バナフダフィット・ヒルベルトイズライル・ゲルファントピーター・ラックス
カテゴリ

精度保証付き数値計算