2019 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 |
数学的な定理の自動証明手法への機械学習の適用について検討を行った．今年度は主に強化学習によって自動証明器，特にホーン節ソルバを従来手法より高性能化できるかどうかについて実験を行った．その結果，ホーン節ソルバの内部状態の情報を用いて，ホーン節ソルバの動作を誘導するポリシーを学習することで，従来手法の証明器の性能を向上することができる見込みが得られた．ポリシーを手動で作り込むことで証明器の性能が向上することは確認できており，少なくともこのポリシーを学習することができれば高性能化が可能になると期待される．そこで今後は，この方向の研究を進め，(1) ポリシーの学習に有用な内部状態情報の同定と (2) 本問題でのポリシーの学習に適した手法の検討を進めたいと考えており，最終的にホーン節ソルバのためのベンチマークで実験的に有用性を確認したいと考えている．
また，付随する研究として RNN からその動作を模倣する重み付き有限状態オートマトン (WFA) を抽出する研究を行い，その成果をAAAI'20にて発表した．この研究は，オートマトン学習手法であるAngluinのアルゴリズムに着想を得て，これをRNNからのWFAの抽出に応用したものであり，その有効性を実験的に確認した．本研究は直接的に定理を機械学習によって証明しようとする手法ではないものの，RNN という機械学習における道具と，オートマトンという記号を扱う道具を結びつける手法としての意義がある．
|
| 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 |
今年度行ったホーン節ソルバの高性能化の実験を進め，強化学習に基づく自動証明手法の研究として結実させることを検討している．また，別途末永が代表となって進めている基盤Bの研究においても，自動証明に類する研究の発想が出つつあり，そちらとのシナジーを得ることも考えている．
|
| Causes of Carryover |
国際会議参加が見込みより少なかったために次年度使用額が生じた．来年度は実験に要する費用と国際会議参加を積極的に行う予定である．新型コロナウイルスの影響により国際会議の参加が難しい場合は，実験用の計算機を購入し，より実験を効率的に行うことを検討する．
|
Research Products
(2 results)
