2021 Fiscal Year Research-status Report
| Project/Area Number |
20K20340
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
久我 健一 千葉大学, 大学院理学研究院, 教授 (30186374)
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Keywords | トポロジー / 数学の形式化 / 証明支援系 / 機械学習 |
|---|
| Outline of Annual Research Achievements |
本研究は証明支援系を用いた数学の形式化に深層学習を適用する可能性を探るものである。深層学習技術は現在著しく発展を遂げている機械学習の分野で、本研究に関連する具体的を挙げると、2020年にOpenAIが発表した言語モデルGTP-3(Generative Pre-trained Transformer-3)は自動翻訳等の分野に飛躍的な発展をもたらした。本研究当初はより伝統的なRNN（LSTM)を用いることを計画していたが、実用的な成果には至らなかった。そこで、GTPのベースであるTransformerを用いたモデルを使用することとした。この方針転換は、これまで証明支援系の出力である証明木構造をいかに深層学習の効率的な入力にするか、という難題を回避したと考えられる。実際Attentionを利用するencoder（例えばBERTがよく知られている）は言語モデルなどのトークン化の詳細に精度が影響されにくことが実験的に知られている。そこで、具体的には証明支援系COQの内部情報の詳細を忘れ、COQで言えばcoqtopの出力をそのままトークン化してBERTに入力しベクトル表現を得るという、すでにルーチンといえる具体的方針をとることが可能となった。この前提となる、COQと言語モデルのプログラム的連携の技術は得ているので、変数等をどう表現するか、などの課題はあるものの、深層学習技術を利用した数学の形式化がより現実味を帯びてきた。実用的成果にはまだ至っていないが、BERTやGTPと同様にいかにして事前学習を行うか、いかにして分野ごとのファインチューニングを行うか、という部分に研究の焦点が絞られてきている。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の難点の一つは、証明木構造のようなデータを、いかに効果的学習が可能なベクトルとして表現するかという点であったが、Attentionを用いたTransformerベースのモデルを採用することによって、この難点を実質的に回避できる可能性が出てきている。また、数学定理の証明は深層学習に必要なビッグデータと呼ばれうるほどのデータ量がないという欠点によって、基本的には強化学習を採用する必要があるが、そのためのCOQと深層学習フレームワーク（具体的にはPyTorch)との連携技術は既に得ているので、学習データの自動生成が可能となっている。自動生成においては、変数名を色々に変えて学習データを増やすことが、変数名の取り扱いの課題に対する一つの処方箋となり得る状況にある。TransformerベースのBERTやGTPと同様のモデルを使用すれば、有効な事前学習の方法として、数学分野として基礎的である（位相空間論など）と同時に、証明支援系による形式化ライプラりとしてもCOQの標準ライブラリを用いることが考えられ、学習データの自動生成と併せて、現実的な方法が視野に入ってきた。
|
| Strategy for Future Research Activity |
Attentionを用いたTransformerベースのエンコーダ・デコーダを用いる。証明支援系Coqからの出力は内部での構造証明木データの詳細に依らず、そのまま（トークン化して）エンコーダ（BERT)に入力する。トークンは予約語の他に変数名があるが、Coqスクリプトのセクション内部でのみ有効な変数名は、いくつかのバリエーションを生成して、学習データを増やすとともに、変数の具体名でなく、変数の役割を機械に学習させる。これらの方針によって、研究の焦点は事前学習とファインチューニングに移る。事前学習については数学的に基礎的、一般的な分野として位相空間論(トポロジー）を選ぶと同時に、具体的な形式化においても基礎的なCoqの標準ライブラリを事前学習に用いる。その際、変数名を色々変える等の方法でデータ数を増やし、学習が進むようにする。SSReflectについては、Coq標準ライプラりとは別に学習させたあと、合併して学習する。ファインチューニングについては、数学の分野だけでなく、より細かく各事項を対象とし、また形式化のライブラリごとにも分けて細かいファインチューニングを行う。事前学習・ファインチューニングの方法について、コンピュータ実験に基づいて、より洗練された方法に改善していく。
|
| Causes of Carryover |
新型コロナウイルス蔓延のため、研究連絡・打ち合わせのための旅費を使用しなかった。
次年度は、コロナウイルス感染状況にもよるが、旅費に限定せず、感染に依存しないウェッブ上での発信の重要性から、証明サイトの構築に重点を置く計画である。このサイト上には数学形式化の深層学習モデルを置くが、このモデルの深層学習には長時間にわたるGPUの使用が必要になるので、すでに使用している計算機に加え、Google Cloud Platform等のクラウドで行う場合の使用料として、３０万円程度を見込んでいる。また、サイトをより充実させるための業務委託等に５０万円程度の使用を見込んでいる。その他、関連する数学専門書籍と関連技術書の購入費や形式化データ作成・入力のための人件費・謝金を状況に応じて使用する計画である。
|
| Remarks |
数学定理形式化サーバ構築中。証明検索データの著作権等未確認等の理由で現在非公開
|
Research Products
(1 results)
