| 研究課題/領域番号 |
19H04084
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| 研究分担者 |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
海野 広志 筑波大学, システム情報系, 准教授 (80569575)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2024-03-31
|
| キーワード | プログラム検証 / 強化学習 / 機械学習 |
|---|
| 研究実績の概要 |
本年は特に課題B（人間による自動検証支援手法）について，大きな進捗があった．人間により自動検証支援を行う当初の計画に関連する研究として，提案時に人間が行うことを予定していた自動検証手法への操作を機械学習を用いて行う手法を研究した．この手法は，CEGIS と呼ばれる検証手法において用いられているヒューリスティクスを強化学習によって自動的に学習する手法である．このヒューリスティクスは，従来は人手でアドホックにチューニングされていたが，これを自動的にチューニングし高性能なヒューリスティクスを得る手法を提案した．
この手法を検証器 PCSat に実装し，自動検証分野の標準的なベンチマークである SyGuS-Comp によって評価した．評価にあたっては，現在このベンチマークで世界トップレベルのツールである CVC4 と比較した．その結果，強化学習により学習されたヒューリスティクスを用いる PCSat の性能は，CVC4 の性能を超えた．この結果は，強化学習により検証器のヒューリスティクスを改善する研究としては新規なものであり，その有用性が実験によって確かめられた点で意義深い．この成果を論文にまとめて投稿中である．
ハイブリッドシステムの検証に関しては引き続き手法の検討を継続しており，今年度の課題Bの成果の適用を視野に入れつつ研究を行っている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
上述した成果は検証器で用いられているヒューリスティクスを機械学習により改善する手法としては新規なものであり，その効果も大きい．
|
| 今後の研究の推進方策 |
上記の研究成果をベースとして，より複雑なプログラムの複雑な性質の検証を効率よく行う手法の研究に発展させる．また，当初のターゲットであるハイブリッドシステムへの適用も行う．
|
