精度保証付き数値計算のソースを表示

{{Differential equations}}
'''精度保証付き数値計算'''<ref>[http://www.oishi.info.waseda.ac.jp/~oishi/sir/index.html 山本哲朗によって発案された用語である]</ref>（せいどほしょうつきすうちけいさん、Validated Numerics, Rigorous Computation, Reliable Computation, Verified Computation, Numerical Verification, {{lang-de-short|Zuverlässiges Rechnen}}）とは数学的に厳密な[[誤差]]（前進誤差、後退誤差、[[丸め誤差]]、打切り誤差、[[離散化誤差]]）の評価を伴う数値計算のことであり、[[数値解析]]の一分野である<ref name="大石他2018">{{harvnb|大石、他 (2018)|ref="大石他2018"}}</ref>。演算では[[区間演算]]を使用し、結果はすべて区間で出力する。精度保証付き数値計算は[[ウォリック・タッカー]]によって14番目の[[スメイルの問題]]を解くのにも活用されており（{{harvnb|Tucker (1999)|ref="Tucker1999"}}を参照）、[[力学系]]の研究では重要なツールとして位置づけられている<ref>{{Cite journal|和書|author=荒井迅 |title=精度保証付き数値計算の力学系への応用について (力学系の研究 : トポロジーと計算機による新展開 RIMS研究集会報告集) |journal=数理解析研究所講究録 |issn=18802818 |publisher=京都大学数理解析研究所 |date=2006-04 |issue=1485 |pages=1-13 |naid=110004541092 |url=https://hdl.handle.net/2433/58149 |hdl=2433/58149 |CRID=1050001202109463040}}</ref><ref>{{Cite journal|和書|author=荒井迅 |title=精度保証付き数値計算の応用 : カオス : 渾沌を殺さず七竅を鑿つために |journal=数学セミナー |issn=03864960 |publisher=日本評論社 |date=2008-11 |volume=47 |issue=11 |pages=31-35 |naid=120001909638 |url=https://hdl.handle.net/2115/42701 |hdl=2115/42701 |CRID=1050001339005746048}}</ref><ref>D. Michelucci (2000), "Reliable computations for dynamic systems". ''Proc. SCAN 2000 / Interval 2000 &mdash; 9th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic, and Validated Numerics''</ref><ref>{{Cite journal |author=Kühn, Wolfgang |year=1998 |url=https://doi.org/10.1007/BF02684450 |title=Rigorously computed orbits of dynamical systems without the wrapping effect |journal=Computing |volume=61 |pages=47-67 |publisher=Springer |doi=10.1007/BF02684450}}</ref>。
{{seealso|数値解析|区間演算}}

==精度保証付き数値計算の必要性==
精度保証付き数値計算ではない通常の数値計算だと誤差によって不都合な事象が生じてしまう。いくつかのその例を挙げる。
===Rumpの例題===
1980年代にRumpは次のような例を提示した（{{harvnb|Rump (1988)|ref="Rump1988"}}を参照）。
:<math>f(a,b) = 333.75b^6 + a^2 ( 11a^2 b^2 - b^6 - 121b^4 - 2 ) + 5.5b^8 + \frac{a}{2b}</math>

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

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

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

===数値計算の誤差による事故===
数値計算の誤差によって生じた事故として次の3つが挙げられる。
*[[湾岸戦争]]でのミサイル迎撃失敗（1991年）<ref>{{Cite web|和書|date=2018-01-30|author=|title=スカッドミサイルの追撃・阻止の失敗による兵舎の被爆|url=https://www.shippai.org/fkd/cf/CA0000298.html |accessdate=2019-04-20|work=失敗知識データベース|publisher=特定非営利活動法人 失敗学会|ref=}}</ref>
*[[アリアン5]]ロケットの発射失敗（1996年）<ref>{{Cite web|和書|date=2018-01-30|author=|title=アリアン5型ロケットが制御不能で４０秒後に爆発|url=https://www.shippai.org/fkd/cf/CA0000284.html|accessdate=2019-04-20|work=失敗知識データベース|publisher=特定非営利活動法人 失敗学会|ref=}}</ref>
*選挙結果の間違い<ref>[http://catless.ncl.ac.uk/Risks/13.37.html#subj4 Rounding error changes Parliament makeup]</ref>

==主な研究分野==
精度保証付き数値計算は主に以下の分野に分かれて研究がなされている<ref name="大石他2018">{{harvnb|大石、他 (2018)|ref="大石他2018"}}</ref><ref>[[大石進一]]：「精度保証付き数値計算」、コロナ社、（1999年）</ref>。
*[[数値線形代数]] ([[:en:Numerical linear algebra|en]]) における精度保証（行列積、連立一次方程式、[[固有値]]問題を扱う<ref name="Yamamoto1">{{Cite book |和書 |author=山本哲朗 |title=数値解析入門 |edition=増訂版 |date=2003-06 |publisher=[[サイエンス社]] |series=サイエンスライブラリ 現代数学への入門 14 |ISBN=4-7819-1038-6}}</ref>）
*[[初等関数]]、[[特殊関数]]の精度保証
**[[ガンマ関数]]<ref>{{PDFlink|[http://verifiedby.me/kv/special/gamma.pdf ガンマ関数の精度保証付き計算メモ]}}</ref><ref>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.</ref><ref>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.</ref>
**[[ベッセル関数]]<ref>[[大石進一]](2008): 電子情報通信学会技術研究報告. NLP, 非線形問題, 108, 55-57.</ref><ref>N. Yamamoto and N. Matsuda (2005): Trans. Jap. Soc. Indust. Appl. Math., 15,
347-359.</ref>
**[[楕円関数]]<ref>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.</ref>
**[[超幾何級数]]<ref>Johansson, F. (2019). Computing Hypergeometric Functions Rigorously. ACM Transactions on Mathematical Software (TOMS), 45(3), 30.</ref>
**[[フルヴィッツのゼータ函数]]<ref>Johansson, F. (2015). Rigorous high-precision computation of the Hurwitz zeta function and its derivatives. Numerical Algorithms, 69(2), 253-270.</ref>
*[[数値積分]]の精度保証<ref>Johansson, F. (2017). Arb: efficient arbitrary-precision midpoint-radius interval arithmetic. IEEE Transactions on Computers, 66(8), 1281-1292.</ref><ref>Johansson, F. (2018, July). Numerical integration in arbitrary-precision ball arithmetic. In International Congress on Mathematical Software (pp. 255-263). Springer, Cham.</ref><ref>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.</ref>
（[[ガウス求積]]、[[二重指数関数型数値積分公式]]などの数値積分公式の誤差評価を行う）
*非線形方程式の精度保証付き数値解法（[[:en:Kantorovich theorem|Newton-Kantorovichの定理]]<ref name="Yamamoto1"/><ref name="zeidler">Zeidler, E., Nonlinear Functional Analysis and Its Applications I-V. [[:en:Springer Science & Business Media]].</ref><ref name="sm">[[杉原正顯]], & 室田一雄. (1994). 数値計算法の数理. [[岩波書店]].</ref><ref name="takayasu">{{PDFlink|[http://www.sr3.t.u-tokyo.ac.jp/jsiam/slides/2016/takayasu_web.pdf 非線形方程式に対する解の精度保証付き数値計算]}}</ref>、Krawczyk法<ref name="takayasu"/>、[[区間ニュートン法]]<ref name="sm"/><ref name="takayasu"/>、Durand-Kerner-Aberth法<ref name="Yamamoto1"/><ref name="sm"/>に関する研究が含まれる）
*ODE・PDEの精度保証付き数値解法（PDEでは[[有限要素法]]、[[関数解析]]の知識を駆使する<ref name="zeidler"/><ref>中尾充宏, & 山本野人. (1998). 精度保証付き数値計算 チュートリアル: 応用数理最前線.<br />中尾充宏, & 渡部善隆. (2011). 実例で学ぶ精度保証付き数値計算, サイエンス社.<br />{{cite book |author=Nakao, Mitsuhiro T; Plum, Michael; Watanabe, Yoshitaka |year=2019 |url=https://link.springer.com/book/10.1007/978-981-13-7669-6 |title=Numerical verification methods and computer-assisted proofs for partial differential equations |publisher=Springer |doi=10.1007/978-981-13-7669-6 |ref=harv}}</ref>）
*[[積分方程式]]の精度保証付き数値解法
*[[線形計画法]]の精度保証<ref>Oishi, S., & Tanabe, K. (2009). Numerical Inclusion of Optimum Point for Linear Programming. JSIAM Letters, 1, 5-8.</ref>
*[[計算幾何学]]における精度保証<ref>{{Cite journal|和書|author=尾崎克久 |date=2008-11 |title=誤らない計算幾何学アルゴリズム |journal=数学セミナー |ISSN=03864960 |publisher=東京 : 日本評論社 |volume=47 |issue=11 |pages=36-39 |url=https://ndlsearch.ndl.go.jp/books/R000000004-I9679518 |CRID=1523951030398658176}}</ref>
*[[高性能計算|HPC]]環境における精度保証
{{seealso|数値線形代数|常微分方程式の数値解法|偏微分方程式の数値解法|数値積分|計算幾何学|高性能計算}}

==主な精度保証付き数値計算ライブラリ==
*[[INTLAB]]: [[MATLAB]]/[[GNU Octave]]を使用するライブラリである<ref>S.M. Rump: INTLAB - INTerval LABoratory. In Tibor Csendes, editor, Developments in Reliable Computing, pages 77-104. Kluwer Academic Publishers, Dordrecht, 1999.</ref>。
**  [http://uivtx.cs.cas.cz/~rohn/matlab/ VERSOFT] ([[MATLAB]]/[[INTLAB]]で開発されたライブラリ)<ref>Rohn, J. (2009). VERSOFT: verification software in [[MATLAB]]/[[INTLAB]].</ref>
** [https://www.swmath.org/software/8787 INTSOLVER] ([[:en:global optimization|大域最適化問題]]を解くためのライブラリ、[[INTLAB]]を使用して開発された)<ref>Montanher, T. M. (2009). Intsolver: An interval based toolbox for global optimization. Version 1.0.</ref>
*[http://verifiedby.me/kv/ kv] ([[C++]]によるライブラリである)<ref>
Overview of kv – a C++ library for verified numerical computation, Masahide Kashiwagi, [[SCAN (国際研究集会)|SCAN]] 2018.</ref>
**{{GitHub|mskashi/kv}}
*[http://arblib.org/ Arb] [[C言語]]によるライブラリであり、様々な特殊関数の精度保証に対応している<ref>Johansson, F. (2013). Arb: a C library for ball arithmetic. ACM Comm. Computer Algebra, 47(3/4), 166-169.</ref>。
**{{GitHub|fredrik-johansson/arb}}
*{{GitHub|JuliaIntervals}} ([[Julia (プログラミング言語)|Julia]]によるライブラリ)<ref>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 (国際研究集会)|SCAN]] 2016, 124.</ref><ref>ValidatedNumerics.jl: a new framework in Julia, David P. Sanders and Luis Benet, [[SCAN (国際研究集会)|SCAN]] 2018.</ref>

その他、様々なライブラリが開発されている<ref>[http://www.cs.utep.edu/interval-comp/intsoft.html Interval and Verified Software]</ref><ref>{{cite thesis|和書|author=松田望 |year=2016 |title=中心値・半径方式による精度保証付き多倍長区間演算ライブラリの開発 |publisher=電気通信大学 |series=博士（工学） 甲第851号 |url=https://uec.repo.nii.ac.jp/records/1291 |naid=500000971971}}</ref>。

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

==関連項目==
*[[浮動小数点数]]
*[[不確かさ (測定)#関連項目|数値計算における誤差解析]]
*[[誤差#計算誤差の種類]]
*[[任意精度演算]]
===関連分野===
*[[計算機援用証明]]
*[[区間演算]]
*[[アフィン演算]]
*[[自動微分]]
*[[数値積分]]
*[[数値線形代数]]

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

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

==出典==
{{reflist|2}}

==参考文献==
洋書
* {{cite journal|author=Warwick Tucker|title=The Lorenz attractor exists|journal=Comptes Rendus de l'Académie des Sciences - Series I - Mathematics|volume=328|issue=12|year=1999|pages=1197-1202|url=https://doi.org/10.1016/S0764-4442(99)80439-X |accessdate=2019-04-20|doi=10.1016/S0764-4442(99)80439-X |ref="Tucker1999"}}
* 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''. [[:en:Society for industrial and applied mathematics|SIAM]]. （[[区間演算]]に詳しい）
* {{Citation | author=Siegfried M. Rump | year=1988 | contribution=Algorithms for Verified Inclusions: Theory and Practice, | contribution-url=https://doi.org/10.15480/882.316 |accessdate=2019-04-20 |doi=10.15480/882.316 | title=''Reliability in Computing: The Role of Interval Methods in Scientific Computing'' | editor = R. E. Moore | pages= 109-126. | publisher= Academic Press| location=Boston |ref= "Rump1988"}}
* 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日)。
* {{cite book|和書|author=[[大石進一]](編著)|title=精度保証付き数値計算の基礎|publisher=[[コロナ社]]|isbn=978-4-339-02887-4|year=2018-7-26|url=http://www.coronasha.co.jp/np/download/6965501695.pdf|accessdate=2019-04-19|ref="大石他2018"}}

==外部リンク==
{{ウィキプロジェクトリンク|数学|[[画像:Nuvola apps edu mathematics blue-p.svg|34px|Project:数学]]}}
{{ウィキポータルリンク|数学|[[画像:Nuvola apps edu mathematics-p.svg|34px|Portal:数学]]}}
* [http://www.ti3.tu-harburg.de/rump/intlab/ INTLAB]
* [https://mathsoc.jp/section/appliedmath/index.htm 応用数学分科会]
* [http://mathsoc.jp/office/prize/haruaki/nakao2012aki.html 精度保証付き数値計算の研究及びその偏微分方程式への応用]、2012年度[[日本数学会]][[秋季賞]]
* [https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-17002012/ 精度保証付き数値計算学の確立]
* [https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-18K03434/ 無限次元精度保証付き数値計算の新展開に向けての基礎的研究]

===解説記事===
* [http://nalab.mind.meiji.ac.jp/~mk/labo/text/IA/seidohosyou.html 精度保証ノート]
* {{PDFlink|[http://www.math.twcu.ac.jp/ogita/lec/u-tokyo2016/ogita01.pdf 計算機援用証明と精度保証付き数値計算]}}
* {{PDFlink|[http://ri2t.kyushu-u.ac.jp/~watanabe/LECTURE/INA/05.pdf 精度保証付き数値計算概論]}}
* {{PDFlink|[http://ri2t.kyushu-u.ac.jp/~watanabe/RESERCH/SLIDE/BIC2001.pdf 精度保証付き数値計算のアイディアお教えします]}}
* {{PDFlink|[https://271.jp/PDF/2015verify.pdf Introduction to verified computation]}}
* [https://discourse.julialang.org/t/reproducing-rump-s-example/6473 Reproducing Rump's example]

{{偏微分方程式の数値解法}}
{{数学}}
{{Functional analysis}}

{{DEFAULTSORT:せいとほしようつきすうちけいさん}}
[[Category:数値解析]]
[[Category:計算科学]]
[[Category:応用数学]]
[[Category:アルゴリズム]]
[[Category:数学に関する記事]]