| 研究実績の概要 |
これまでの研究によって、証明支援系を現状のまま用いた場合、４次元ポアンカレ予想の核心部である、キャッソンハンドル=位相的ハンドル定理を形式化することに限っても、形式化にかかる時間・コストは当初の予想よりはるかに大きいことが判明してきた。これは、世界的に見ても、形式化がまだ組み合せ論や有限群論等の分野の周辺で進んでいるものの、トポロジーや多様体論の方向では全く進んでいないため、関連研究の利用ができない状況も影響している。それと同時に、ここ2年程度の間に、コンピューターが論理的推論を効率的に行う可能性が広がってきている。そこで、研究代表者はより包括的なアプローチとして、形式化の作業をコンピュータによって自動化する方法を探索することとした。現状でCOQで提供される自動証明はLtacという特殊言語でプログラムされるもので、局所的な自動化にとどまっている。ごく近年、深層学習フレームワークtensorflowがGoogle
から公開されたので、挑戦的方向として、深層強化学習を証明支援系に適用する方針をとった。世界の現状を把握するため、Aussois（仏）で開催されたAITP2018に出席した。証明支援系Coqと深層学習フレームワークTensorflowを同一プログラムからコントロールする問題を解決するため、研究代表者はCoqに対するPythonインターフェースを開発した：Kuga:PICoq Python Interface for Coq,ソフトウェアhttps://bitbucket.org/kenkuga/picoq このことによって、Coqからの応答をstateとし、tacticsの選択をactionとする深層強化学習の使用環境ができた。
|
