| Project/Area Number |
23K24820
|
|---|
| Project/Area Number (Other) |
22H03564 (2022-2023)
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Multi-year Fund (2024)
Single-year Grants (2022-2023) |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
海野 広志 東北大学, 電気通信研究所, 教授 (80569575)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
|
|---|
| Project Period (FY) |
2022-04-01 – 2027-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥17,290,000 (Direct Cost: ¥13,300,000、Indirect Cost: ¥3,990,000)
Fiscal Year 2026: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2025: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2024: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2023: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2022: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
|
|---|
| Keywords | 演繹的推論 / 機械学習 / 定理自動証明 / プログラム検証 / CHCソルバ / システム検証 |
|---|
| Outline of Research at the Start |
本研究では、近年著しい発展を遂げている機械学習技術を数理論理学的な問題に応用して、高効率な演繹的推論エンジンを構成することを目指す。機械学習技術は言語処理やゲームAIを含む様々な分野で著しい成功を遂げているが、証明などの演繹的推論が関わる分野には未だに古典的な演繹的推論技術が機械学習技術に優位である問題が多い。これまでの研究では解きたい問題を直接解く機械学習モデルを作る End-to-End の方法が主流であったが、本研究では解きたい問題ではなく機械学習に適した問題を学習させて、学習結果を演繹的推論エンジンで活用する。
|
| Outline of Annual Research Achievements |
停止性検証という発展的な問題のソルバを補助するためのモジュールを機械学習技術を利用して作成し、停止性検証競技会（Termination Competition 2023）に参加し Integer Transition Systems 部門で２位などの成績を収めるなど一定の成果を上げた。しかしながらベースとしている MuVal というソルバの人間によるヒューリスティクスを超えておらず、その面ではまだ不十分な結果となっている。
昨年度の成果である SyGuS の Inv トラックの場合と異なり、停止性検証の補助については人間によるヒューリスティクスを超えられていない。これは学習に問題があるためであると考えており、年度の後半は原因の分析を進めてきた。最も主要な問題だと考えているのはエージェントが複数存在する環境下での強化学習としてソルバ補助モジュールの学習が定式化されている点であり、マルチエージェント強化学習の既存技術を利用することでの問題解決に向けて研究を進めている。別の解決策としてマルチエージェントとしての定式化を止め、単一のエージェントが全体を制御する形の定式化を採用する方法も検討している。マルチエージェント以外の原因の候補としては、環境からの情報の不足によって partially observed な設定となっていることも原因の候補に挙がっており、こちらの視点からの問題克服も同時に検討している。
停止性検証以外にも（一般の）制約付きホーン制約充足問題（CHC）の開発も並行して進めているが、こちらについても停止性問題の場合と同様の学習上の問題が生じており、停止性検証の学習上の問題の克服と並行して原因の分析と対策を検討している。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
本年度の当初の予定の通りに停止性検証競技会への参加し一定の成績を収めることはできたものの、ホーン節制約充足問題や停止性問題のための機械学習技術の適用には重要な課題を残しているため。
|
| Strategy for Future Research Activity |
停止性検証やホーン節制約充足問題のソルバを補助するためのより良いモジュールの開発を目指して、現状で残されている学習上の課題を克服して人間のヒューリスティクスよりも優れたものを開発する。これは「研究実績の概要」でも述べたマルチエージェントや partially observed という設定を克服するということであり、どちらも機械学習分野の蓄積があるため、既存のアイデアを本研究課題の設定に合うように応用することで克服を試みる。
|
