H行列を用いた連立一次方程式の精度保証付き数値計算法近年，H行列を用いた連立一次方程式の精度保証付き数値計算法がいくつか提案されている． 高精度な近似解を用いることができ，高精度計算と親和性が良いことから広く用いられている． 特にINTLABと呼ばれるソフトウェアで用いられている． 今年，INTLABがv11となり連立一次方程式の精度保証付き数値計算法のverifylssのコードがバージョンアップされた． 主な変更点は誤差評価式の変更であり，過去に著者らが開発した誤差評価式である． 誤差評価式とINTLABにどのように実装されているかを簡単に説明し，この誤差評価式の強みと弱みを説明する． また，時間が許せば関連するテーマの話題提供を行う．
大規模線形計算に関する精度保証付き数値計算極限の探究に資する精度保証付き数値計算学の展開と超高性能計算環境の創成と いうプロジェクトを推進している．研究分担を行っている芝浦工業大学グループ は大規模線形計算の精度保証法について研究しており，基本演算，連立一次方程 式，高精度計算などについて成果をあげている．本研究集会ではその成果を報告 し，スーパーコンピュータとして理研・京コンピュータと富士通FX100を使用し た研究結果について紹介したい．
線形熱方程式の時間周期解に対する近似解の誤差評価について線形熱方程式の時間周期解に対する近似解の誤差評価を行う手法を提案する．提案手法は発表者らがこれまでに提案してきた行列指数関数を用いた微分方程式の初期値境界値問題に対する精度保証付き数値計算法を拡張して応用したものであり，ある時間での解の半離散近似における誤差評価と，それを初期値とした常微分方程式の初期値問題に対する近似解の誤差評価とを組み合わせることで周期解とその近似との誤差評価を行うものである．
半線形熱方程式の解の精度保証付き数値計算法について半線形熱方程式を含めた時間発展方程式の解の精度保証付き数値計算法は, 中尾充宏先生の手法から始まり様々な手法が提案されてきた. しかし, 一般に時間発展方程式の解の存在検証に用いられる評価式は時間が経過すると過大評価になりやすく, 真の解と近似解との間の誤差の数値が大きく見積もられる傾向にある. そのため現状では長時間の解の数値的存在検証がとても困難とされている. そこで本講演では, 既存の手法を組み合わせて長い時間の解の存在を検証する方法を考察し, その案とその案に含まれる未解決な点を講演する.
発展方程式の初期値問題に対する数値的検証法発展方程式の初期値問題に対して、全離散有限要素スキームの構成的誤差評価を用いて、時間ステップアプローチでのNakao法による非線形問題の解に対する数値的検証法について講演する。 時間ステップアプローチでは誤差の積み重なりが問題となり、線形化逆作用素の縮小性、非線形項の引き込み性の評価の工夫が必要となる。 講演では、発展型Allen-Cahn方程式とFujita-type方程式の数値結果を基に、これまでの研究状況について講演する。
Hyper Dual Number の性質を用いた高階微分の精度保証付き数値計算法材料工学では材料構成則の高精度な数値計算を行うのに、増分ポテンシャル法というエネルギーベースで統一的に記述する方法が開発されており、 その利用にはひずみエネルギー密度関数や損失エネルギーの高階偏微分が必要となる。ここでは、同分野で利用されている Hyper Dual Number を基礎とした、高階偏微分計算の高性能化について述べる。
精度保証付き数値計算のライブラリの開発についてナビエストークス方程式の解の検証などの計算機援用証明の計算では、 多くの精度保証付き数値計算のライブライの開発が必要となっています。 この発表では、発表者が取り込んでいる幾つかのライブライの開発状況を報告します。 また、より効率的なコードの開発・共有方法について、研究集会の参加者と一緒に検討したいです。
線形化作用素の逆作用素のノルム評価を利用しない楕円型偏微分方程式の解に対する計算機援用証明 法現在の楕円型偏微分方程式の解の計算機援用存在証明法は「線形化作用素の逆作用素」と「無限次元Newton法」を用いて問題を不動点形式化してから，不動点定理を利用して解の存在を証明する. しかし無限次元問題であるため直接的には計算することができず，「線形化作用素の逆作用素のノルム」，「残差ノルム」，「リプシッツ項」と過大評価ではあるが3つにわけることで計算可能である. 本発表では線形化作用素の逆作用素を用いた無限次元Newton法に対して不動点定理を利用するにもかかわらず，有限次元と無限次元にわけることで上記の過大評価を回避した新しい解の計算機援用存在証明法を提案する.
反復解法における誤差履歴連立一次方程式に対する非定常反復法において、反復における 残差履歴と一緒に精度保証された誤差履歴を表示するとどうな るか、いくつかの問題に対してデータを採取してみました。 結論は特にありません。
複素対称線形方程式における反復法と多倍⻑精度計算について高周波電磁界解析において，電場を未知関数としたベクトル波動方程式を辺要素有限要素法で離散化すると，複素対称行列を係数とする線形方程式が得られる．このときの係数行列は，対角優位ではない，エルミート行列でいうところの半正定値に近い，などの特徴がある．著者らは，この方程式に対するKrylov部分空間法の開発や多倍長精度計算の有効性評価に関する研究を行っている．今回はこれまでの研究成果と今後の課題について報告する．
Why3を用いた区間演算ライブラリの検証区間演算ライブラリは浮動小数点数区間を対象とした高信頼な四則演算手続きを提供する．これらの手続きの実装では，区間の端の組み合わせや浮動小数点数の特殊値を考慮する必要があるため，多数の条件分岐を記述することになり，実装の正しさは自明でない． 本研究では，区間演算ライブラリを対象としたプログラム検証に取り組み，高信頼な実装を提供することを目標とする．プログラム検証には Why3 プラットフォームを用いる．Why3 を用いることにより，独自言語を用いてアノテーション付きプログラムを記述し，記述結果から検証条件への変換を対話的に実施し，検証条件の妥当性をSMTソルバーや証明支援系を用いて判定することにより，アノテーション付きプログラムの正しさを半自動的に証明することができる．本研究で扱う検証条件は，浮動小数点理論に基づく述語論理式となるが，最新のSMTソルバーとCoqがプラグインされたWhy3を利用し，区間の四則演算手続きを検証することができた．
尾崎スキームによる高精度かつ再現性のあるBLASルーチンの実装と評価本講演では尾崎らが提案したlevel-3 BLASに基づく高精度行列積計算法（尾崎スキーム）を用いた，高精度かつ再現性（reproducibility）のあるBLASルーチン群の実装と性能について報告する．これまでにDOT，GEMV，GEMMの3ルーチンをCUDAで実装し，VoltaアーキテクチャGPUにおいて，期待される性能の80%前後の性能が得られることを確認した．
マルチコアCPUおよびGPUにおける高精度行列-行列積のための疎行列演算の実装と評 価本発表では、尾崎らによって開発された高精度行列-行列積演算中に現れる 複数の行列-行列積演算において各行列が疎行列となる場合に、 疎行列演算に置き換えることで高性能化する実装方式を評価する。 マルチコアCPUに加えて、GPU向けの疎行列演算数値計算ライブラリを 用いた実装方式の性能評価を行い、双方の計算機環境で疎行列化の有効性を評価する。
自動微分・アルゴリズム微分の最近の話題自動微分・アルゴリズム微分における最近の話題について触れる． 自動微分は機械学習の文脈で今まで以上に広く知られるようになってきているが，自動微分の進展としては Griewank 教授等による絶対値演算の系統的な処理法とその応用が目覚ましい． ここではその原理をなすAbsolute Normal Form の導出法を解説し，その応用や変種等について紹介する．
常微分方程式の精度保証パッケージの評価と今後の展望LohnerのAWAパッケージ、kvの精度保証付き常微分方程式ソルバ、 Intlab11で実装されたawa、verifyodeを比較・評価する。 その結果を元に、特にstiffな常微分方程式の精度保証について、 今後の展望を考える。