2018 Fiscal Year Annual Research Report
| Project/Area Number |
18H05321
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
久我 健一 千葉大学, 大学院理学研究院, 教授 (30186374)
|
|---|
| Project Period (FY) |
2018-06-29 – 2022-03-31
|
| Keywords | 形式化 / 有限射影平面 / 証明支援システム / 深層学習 / 強化学習 / Coq / SSReflect / TensorFlow |
|---|
| Outline of Annual Research Achievements |
形式化の数学対象を公理的射影幾何学からさらに限定し、有限幾何学、有限射影平面、有限アフィン平面を設定し、大学院生の協力を得て、有限射影平面の位数の定義や関連する基礎的補題、定理群からなる基礎理論を、証明支援システムCOQ/SSReflectを用いて形式化した。これは通常の（人の手による対話的な）証明支援システムの使用によるものであるが、形式化自体に意味があるのと同時に、ニューラルネットの教師付き学習データの作成としての意味をもつ。これに並行して、証明支援システムをニューラル・ネットワーク（具体的には TensorFlowおよびKeras）と連携する方法として、pythonのsubprocessを用いて直接coqtopを実行する手法、COQ XML Protocolを用いて連携する手法、さらに開発途中の coq SerApiを用いてS式を介して連携する手法、の３手法について、技術的問題をほぼ解消し、簡単な例について試験的に実行した。また、alpha-zero generalのコードからモンテカルロ木探索の部分を抽出し、二人対戦ゲームとしての特殊性を排して、汎用性を持たせた。これを数学証明に適用するにあたり、マルコフ決定過程としての状態と行動をどのように設定するべきかについて考察し、行動設定の粒度レベルの自由度があることを認識した。行動の粒度を上げる方法として、Coqの局所言語Ltacを用いて自動性の高いtacticsを作成する方法を試験的に作成した。もっとも粒度が低い行動設定（行動=tactic)および限定したtacticを用いて、試験的に深層学習を実行したが、学習が収束するには至らなかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
この研究の課題を達成するためには、次の項目について研究・開発を行う必要がある。1. 適正な数学対象の設定と、証明支援系の通常の（対話的）使用による形式化の達成。2. 証明支援系と深層学習フレームワークの連携技術 3. 方策改善のためのモンテカルロ木探索法の実装 4. 粒度の高い（大きい）行動設定。このうち、1. については、公理的射影幾何学からさらに限定し、有限幾何、有限射影平面、有限アフィン幾何について、大学院生の協力を得て、有限射影平面の位数の定義や関連する基礎的補題、定理群からなる基礎理論を、証明支援システムCOQ/SSReflectを用いて形式化した。
2. については、pythonのsubprocessを用いて直接coqtopを実行する手法、COQ XML Protocolを用いて連携する手法、さらに開発途中の coq SerApiを用いてS式を介して連携する手法、の３手法について、技術的問題をほぼ解消し、簡単な例について試験的に実行した。3. についてはalpha-zero generalのコードからモンテカルロ木探索の部分を抽出し、二人対戦ゲームとしての特殊性を排して、汎用性を持たせた。4. についてはCoqの局所言語Ltacを用いて自動性の高いtacticsを作成する方法を試験的に作成した。これらを総合的に組み合わせて、目標としている数学証明の学習が収束するまでには至ってないが、そのための準備として概ね順調に進展していると考える。
|
| Strategy for Future Research Activity |
有限射影平面から無限射影平面に形式化を拡張子、さらにデザルグの公理を設定することによって、古典的な平面射影幾何を形式化する。これによって深層学習への教室付き学習データを増やせる。これとは別に、数学証明を（一人）ゲームとして状態と行動を設定するにあたり、行動の「粒度」を複数考えることによって、階層的な深層学習システムを考える。もっとも大きい粒度として、形式化された定理、補題がある。すなわち個々の定理をapplyすることをそれぞれの行動と考えることによって、学習効率が高くなることが期待される。そのために、定理を柔軟にapply可能な「行動定理」に書き換える必要がある。このためにCoqの局所言語Ltacを用いて、「定理」を「行動定理」に書き換える方法を開発する。全く新しい試みとして、定理・補題発見がある。各時点でのゴールにどのどのように補題を設定して証明すればいいのか、という問題である。これについてもモンテカルロ木探索法を利用した強化学習が有効であると考えている。行動の粒度が異なるいくつかのマルコフ決定過程を用意し、状況によって使い分け、協調的にニューラすネットの学習の収束が進むようにする。
|
Research Products
(2 results)
