4 0 0 0 数学の自動化を推進するための機械学習を用いた定理自動証明手法
数学における証明のを計算機を用いて一部自動化することを目指します.本申請課題は,この最終目標に対する探索研究として,自然数に関する命題の証明の一部自動化を目指します.本申請課題では,証明が二者ゲームとして定式化でき,したがってゲーム AI の学習手法を証明ゲームに適用することで有能な自動証明アルゴリズムを錬成できるのではないか,というアイデアに基づいて研究を進めます.自動証明は様々なシステムが意図通りに動作することを保証するための要素技術として用いられており,その点で将来的に産業的なインパクト・貢献の可能性が期待できると考えています.
1 0 0 0 機械学習技術による高速な演繹的推論エンジンの開発
本研究では,近年著しい発展を遂げている機械学習技術を数理論理学的な問題に応用して,高効率な演繹的推論エンジンを構成することを目指す.機械学習技術は画像認識やゲームAIを含む様々な分野で著しい成功を遂げているが,証明などの演繹的推論が関わる分野には未だに古典的な演繹的推論技術が機械学習技術に優位である問題が多い.これまでの研究では解きたい問題を直接解く機械学習モデルを作る End-to-End の方法が主流であったが,本研究では解きたい問題ではなく機械学習に適した問題を学習させて,学習結果を演繹的推論エンジンで活用する.
1 0 0 0 OA AI時代を見据えたプログラム検証技術
プログラム検証とは、プログラムが正しく振る舞うかどうかを実行前に網羅的に検証する技術であり、ソフトウェアの信頼性向上のために欠かせないものである。本研究課題では、近年の機械学習技術の台頭とそれに伴うコンピュータによって制御されたシステムの社会への普及を踏まえ、(1)代表者らがこれまで研究を進めてきた高階モデル検査などの自動プログラム検証技術や理論をさらに発展させるとともに、(2)プログラム検証技術のさらなる飛躍のために機械学習技術を活用し、さらに(3)機械学習技術の台頭に伴うソフトウェアの質と量の変化に対応するための、新たなプログラム検証技術の確立を目指す。