| 研究課題/領域番号 |
19K22842
|
|---|
| 研究種目 |
挑戦的研究(萌芽)
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
中区分60:情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
|
|---|
| 研究分担者 |
塚田 武志 千葉大学, 大学院理学研究院, 准教授 (50758951)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| 研究期間 (年度) |
2019-06-28 – 2022-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
6,240千円 (直接経費: 4,800千円、間接経費: 1,440千円)
2021年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2019年度: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
|
|---|
| キーワード | 強化学習 / 自動証明 / 制約付きホーン節 / 機械学習 / プログラム検証 / 定理証明 / ホーン節ソルバ / 人工知能 / 深層学習 |
|---|
| 研究開始時の研究の概要 |
数学における証明のを計算機を用いて一部自動化することを目指します．本申請課題は，この最終目標に対する探索研究として，自然数に関する命題の証明の一部自動化を目指します．本申請課題では，証明が二者ゲームとして定式化でき，したがってゲーム AI の学習手法を証明ゲームに適用することで有能な自動証明アルゴリズムを錬成できるのではないか，というアイデアに基づいて研究を進めます．自動証明は様々なシステムが意図通りに動作することを保証するための要素技術として用いられており，その点で将来的に産業的なインパクト・貢献の可能性が期待できると考えています．
|
| 研究成果の概要 |
本研究においては，数学における証明タスクを計算機によって一部自動化することを最終的な目標とし，整数上の制約付き線形ホーン節 (CHC) と呼ばれる形式で記述された制約のための自動証明手法の研究を行った．特に CHC を解く上で重要な述語発見を高速化するために強化学習を用いた．そのために CEGIS を強化学習の問題として再定式化し，CHC制約をソルバが解くまでの時間の負値を報酬とした上で，強化学習によってソルバが用いるヒューリスティクスを学習した．その結果，人手によって注意深くチューニングされたソルバを，解けた制約数の点でも実行時間の点でも上回るヒューリスティクスが得られうことを示した．
|
| 研究成果の学術的意義や社会的意義 |
近代の自然科学や産業の発展は，数学を用いて抽象力と信頼性の高い理論を構築し，その理論を様々な分野に適用することにより支えられているといっても過言ではない．また，証明支援はプロパーな数学にとってのみ重要なわけではなく，自動プログラム検証手法においてもコアな技術となっている．本研究の成果は記号処理に基づく自動証明手法と統計的機械学習に基づくヒューリスティクス探索が2つの潮流を合流させるためのスイートスポットであることを示すものである．この成果をベースとして，より複雑かつ非自明な自動証明手法につなげることで，数学に対しても形式検証に対してもインパクトを与える手法が得られるものと期待される．
|
