2015 Fiscal Year Annual Research Report
論理式の探索と自動合成による計算限界解析
Publicly Offered Research
| Project Area | A multifaceted approach toward understanding the limitations of computation |
|---|
| Project/Area Number |
15H00847
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2015-04-01 – 2017-03-31
|
| Keywords | 記述計算量 / 機会学習 / 並列計算 / 分散計算 |
|---|
| Outline of Annual Research Achievements |
本研究では記述計算量に基づき様々な論理式の探索と自動合成について一般的なモデルとそれに関するアルゴリズム・応用を課題にしている。今年の計画では、近年記述計算量をプログラム合成や形式検証で応用する研究をunifyする一般的なモデルを大きな目的の一つにしている。つまり、計算量の帰着やプログラム合成など応用毎に最初からやり直すのではなく、一般的なモデルの実現として扱えるモデルがあればそれぞれの応用で簡単に利用ができ、新しい分野での実験や違う論理の論理式を合成することがすぐできる。
そのモデルについては共同研究者と本年度作成できたが、査読の遅さなどによってまだ雑誌などではまだ出ていない。しかし、目的にしていたモデルができたので計画していた目的は得られている。このモデルでは、従来の関連研究で使われて論理だけではなく実数を扱うmetafiniteストラクチャーを利用し、ニューラルネットワークや重みつきグラフも取り扱えるため新しい応用もできる。また、モデルの基本的な性質をいくつか証明し応用でそれなりの保証付きで合成・探索ができる。査読はかなり時間がかかる場合があるが、従来のものをunifyできるモデルができた。また、このモデルを実装する時必要になる道具の一つであるQBFに関していくつか成果もできた。
しかし、新学術領域に参加できたことによって本領域に参加している研究者と共同研究もできた。それで本領域に参加できたおかげで当初想像していなかった成果ができ、今後の研究に強く影響を与える。特に、その一部は本領域に参加できたことによって利用できるスパコンTsubameを利用する共同研究だが、スパコンなど大規模な計算機を使うための高速な分散フリーソフトを公開し、他分野の研究者が現在利用している。従来のものより千倍以上速くなる場合もあり、今まで解けなかった計算問題が解けるようになった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の目的は前述した論理式の探索と合成に関する一般的なモデルとその応用である。当初の計画では、本年度は従来の応用をunifyするモデルを提案することとそのモデルの基本的な性質について研究する。ジャーナルの査読の遅さによって、まだ論文が出ていないが、その一般的なモデルと理論的な性質を証明することができたた。これは当初の計画としておおむね順調に進展している。
本領域のほかのメンバーと交流し、当初想像していなかった共同研究もできた。それは想像もしていなかったため、当初の計画以上進展しているところもある。特に本領域に参加することによって、大規模なスパコンTsubameを利用し、本領域のほかの班との共同研究で、計算幾何学の問題を解く高速な分散プログラムをフリーソフトとして公開した。広く使われるソフトの新バージョンのため、大規模な問題を並列で解きたい研究者に利用すると思われる。また、その共同研究ではその実装だけではなくもっと一般的に利用できることと様々な理論的な保証もあるため、今後の新しい研究につながる。これは本領域に参加できたことによって想像していなかった成果で、今後の研究に影響するので、第一年度は満足している。
第一年度は、当初の計画で必要な道具として挙げていたQBFソルバについては、QBFのコミュニティと共同研究なども行って、本研究の応用のいくつかをQBFの国際コンペティションでベンチマークとして利用されるようにもなっている。QBFの新しい研究にもつながる。
|
| Strategy for Future Research Activity |
本研究の目的は前述した論理式と探索と自動合成による計算限界解析である。特に形式論理と計算量理論を研究室いる計画研究A01班と最近大規模な探索問題の分散アルゴリズムについて共同研究している計画研究B02班と連結が強い。
従って、本研究の目的を達成するため本年度計画研究A01・B02班のメンバーなどと連携し、打ち合わせや共同研究が予想できる。または、計画研究班以外にも関係している研究者と相談・共同研究も重要でそれも続く。例えば、マサチューセッツ大学のイマーマン先生や最近共同研究をしているグーグルのカイザーさんとの関係の引き続きを続く。本研究ではQBFソルバが重要な道具であるため、QBFのコミュニティとの関係も重要になる。本研究の大規模な問題を解くためにも利用できるため、今年度は分散QBFソルバに関する共同研究も続き、従来の並列QBFソルバをはるかに超えるものについて研究する。QBFソルバは本研究だけではなく、広く使われるため本研究以外にもインパクトがあり、専用な実装より意味がある。
また、第一年度得られたモデルに関する論文は査読の遅さの影響があったが、今年度は早めにプリープリントやテクニカルレポートでも何かの形で公開する。第一年度と同様に本領域に参加するおかげで、自分がまだ想像していない共同研究や新しい分野への応用なども考えられる。特に、難しい計算問題を大規模なスパコンや分散システムで実際に解こうとする時の計算限界に興味があり、その限界をプッシュすることによって限界について考える。
|
Research Products
(6 results)
