|
本研究では記述計算量に基づき様々な論理式の探索と自動合成について一般的なモデルとそれに関するアルゴリズム・応用を課題にした。近年記述計算量をプログラム合成や形式検証で応用する研究がいくつかあるが、本研究ではそれらをunifyする一般的なモデルを大きな目的の一つにしている。つまり、計算量の帰着やプログラム合成など応用毎に最初からやり直すのではなく、一般的なモデルと実装の応用として簡単に利用できることを目的にしている。
本研究で得た主な成果は3つに分ける。まずは、最初から目的にしていた上記の一般的なモデルの提案とそれに関する基本的な性質を証明した。このモデルでは、従来の関連研究で使われた論理だけではなく、実数を扱える論理に拡張することによって、ニューラルネットワークや重み付きのグラフも取り扱えるようになった。
次は、このモデルを実装する時必要になる道具の一つであるQBFソルバに関していくつか成果もできた。特に、本領域に参加することによって、大規模なスパコンTsubameを利用することができて、並列計算や新しいQBF技術に関する研究ができて、複雑な合成問題などに応用することができる。最後は新学術領域に参加することによって、本領域に参加している研究者と議論したり新しい共同研究もできた。
それで本領域に参加できたおかげで、当初想像していなかった成果ができ、今後の研究に強く影響を与える。特に、本領域で初めて会った共同研究者と本領域で利用できたスパコンの組み合わせで新しい共同研究が生まれ、スパコンなど大規模な計算機で使える高速なフリーソフトを公開し、他分野の研究者が現在利用している。従来のものより千倍以上速くなる場合もあり、今まで解けなかった計算問題が解けるようになったので、計算限界をプッシュしている課題の一つになる。査読は何年間かかるものもあるため、論文はarXivなどで公開している。
|
