| 研究課題/領域番号 |
22H03564
|
|---|
| 配分区分 | 補助金 |
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
|
|---|
| 研究分担者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2027-03-31
|
| キーワード | 演繹的推論 / 機械学習 / CHCソルバ / プログラム検証 |
|---|
| 研究実績の概要 |
SyGuS という競技会における Inv トラックで優勝できるレベルの高性能なソルバを作成することができた。これは当初の計画における最初のステップであり、これが目論見通り達成できたことになる。機械学習としては強化学習を用いており、素朴なアルゴリズムでも専門家が与えたヒューリスティクスや他の SyGuS の参加ソルバよりも高性能なソルバを作成することができ、さらに進んだアルゴリズムを使うことでさらに高性能なソルバを作ることができた。しかしながら SyGuS 競技会の内容が変更されたため、実際に競技会に参加して優勝することは叶わなかった。
この成果の意義は不変条件の発見というタスクにおいても機械学習技術が効果を発揮することを明らかにしたことにある。機械学習の演繹的推論への応用例は多いが、それらは不変条件の発見のような適切な論理式を発見するタスクを対象外または苦手とするか、あるいは適切な論理式の発見タスクを扱うが既存ソルバに比べて実行効率の面で劣っていた。不変条件の発見のようなタスクにおいても機械学習技術を援用することでソルバの効率を挙げられるということは、重要な発見である。
SyGuS に優勝するレベルのソルバができたことは重要な進展だが、一方でプログラム検証などへの応用を考えると、作成したソルバが完全に満足の行くものとまでは言えない。その理由は (1) SyGuS 競技会に参加していない非常に優秀なあるソルバと比べると必ずしも勝っているとは言えないこと、(2) SyGuS の Inv トラックの問題はある側面では比較的簡単な（正確にいうと未定述語が１つ）ものであり、応用法はこのクラスから外れる問題も多いこと、が挙げられる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
最初のステップとして位置づけていた、SyGuS 優勝レベルのソルバを作成することが、目論見通り達成できたため。
|
| 今後の研究の推進方策 |
当初の計画の通り順調に推移しているため、基本的には計画通りに研究を進める。特に重点的に取り組む課題として次を挙げる。
まずソルバをプログラム検証等の応用上重要な課題に直接適用できるようにすることである。重要な問題としては CHC 充足問題があり、これは SyGuS の Inv トラックの問題に近いが、未定述語の数が複数であるなどの違いがある。原理的には SyGuS の Inv トラックと CHC 充足問題の差は大きくはないはずだが、強化学習によって高性能ソルバを得るためには、状態空間が問題依存になる点や探索空間が広大になってしまうことへの対処方法が必要である。またプログラム検証の観点で重要な類似の問題として停止性検証問題があり、こちらについても類似の方法で高性能ソルバを作成できないかを検討する。
また強化学習が成功している要因の分析も行う。適切な論理式を推定するタスクに機械学習を応用する研究は多いが、既存ソルバに勝る効率のソルバを作成したという報告はほとんどない。我々の方法で効率のよいソルバを構成できた理由は、機械学習で推定するものが論理式そのものではなくて論理式のテンプレートであることが効いているものと思われる。この仮説を検討し、テンプレートの学習なら一般に上手く行くのかどうかや、テンプレートのどういう性質が学習を容易にしているのかを明らかにする。
|
