2020 Fiscal Year Research-status Report
| Project/Area Number |
20K20340
|
|---|
| Allocation Type | Multi-year Fund |
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
久我 健一 千葉大学, 大学院理学研究院, 教授 (30186374)
|
|---|
| Project Period (FY) |
2020-04-01 – 2022-03-31
|
| Keywords | トポロジー / 数学の形式化 / 証明支援系 / 機械学習 |
|---|
| Outline of Annual Research Achievements |
現在行われている機械学習（特に深層学習）では一般に膨大なデータを必要とする一方で、インターネット上の数学証明データは少なく、かつ証明に利用できる形のデータはさらに少ない。そこで、機械学習を用いて証明支援系による定理証明の形式化を行う前提として必要な有効な（機械で使用可能な）数学データの選定と収集を行い、同時にデータ整形と、検索プログラムの実装を行なった（この研究では花輪和孝氏の協力を得ている）。数学データとしては、ProofWiki (https://proofwiki.org/wiki/), nLab (https://ncatlab.org/nlab/), Arxiv (https://arxiv.org/), Encyclopedia of Math (https://www.encyclopediaofmath.org) からのhtmlファイル群を主に収集し、整形とデータベース化をして、検索可能にした。また、数学書籍のpdfファイル群（約10G B）を収集し、証明支援系Coqを用いて形式化された定理群（これは、フランスINRIA研究所を中心とするCoq/SSReflectを用いた、ファイト・トンプソンの定理（奇数位数定理(https://github.com/math-comp/odd-order) の他、主にCoqGym (https://github.com/princeton-vl/CoqGym) で収集された7万余の定理証明を含む）などである。このうち、htmlファイル群については、データベース化し、Webサイト
(http://163.43.192.18:8000/proofs)を構築して定理、証明、データ元の検索・表示ができるようになっている。（著作権等の確認の詰めが未了で、認証をかけてあり、現時点で非公開である）このサイトではサーバーに証明支援系Coq/SSReflectをおき、JSCoq (https://jscoq.github.io/) を配置して、インターラクティブに証明の形式化ができる環境となっている。この環境において、証明の次のステップ（証明支援系ではtactics）を予想する機械学習はまだ実験途上である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
機械学習を用いて証明支援系による定理証明の形式化を行う前提として必要な数学データの収集と整形、検索プログラムの実装については、順調に進んでおり、研究期間内に定理検索と定理証明のWeb sサイト(http://163.43.192.18:8000/proofs)を公開できる可能性が大きい。現在検索対象はProofWiki (https://proofwiki.org/wiki/), nLab (https://ncatlab.org/nlab/), Arxiv (https://arxiv.org/), Encyclopedia of Math (https://www.encyclopediaofmath.org) からのhtmlファイル群であるが、数学書籍等のpdfファイルを解析する研究も行なっている。証明支援系Coqを用いて形式化された定理群を用いた機械学習はCoqGym (https://github.com/princeton-vl/CoqGym) のASTacticをattentionベースにする研究を行なっている。しかし、証明支援系を用いた形式化の機械学習のみでは、大局的方策を学習することが困難であることが徐々に判明してきており、この対策として、自然言語処理として関連する定理をランクづけする研究も開始した。これにより、より人間に近い判断ができることが期待される。
|
| Strategy for Future Research Activity |
引き続き、数学データの収集とデータベース化を進めるとともに、サーバー上の証明支援系Coq/SSReflectを用いて形式化する環境を整えていく。また、ここにトポロジーの定理群の（相対的）形式化ファイルを配置していく方針である。これは、公理系からの完全な形式化には多大な時間と労力がかる一方で、すでに確立した数学定理の証明は正しいと考えられるので、これを一時的に公理と見做し、形式化を加速する目的である。また同時に、機械学習においても、初等的なレベルのTactic予想のみでは実際的でないので、中間的な公理を利用することで、より高レベルの予想を学習することが可能となると考えられる。そこで、証明試験系の形式化に限定されず、自然言語レベルでの学習を行なっていく方針である。技術的には、attentionベースのtransformerを利用することを考えている。このために、汎用的な「定理」のpythonによるクラス設計をしていく。このクラスでは、形式化された場合はCoqスクリプトのデータベースへのキーが入るが、形式化未了の場合でも、確立されている定理の場合は、機械証明の学習対象となる。
|
| Causes of Carryover |
次年度使用額が生じた主な原因は、コロナ感染症拡大のため、出張を控えたため、旅費予定分を使用することができなかったためである。令和3年度においてもコロナ感染症の状況は不明である。その一方で、ウェッブコンテンツの重要性は一層増大している。我々の研究において定理証明と検索サイトを構築することが目標として重みを増してきたと考えている。このために、今回生じた使用額を研究成果を公開するウェッブサイトとサーバープログラム、データベース作成のための人件費・謝金にまわす計画である。
|
| Remarks |
著作権等の確認未了のため認証がかけてあります（現時点で非公開）
|
Research Products
(1 results)
