数学の自動化を推進するための機械学習を用いた定理自動証明手法

2021 Fiscal Year Annual Research 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

数学における証明のプロセスを計算機を用いて一部自動化することを目指した．当初の目標は命題の証明を二者間のゲームと捉える立場に立ち，ゲームAIに対する学習手法，特に強化学習のみを用いて自然数を含む命題を自動証明する手法の研究であった．しかし，研究を進めるにつれて，強化学習のみでは学習を収束させることが難しく，安定的に十分な性能を得ることが困難であることが分かってきた．そのため，本研究では機械学習を用いることなく実装されている自動定理証明器を強化学習によって高性能化する方向で研究を進めた．具体的には，自動定理証明器 PCSat が内部で用いているヒューリスティクスを強化学習によって高性能化する研究を行った．PCSat は二階の自由な述語変数を含む自然数上の述語が与えられると，全体の制約が妥当となるような，述語変数に対して代入すべき述語を探索することによって証明を行う．この探索を行う際のヒューリスティクスを強化学習によって学習する手法を研究した．研究においては PCSat の挙動をマルコフ決定過程として抽象化し，証明が成功するまでにかかる時間の-1倍を報酬として，報酬を最大化するようなポリシーを学習した．学習法としてモンテカルロ法とアクタークリティック法を用いたところ，ベンチマークとして用いた問題セットにおいて，世界トップレベルの証明器に匹敵する性能を持つヒューリスティクスが得られた．この結果は機械学習の自動証明器の高性能化に対する有効性をある程度示していると考えられる．本研究の成果は論文としてまとめ，現在投稿中であり，プレプリントとして https://arxiv.org/abs/2107.09766 に公開している．