| 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) |
2024-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 ソルバ / システム検証 / CHCソルバ |
|---|
| Outline of Research at the Start |
本研究では、近年著しい発展を遂げている機械学習技術を数理論理学的な問題に応用して、高効率な演繹的推論エンジンを構成することを目指す。機械学習技術は言語処理やゲームAIを含む様々な分野で著しい成功を遂げているが、証明などの演繹的推論が関わる分野には未だに古典的な演繹的推論技術が機械学習技術に優位である問題が多い。これまでの研究では解きたい問題を直接解く機械学習モデルを作る End-to-End の方法が主流であったが、本研究では解きたい問題ではなく機械学習に適した問題を学習させて、学習結果を演繹的推論エンジンで活用する。
|
| Outline of Annual Research Achievements |
本研究計画は機械学習技術を用いて高速な演繹的推論エンジンの作成を目指すものである。本年度は主に次の２つの成果を得た。
第一に、機械学習などで頻繁に利用される双対性原理をプログラム検証の文脈でも見出すことができることを明らかにした。実際に様々なプログラム検証関連の手続きが Lagrange 双対性を利用したものであると見るすることができ、これによって多くの手続きを見通し良く理解することが可能になった。機械学習技術とプログラム検証のための演繹的手続きの関連を明らかにしたことにより、機械学習技術を演繹的手続きに適用するための新機軸に繋がることが期待される。この成果はプログラミング言語分野のトップ会議である Principles of Programming Languages に採択され、Distinguished paper award を受賞した。
第二に、重要な論理的問題である充足可能性問題 (SAT) の高階版である高階 SAT という問題の新しい解法を提案した。この問題は有用で様々な応用を持つが、残念ながら解くのが困難（TOWER-complete）であり、そのためもあってソルバが存在していなかった。我々はこの問題に対するはじめてのソルバを与えた。その方針は TOWER-complete な別の問題である高階モデル検査に帰着して高階モデル検査のためのソルバを利用するというものである。本研究は人工知能分野の主要国際会議である AAAI に採択された。この成果には、ソルバのなかった問題のソルバを開発したという側面の他に、高階モデル検査の新しい応用例という側面もある。我々の提案する帰着の像に含まれるような高階モデル検査問題の解法の効率化が課題となるが、ここに機械学習技術が利用できないかは面白い問である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の研究計画で主要なターゲットとしていた CHC ソルバや停止性検証機の開発についてはまだ克服できていない技術的困難があるものの、当初計画では予想外であったところで機械学習技術と演繹的推論技術の交わるところを見つけることができた。この結果はトップ会議で distinguished paper award を取るなど高く評価され、この成果を推し進める形での機械学習技術の演繹的推論への応用という新しい道がひらけた。
計画外の困難と計画外の新展開があったが、全体の研究成果としては主要国際会議において複数本の論文発表という目覚ましい成果を上げており、おおむね順調に進展しているといえる。
|
| Strategy for Future Research Activity |
今年度は次の２つの方向での研究の進展を目指す。
第一の方向は当初計画に沿う方向であり、MuVal などの演繹的推論エンジンの高速化のための機械学習技術の適用を目指す。ベースとなるソルバである MuVal 等は順調に開発が進んでおり、停止性検証等の競技会で一位を取ることもあるなど重要度が高まっており、これの高速化を目指す本研究計画の意義は増している。線形 CHC と呼ばれるクラスについては効率化に一定程度成功しており、線形 CHC の範囲を超えて非線形 CHC や停止性検証なども効率化することが課題である。
第二の方向は、2024年度の研究成果であるプログラム検証器などの演繹的推論手続きを Lagrange 双対性に基づく視点から分析することを通じたものである。これまでの研究では、いくつかの比較的簡単な演繹的推論手続きを分析したのみだが、この分析の適用範囲を広げたり分析の深さを深めたりすることで、新たな効率化の余地や機械学習技術の適用可能性が生じることを期待している。
|
