1 0 0 0 機械学習技術による高速な演繹的推論エンジンの開発
本研究では,近年著しい発展を遂げている機械学習技術を数理論理学的な問題に応用して,高効率な演繹的推論エンジンを構成することを目指す.機械学習技術は画像認識やゲームAIを含む様々な分野で著しい成功を遂げているが,証明などの演繹的推論が関わる分野には未だに古典的な演繹的推論技術が機械学習技術に優位である問題が多い.これまでの研究では解きたい問題を直接解く機械学習モデルを作る End-to-End の方法が主流であったが,本研究では解きたい問題ではなく機械学習に適した問題を学習させて,学習結果を演繹的推論エンジンで活用する.
1 0 0 0 OA AI時代を見据えたプログラム検証技術
プログラム検証とは、プログラムが正しく振る舞うかどうかを実行前に網羅的に検証する技術であり、ソフトウェアの信頼性向上のために欠かせないものである。本研究課題では、近年の機械学習技術の台頭とそれに伴うコンピュータによって制御されたシステムの社会への普及を踏まえ、(1)代表者らがこれまで研究を進めてきた高階モデル検査などの自動プログラム検証技術や理論をさらに発展させるとともに、(2)プログラム検証技術のさらなる飛躍のために機械学習技術を活用し、さらに(3)機械学習技術の台頭に伴うソフトウェアの質と量の変化に対応するための、新たなプログラム検証技術の確立を目指す。
1 0 0 0 OA 高階モデル検査の深化と発展
本課題では、高階モデル検査の(1)理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、(2)プログラム検証への応用、(3)高階モデル検査の拡張とそのプログラム検証への応用、(4)データ圧縮への応用、の4つを柱に研究を進めている。以下、それぞれの項目について、平成28年度(およびその繰越として遂行した平成29年度の一部の結果)について述べる。(1)理論的基盤の強化:HORSモデル検査とHFLモデル検査という2種類の高階モデル検査の間に相互変換が存在することを示すとともに、HFLモデル検査問題を型推論問題に帰着できることを示した。後者の結果に基づき、HFLモデル検査器のプロトタイプを作成した。また、高階文法の性質について調べ、語を生成するオーダーnの文法と木文法を生成するオーダーn-1の文法と間の対応関係を示した。さらに、高階モデル検査アルゴリズムの改良を行い、値呼びプログラムに対して直接的に高階モデル検査を適用する手法を考案、実装した。(2)プログラム検証への応用:プログラム検証で扱える対象プログラムや性質の拡充を行い、関数型プログラムの公平非停止性の検証、コード生成プログラムの検証、動的なスレッド生成を伴う高階並列プログラムの検証、などを可能にした。(3)拡張高階モデル検査:HORSに再帰型を加えて拡張したμHORSに対するモデル検査アルゴリズムの改良を行い、その有効性をJavaプログラムの検証を通して示した。(4)データ圧縮への応用:データをそれを生成する関数型プログラムの形に圧縮する方式(高階圧縮)について、圧縮後のプログラムをビット列に変換する部分の改良を行った。また、高階圧縮のための様々な要素技術について研究を進めた。