Automated Theorem Proving with Machine Learning for Automating Mathematics

2021 Fiscal Year Final Research Report

• Project/Area Number: 19K22842
• Research Category: Grant-in-Aid for Challenging Research (Exploratory)
• Allocation Type: Multi-year Fund
• Review Section: Medium-sized Section 60:Information science, computer engineering, and related fields
• Research Institution: Kyoto University
• Principal Investigator: Suenaga Kohei 京都大学, 情報学研究科, 准教授 (70633692)
• Co-Investigator(Kenkyū-buntansha): 塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951) ; 関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
• Project Period (FY): 2019-06-28 – 2022-03-31
• Keywords: 強化学習 / 自動証明 / 制約付きホーン節

Outline of Final Research Achievements

We aimed at partially automating proof tasks in mathematics. As the first step towards this goal, we studied automatic proof methods for constraints expressed as constrained linear Horn clauses (CHC) on integers. In particular, we used reinforcement learning to speed up predicate discovery, which is an essential step in solving CHCs. For this purpose, we reformulated CEGIS as an MDP and learned the heuristics used by a solver by reinforcement learning. We used the negative value of the time spent by the solver to solve the CHC constraint as the reward. The results showed that the heuristics outperformed carefully tuned human solvers in terms of both the number of constraints solved and execution time.

Free Research Field

プログラム検証

Academic Significance and Societal Importance of the Research Achievements

近代の自然科学や産業の発展は，数学を用いて抽象力と信頼性の高い理論を構築し，その理論を様々な分野に適用することにより支えられているといっても過言ではない．また，証明支援はプロパーな数学にとってのみ重要なわけではなく，自動プログラム検証手法においてもコアな技術となっている．本研究の成果は記号処理に基づく自動証明手法と統計的機械学習に基づくヒューリスティクス探索が2つの潮流を合流させるためのスイートスポットであることを示すものである．この成果をベースとして，より複雑かつ非自明な自動証明手法につなげることで，数学に対しても形式検証に対してもインパクトを与える手法が得られるものと期待される．