2019 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 / 深層学習 |
|---|
| Outline of Annual Research Achievements |
有限幾何と（平面）射影幾何、及びトポロジーの証明支援系を用いた形式化において、深層学習を適用して次のtacticを予想するために、証明支援系Coq/Ssreflectと深層学習システム（TensorFlow）をプログラムするpythonを効率的に連携させる必要がある。我々のpexpectを用いた暫定的な方法では、学習が十分収束するような結果が得られなかった。そこで、より直接的にcoq とtensorflowを連携するために、基本的にはS式で連携するserapi の使用が必要になった。そこで、K. Yang と J. Deng が2019年に発表したCoqGymと、D. Huang達が2018年に発表した定理証明のためのGamePadの使用を検討した。このうち、GamePadを用いて、特に有限幾何において、深層学習を行なったが、既存の結果をさらに改善するような結果は得られなかった。そこで、我々はこれらの「tactic ベース」の学習は近視眼的学習になるので、どうしても限界があり、見通しの立つ学習を成功させるためには、これまでに証明された定理を収集し、証明の各コンテキストで、どの定理が最も有用かを予想する学習に移行する必要があると考えるに至った。これを「theoremベース」の学習と呼ぶことにすると、このためには、極めて簡単で基礎的な定理群から、長大な証明の末に得られる定理まで、多くの定理を収集することが最初の仕事となる。そこで花輪和孝氏から技術的サポートを得て、http://163.43.192.18:8000（現在非公開）にDjangoサーバを構築し、proofwiki及びarxivの数学データベースを作り、proofwikiデータの定理と証明の分離、定理検索機能を備えた。同時にウェブ上でcoqを使うjscoqを配置し,形式化された証明の保存機能も作成した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要で述べたように、既存の「tacticベース」の深層学習から、学習効率の改善が見られないことを確認し、我々が「theoremベース」と呼ぶ学習に方針を変えた。多くの既存の定理は形式化されていないが、「theoremベース」ではそれをいわば公理的に前提に置く事で「相対的形式化」による学習を行う。従って、形式化されているかどうかを問わず、既存の定理をできるだけ多く集めて、データベース化することが重要となった。また、証明支援系coqと、深層学習フレームワーク（tenforflow, しかし我々はpytorchに移行しつつある）をサーバにおいて、ウェッブ上から深層学習結果を用いた定理検索を行うシステムの構築が重要となった。そこで花輪和孝氏から技術的サポートを得て、http://163.43.192.18:8000（現在非公開）に、定理証明支援系と、深層学習フレームワークとの連携の観点からDjangoサーバを構築し、proofwiki及びarxivの膨大な数学データベースを作り、proofwikiデータの定理と証明の分離、定理検索機能を備えた。同時にウェブ上でcoqを使うjscoqを配置し,形式化された証明の保存機能も作成した。これによって、「theoremベース」の深層学習環境が整いつつある。
|
| Strategy for Future Research Activity |
「tacticベース」の学習から「theoremベース」の証明に移行するために、次の３点で研究を進める必要がある。第1は、有効な”theorem embedding"を得ること。これは自然言語処理での"word embedding"に対応するもので、theorem、より一般にpropositionをできるだけ小さい有限次元のベクトル空間で表現するプロセスである。ここで一つの理論的問題として、与えられた命題の族に対し、その"one hot"表現を入力と出力にもつオートエンコーダーで、入力に対し、出力は、入力と同値の命題であれば正解という条件で学習を行う時、中間の隠れ層の次元の最小値は何か？が考えられる。我々のプロジェクトはこれに対し理論的解答を得ることが主眼ではないが、試行錯誤によって、最小次元に近い隠れ層を用いることで、より有効なtheorem embeddingを実現することを考えている。第2は、深層学習アルゴリズムの改善である。我々はRNNベース、より正確にはLSTMベースのtactic予想アルゴリズムを考えていたが、最近２年間の"attention"アルゴリズムの進展は目覚しく、attention/transformerを用いて(証明の各ステップで適用する)theorem/lemma/proposition予想アルゴリズムに切り替える。より具体的には、(coqにLtacを埋め込んだtcoqを用いて形式化を行う）gamepadで用いられている"torchfold"を"transfomer"に置き換えることで、それができると考えている。第３は、すでに構築中のデータベースに、さらに多くの既存定理のデータを加えていくこと。またウェッブからの検索アルゴリズム、及び証明支援系(coq)で扱うシステムの構築である。以上の3点について研究を進めていく。
|
| Remarks |
著作権の問題が解決していない等の理由により、セキュリティーコードを設定している。
|
Research Products
(2 results)
