| 研究課題/領域番号 |
15K11984
|
|---|
| 研究機関 | 国立情報学研究所 |
|---|
研究代表者 |
蓮尾 一郎 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (60456762)
|
|---|
| 研究分担者 |
星野 直彦 京都大学, 数理解析研究所, 助教 (20611883)
室屋 晃子 京都大学, 数理解析研究所, 助教 (00827454)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2019-03-31
|
| キーワード | プログラミング言語理論 / 確率的プログラミング言語 / 高階計算 / プログラム検証 / 確率的システム / 確率的システム検証 / 統計的機械学習 |
|---|
| 研究実績の概要 |
以下の3つの方向で研究を行い，それぞれで（理論計算機科学の旗艦国際会議 LICS の予稿集論文を含む）多くの論文を出版した．
まず最初に，昨年度から引き続き，一階の確率的プログラムに対する静的解析手法（特に可達性確率計算アルゴリズム）を研究した．この成果はトップ国際会議 ATVA’18，TACAS’19 において（プロトタイプ実装と実験による性能評価とともに）発表された．この成果の技術的なキーは適切なマルチンゲール概念の定義であり，そのための束論的・圏論的基盤についても研究を行い，CMCS’18，LICS’19 で論文が採択された．
次に，上述の非高階の確率的プログラム解析手法について，これを本研究の対象たるconditioning および sampling をプリミティブとして持つ高階・関数型プログラムへ応用するにあたり，コアとなる「高階から一階へ」の翻訳手法を研究した．この翻訳手法は高階の確率的プログラムを一階の確率的プログラムで記述可能な確率的状態遷移系に変換するもので，その正しさが数学的に保証されている．この成果は LICS’19 に採択された．
並行して，本研究のもう一つの獲得目標である，確率的プログラムの効率的実装に向けて，以下の研究を行い LICS’18, FLOPS’18 で論文を発表した．確率的モデルや機械学習モデルに共通する特徴に，実行時に上書きされるパラメータがある（ニューラルネットの重みなど）．その簡便な扱いについて既存の機械学習ライブラリ (TensorFlow) から着想し，高階・関数型プログラミングとの融合を可能にする言語設計・実行モデル設計・プロトタイプ実装を行った。特に実行モデルは，GoIとグラフ書き換え系の融合により実行コスト解析が可能なモデルを応用した．
|
