| 研究課題/領域番号 |
23700164
|
|---|
| 研究機関 | 山梨大学 |
|---|
研究代表者 |
鍋島 英知 山梨大学, 医学工学総合研究部, 准教授 (10334848)
|
|---|
| 研究期間 (年度) |
2011-04-28 – 2014-03-31
|
| キーワード | 結論発見 / 仮説発見 / 一階述語論理 / 命題論理 / 推論システム / 分割統治 |
|---|
| 研究概要 |
平成23年度は主に以下の2つの研究課題に関して取り組んだ．それぞれの実績概要を示す．1. 分割統治法に基づく直列版結論発見手続きの実現 結論発見手続き SOL タブロー法に分割統治法を導入した手法を考案した．提案手法では，タブローを部分タブローに分割し，それぞれ独立して直列に解いた後，部分問題の解集合を統合する．提案手法を実装し，一階の定理証明問題からすべての反駁を求める評価実験を行った結果，分割統治法を適用することで大きく求解数が向上することを確認した．また結論発見問題では，部分結論集合同士の統合が必要となるが，部分結論集合をトライにより表現し，統合時に重複する繰り返し計算を抑制することで，統合に必要な計算量が大きく改善できることを示した．2. 命題論理版 SOLAR のアルゴリズムの検討 命題論理版 SOLAR の実現のため，SOL タブロー手続きに，矛盾からの節学習やバックジャンプ法，高速単位伝搬等の手法を導入したソルバを試作し性能評価を行った．その結果，一階の SOLAR より性能は向上するものの，SAT ソルバーが対象とするような大規模問題ではスケーラビリティの点で難があることが判明した．そこで，SAT ソルバーを直接利用する反駁定理に基づく結論発見手法を考案した．この手法では，年々性能が向上するSATソルバーの高速性を直接利用可能であるとともに，最新SAT技術であるインクリメンタル探索や原因解析技術を用いて仮説候補を枝刈りし，またモデルやシンメトリーに基づく枝刈り手法を導入することでさらなる性能の向上が見込める．これらの技術の一部を実装した試作ソルバーを開発し，命題版 SOLAR よりも大きな性能向上が得られることを確認した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究実績の概要で示した2テーマのうち，「1. 分割統治法に基づく直列版結論発見手続きの実現」に関しては，直列版結論発見手続きを考案し，その実装もほぼ完了しており，計画通り進展している． また「2. 命題論理版 SOLAR のアルゴリズムの検討」に関しては，当初の計画では命題版 SOL タブロー法に最新 SAT 技術を導入した手法をもとに研究を進める予定であったが，試作ソルバーの性能評価実験よりスケーラビリティの点において今後の改善が困難であると判断し，SAT ソルバーを直接利用する反駁定理に基づく結論発見手法を考案するに至った．本手法では，各種の枝刈り手法を考案し，その一部をすでに実装済みであり，試作ソルバーも命題版SOLARよりも大きく性能が向上している．今後すでに考案済みのシンメトリーに基づく枝刈り手法を導入することで，さらなる性能の向上が期待できるため，本テーマに関しては当初の計画以上に進展していると判断している． 一方，平成23年度には，「3. トップダウン型とボトムアップ型推論手続きの融合手法の実現」に関しても検討を進める予定であった．SOL タブロー法は，トップダウン型推論手続きであり，探索順序に強い制約がある．この制約を緩和することで，具体的には探索完了の見込みの高いタブローから優先的に処理する手法を導入することで，性能改善の見込みがあるため，平成23年度に検討する予定であったが，上述のテーマ 2 に研究リソースを割いたため，十分に検討を進めることができなかった． 以上より，テーマ 1 に関しては順調に進展中であり，テーマ 2 に関しては計画以上に進展しており，テーマ 3 に関しては遅れているため，総合的におおむね順調と判断した．
|
| 今後の研究の推進方策 |
平成24年度は，前年度の成果を受けて以下の課題に取り組む． 1. 分割統治法に基づく共有メモリ環境での並列分散結論発見手続きの実現と評価：前年度に引き続き，分割統治法に基づく結論発見手法に関して，共有メモリ環境での並列分散処理の実現に取り組む．既存システムである SOLAR は，並列分散処理を前提としていないため，その再設計から取りかかる．また次年度にむけて非共有メモリ環境への拡張を前提とした設計とする．理論面においては，部分結論集合の統合において factoring 操作を再現する必要があり，その効率的処理に関して検討を進める． 2. トップダウン型とボトムアップ型推論手続きの融合手法の実現と，トップダウン型推論手続きへの制限資源下での探索戦略の導入：昨年度の課題であったトップダウン型とボトムアップ型推論手続きの融合に関しては，スケーラビリティ向上のために不可欠な技術であるので，今年度より検討を進める．ボトムアップ型推論手続きでは，探索完了の見込みの高いタブローを評価する尺度が必要とされるが，この評価尺度に基づき，優れた現実的探索戦略として知られる制限資源下での探索戦略の導入を図る． 3. 命題版結論発見システムの実装と評価：昨年考案したシンメトリーに基づく仮説枝刈り手法を実装する．またスケーラビリティの向上に伴い，膨大な結論の管理方法が問題となるため，その効率的な表現・操作手法について検討する．その後，ハードウェアやソフトウェアの検証問題などに応用し，性能を評価する． 4. SOLAR の結論発見能力を利用可能なスクリプト言語の開発：JRuby などの実用的スクリプト言語の Java による実装をベースに，SOLAR の結論発見能力，および一階述語論理における包摂チェックなどの各種操作を自然に利用可能なスクリプト言語を開発する．
|
| 次年度の研究費の使用計画 |
本研究では，各年度毎に大学院生2名を研究課題に割り当てるため，開発用計算機2台を年度毎に計上している．平成24年度も多くの実装作業が発生するため，2台の開発用計算機（2式×10万円，計20万円）を購入予定である．また研究成果発表のために，国内での成果発表費用（2回×2人×2.5万円，計10万円），ならびに外国での成果発表費用（1回×1人×25万円，計25万円）を計上している．さらに研究成果の投稿にかかる費用として5万円を計上している．
|
