精度保証付き数値計算

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

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

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

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

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

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

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

主な研究分野
精度保証付き数値計算は主に以下の分野に分かれて研究がなされている。
数値線形代数 (en) における精度保証（行列積、連立一次方程式、固有値問題を扱う）
初等関数、特殊関数の精度保証
ガンマ関数
ベッセル関数
楕円関数
超幾何級数
フルヴィッツのゼータ函数
数値積分の精度保証
（ガウス求積、二重指数関数型数値積分公式などの数値積分公式の誤差評価を行う）
非線形方程式の精度保証付き数値解法（Newton-Kantorovichの定理、Krawczyk法、区間ニュートン法、Durand-Kerner-Aberth法に関する研究が含まれる）
ODE・PDEの精度保証付き数値解法（PDEでは有限要素法、関数解析の知識を駆使する）
積分方程式の精度保証付き数値解法
線形計画法の精度保証
計算幾何学における精度保証
HPC環境における精度保証

主な精度保証付き数値計算ライブラリ
INTLAB: MATLAB/GNU Octaveを使用するライブラリである。
  VERSOFT (MATLAB/INTLABで開発されたライブラリ)
 INTSOLVER (大域最適化問題を解くためのライブラリ、INTLABを使用して開発された)
kv (C++によるライブラリである)

Arb C言語によるライブラリであり、様々な特殊関数の精度保証に対応している。

 (Juliaによるライブラリ)

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

関連する研究集会
日本数学会・応用数学分科会
日本応用数理学会・計算の品質研究部会
日本シミュレーション学会・精度保証付シミュレーション技術研究委員会
数値解析シンポジウム (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), 非線形解析入門, コロナ社. （PDEの精度保証付き数値解法で用いる関数解析の知識を詳述している）
 中尾充宏，渡部善隆：「実例で学ぶ精度保証付き数値計算」、サイエンス社（SGCライブラリ 85）、（2011年10月25日）。

外部リンク

 INTLAB
 応用数学分科会
 精度保証付き数値計算の研究及びその偏微分方程式への応用、2012年度日本数学会秋季賞
 精度保証付き数値計算学の確立
 無限次元精度保証付き数値計算の新展開に向けての基礎的研究

解説記事
 精度保証ノート
 
 
 
 
 Reproducing Rump's example

数値解析
計算科学
応用数学
アルゴリズム
数学に関する記事