| 研究課題/領域番号 |
19K22842
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| 研究分担者 |
塚田 武志 東京大学, 大学院情報理工学系研究科, 助教 (50758951)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| 研究期間 (年度) |
2019-06-28 – 2022-03-31
|
| キーワード | プログラム検証 / 定理証明 / 機械学習 / 強化学習 |
|---|
| 研究実績の概要 |
本年度は主に定理証明の重要な応用であるプログラム検証器の高性能化に機械学習を適用する研究を行った．具体的には，自動検証手法の内部で用いられているヒューリスティクスのチューニングを機械学習を用いて行う手法を研究した．この手法は，CEGIS と呼ばれる検証手法において用いられているヒューリスティクスを強化学習によって自動的に学習する手法である．このヒューリスティクスは，従来は人手でアドホックにチューニングされていたが，これを自動的にチューニングし高性能なヒューリスティクスを得る手法を提案した.
この手法を検証器 PCSat に実装し，自動検証分野の標準的なベンチマークである SyGuS-Comp によって評価した．評価にあたっては，現在このベンチマークで世界トップレベルのツールである CVC4 と比較した．その結果，強化学習により学習されたヒューリスティクスを用いる PCSat の性能は，CVC4 の性能を超えた. この結果は，強化学習により検証器のヒューリスティクスを改善する研究としては新規なものであり，その有用性が実験によって確かめられた点で意義深い．この成果を論文にまとめて投稿中である.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
上述した機械学習の検証器への適用によって，良い成果が得られている．
|
| 今後の研究の推進方策 |
上述の成果を発展させる形で研究を行う．具体的には，より複雑なプログラムのより複雑な性質を検証する手法の研究や，定理証明器に対する本手法の適用を行う予定である．
|
| 次年度使用額が生じた理由 |
新型コロナウイルスの影響で旅費の使用がなかったため．
|
