| 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 |
SyGuS という競技会における Inv トラックで優勝できるレベルの高性能なソルバを作成することができた。これは当初の計画における最初のステップであり、これが目論見通り達成できたことになる。機械学習としては強化学習を用いており、素朴なアルゴリズムでも専門家が与えたヒューリスティクスや他の SyGuS の参加ソルバよりも高性能なソルバを作成することができ、さらに進んだアルゴリズムを使うことでさらに高性能なソルバを作ることができた。しかしながら SyGuS 競技会の内容が変更されたため、実際に競技会に参加して優勝することは叶わなかった。
この成果の意義は不変条件の発見というタスクにおいても機械学習技術が効果を発揮することを明らかにしたことにある。機械学習の演繹的推論への応用例は多いが、それらは不変条件の発見のような適切な論理式を発見するタスクを対象外または苦手とするか、あるいは適切な論理式の発見タスクを扱うが既存ソルバに比べて実行効率の面で劣っていた。不変条件の発見のようなタスクにおいても機械学習技術を援用することでソルバの効率を挙げられるということは、重要な発見である。
SyGuS に優勝するレベルのソルバができたことは重要な進展だが、一方でプログラム検証などへの応用を考えると、作成したソルバが完全に満足の行くものとまでは言えない。その理由は (1) SyGuS 競技会に参加していない非常に優秀なあるソルバと比べると必ずしも勝っているとは言えないこと、(2) SyGuS の Inv トラックの問題はある側面では比較的簡単な（正確にいうと未定述語が１つ）ものであり、応用法はこのクラスから外れる問題も多いこと、が挙げられる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
最初のステップとして位置づけていた、SyGuS 優勝レベルのソルバを作成することが、目論見通り達成できたため。
|
| Strategy for Future Research Activity |
当初の計画の通り順調に推移しているため、基本的には計画通りに研究を進める。特に重点的に取り組む課題として次を挙げる。
まずソルバをプログラム検証等の応用上重要な課題に直接適用できるようにすることである。重要な問題としては CHC 充足問題があり、これは SyGuS の Inv トラックの問題に近いが、未定述語の数が複数であるなどの違いがある。原理的には SyGuS の Inv トラックと CHC 充足問題の差は大きくはないはずだが、強化学習によって高性能ソルバを得るためには、状態空間が問題依存になる点や探索空間が広大になってしまうことへの対処方法が必要である。またプログラム検証の観点で重要な類似の問題として停止性検証問題があり、こちらについても類似の方法で高性能ソルバを作成できないかを検討する。
また強化学習が成功している要因の分析も行う。適切な論理式を推定するタスクに機械学習を応用する研究は多いが、既存ソルバに勝る効率のソルバを作成したという報告はほとんどない。我々の方法で効率のよいソルバを構成できた理由は、機械学習で推定するものが論理式そのものではなくて論理式のテンプレートであることが効いているものと思われる。この仮説を検討し、テンプレートの学習なら一般に上手く行くのかどうかや、テンプレートのどういう性質が学習を容易にしているのかを明らかにする。
|
Report
(1 results)
Research Products
(1 results)
