| 研究課題/領域番号 |
22H03564
|
|---|
| 配分区分 | 補助金 |
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
|
|---|
| 研究分担者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
|
|---|
| 研究期間 (年度) |
2022-04-01 – 2027-03-31
|
| キーワード | 演繹的推論 / 機械学習 / 定理自動証明 / プログラム検証 |
|---|
| 研究実績の概要 |
停止性検証という発展的な問題のソルバを補助するためのモジュールを機械学習技術を利用して作成し、停止性検証競技会（Termination Competition 2023）に参加し Integer Transition Systems 部門で２位などの成績を収めるなど一定の成果を上げた。しかしながらベースとしている MuVal というソルバの人間によるヒューリスティクスを超えておらず、その面ではまだ不十分な結果となっている。
昨年度の成果である SyGuS の Inv トラックの場合と異なり、停止性検証の補助については人間によるヒューリスティクスを超えられていない。これは学習に問題があるためであると考えており、年度の後半は原因の分析を進めてきた。最も主要な問題だと考えているのはエージェントが複数存在する環境下での強化学習としてソルバ補助モジュールの学習が定式化されている点であり、マルチエージェント強化学習の既存技術を利用することでの問題解決に向けて研究を進めている。別の解決策としてマルチエージェントとしての定式化を止め、単一のエージェントが全体を制御する形の定式化を採用する方法も検討している。マルチエージェント以外の原因の候補としては、環境からの情報の不足によって partially observed な設定となっていることも原因の候補に挙がっており、こちらの視点からの問題克服も同時に検討している。
停止性検証以外にも（一般の）制約付きホーン制約充足問題（CHC）の開発も並行して進めているが、こちらについても停止性問題の場合と同様の学習上の問題が生じており、停止性検証の学習上の問題の克服と並行して原因の分析と対策を検討している。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
本年度の当初の予定の通りに停止性検証競技会への参加し一定の成績を収めることはできたものの、ホーン節制約充足問題や停止性問題のための機械学習技術の適用には重要な課題を残しているため。
|
| 今後の研究の推進方策 |
停止性検証やホーン節制約充足問題のソルバを補助するためのより良いモジュールの開発を目指して、現状で残されている学習上の課題を克服して人間のヒューリスティクスよりも優れたものを開発する。これは「研究実績の概要」でも述べたマルチエージェントや partially observed という設定を克服するということであり、どちらも機械学習分野の蓄積があるため、既存のアイデアを本研究課題の設定に合うように応用することで克服を試みる。
|
