| 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
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥6,240,000 (Direct Cost: ¥4,800,000、Indirect Cost: ¥1,440,000)
Fiscal Year 2021: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
|
|---|
| Keywords | 強化学習 / 自動証明 / 制約付きホーン節 / 機械学習 / プログラム検証 / 定理証明 / ホーン節ソルバ / 人工知能 / 深層学習 |
|---|
| Outline of Research at the Start |
数学における証明のを計算機を用いて一部自動化することを目指します．本申請課題は，この最終目標に対する探索研究として，自然数に関する命題の証明の一部自動化を目指します．本申請課題では，証明が二者ゲームとして定式化でき，したがってゲーム AI の学習手法を証明ゲームに適用することで有能な自動証明アルゴリズムを錬成できるのではないか，というアイデアに基づいて研究を進めます．自動証明は様々なシステムが意図通りに動作することを保証するための要素技術として用いられており，その点で将来的に産業的なインパクト・貢献の可能性が期待できると考えています．
|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
近代の自然科学や産業の発展は，数学を用いて抽象力と信頼性の高い理論を構築し，その理論を様々な分野に適用することにより支えられているといっても過言ではない．また，証明支援はプロパーな数学にとってのみ重要なわけではなく，自動プログラム検証手法においてもコアな技術となっている．本研究の成果は記号処理に基づく自動証明手法と統計的機械学習に基づくヒューリスティクス探索が2つの潮流を合流させるためのスイートスポットであることを示すものである．この成果をベースとして，より複雑かつ非自明な自動証明手法につなげることで，数学に対しても形式検証に対してもインパクトを与える手法が得られるものと期待される．
|
