2020 Fiscal Year Annual Research Report
Program Verification Techniques for the AI Era
| Project/Area Number |
20H05703
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
小林 直樹 東京大学, 大学院情報理工学系研究科, 教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
吉仲 亮 東北大学, 情報科学研究科, 准教授 (80466424)
佐藤 一誠 東京大学, 大学院情報理工学系研究科, 准教授 (90610155)
佐藤 亮介 東京大学, 大学院情報理工学系研究科, 助教 (10804677)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
|
|---|
| Project Period (FY) |
2020-08-31 – 2025-03-31
|
| Keywords | 高階モデル検査 / プログラム検証 / 高階不動点論理 / 機械学習 |
|---|
| Outline of Annual Research Achievements |
研究課題全体を(A)高階モデル検査をはじめとするプログラム検証理論・技術のさらなる発展、(B)プログラム検証への機械学習技術の応用、(C)質の変化したプログラムの検証手法、の3つの課題に分けて並行して研究を進めた。2020年度の主な研究実績（一部、繰越分として2021年度に実施した成果を含む）は以下のとおり。
(A)プログラム検証技術の発展：高階モデル検査の一種である高階不動点論理HFL(Z)の真偽値判定に基づくプログラム検証の統一的枠組みについての研究を進め、HFL(Z)の真偽値判定手法およびその実装を進めた。また、ポインタを扱うプログラムの検証のため、所有権型を持つプログラムの検証問題を、不動点論理の一種であるCHCの充足可能性判定問題に帰着する手法の改良や、"Relational Verification"と呼ばれる、複数のプログラムまたはプログラムの複数の実行間の関係を検証する手法の研究を行い、そられの有効性を確認した。
(B)プログラム検証への機械学習技術の応用：(A)で触れたCHCの充足可能性判定器の改良のため、(i)解の候補のテンプレートの選択に強化学習を応用する方式、(ii)正例・負例データをもとにニューラルネットワークを学習させ、その重み情報を利用して解の候補を発見する方式（NeuGuS: Neural Network Guided Synthesis）を考案し、そられの実装・実験を行って有効性を確認した。
(C)質の変化したプログラムの検証手法： (B)のNeuGuSの枠組みを利用し、一部がオラクルとして未定のプログラムとその仕様を入力とし、オラクル部分の式を自動発見する仕組みを考案し、予備実験を行った。また、確率付きプログラムの検証のための基礎として、確率付き高階不動点論理について研究を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要に述べた通り順調に研究成果が出ており、一流の国際ジャーナルや国際会議に論文を発表している。
COVID-19により、海外からの研究員の雇用などの遅れなどの影響は出ているものの、理論面の検討などを先に進める等の調整によって、研究全体としては順調に進展している。
|
| Strategy for Future Research Activity |
前項でも述べたとおり、COVID-19の影響によって海外からの研究員の雇用が遅れ、担当予定の実験等の部分について遅れが生じているが、理論面の検討を先に進めることにより対処し、全体として最終年度までに当初の計画またはそれ以上の成果が得られるようにする。
|
