2020 Fiscal Year Research-status Report
数学の自動化を推進するための機械学習を用いた定理自動証明手法
| Project/Area Number |
19K22842
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
塚田 武志 東京大学, 大学院情報理工学系研究科, 助教 (50758951)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| Project Period (FY) |
2019-06-28 – 2022-03-31
|
| Keywords | プログラム検証 / 定理証明 / 機械学習 / 強化学習 |
|---|
| Outline of Annual Research Achievements |
本年度は主に定理証明の重要な応用であるプログラム検証器の高性能化に機械学習を適用する研究を行った．具体的には，自動検証手法の内部で用いられているヒューリスティクスのチューニングを機械学習を用いて行う手法を研究した．この手法は，CEGIS と呼ばれる検証手法において用いられているヒューリスティクスを強化学習によって自動的に学習する手法である．このヒューリスティクスは，従来は人手でアドホックにチューニングされていたが，これを自動的にチューニングし高性能なヒューリスティクスを得る手法を提案した.
この手法を検証器 PCSat に実装し，自動検証分野の標準的なベンチマークである SyGuS-Comp によって評価した．評価にあたっては，現在このベンチマークで世界トップレベルのツールである CVC4 と比較した．その結果，強化学習により学習されたヒューリスティクスを用いる PCSat の性能は，CVC4 の性能を超えた. この結果は，強化学習により検証器のヒューリスティクスを改善する研究としては新規なものであり，その有用性が実験によって確かめられた点で意義深い．この成果を論文にまとめて投稿中である.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
上述した機械学習の検証器への適用によって，良い成果が得られている．
|
| Strategy for Future Research Activity |
上述の成果を発展させる形で研究を行う．具体的には，より複雑なプログラムのより複雑な性質を検証する手法の研究や，定理証明器に対する本手法の適用を行う予定である．
|
| Causes of Carryover |
新型コロナウイルスの影響で旅費の使用がなかったため．
|
