トポロジーの形式化における深層学習の適用の研究

点击翻译按钮获取中文摘要

証明支援系を用いた数学の形式化は一般に非常に困難であるので、この研究では位相幾何学を起点とする数学の形式化において、深層学習を適用することを目標においている。そのために、自然言語処理の深層学習アーキテクチャーであるtransformerを利用するための研究を行なった。研究開始当初は当時主流であったRNN特にLSTMの利用を計画していたが、2018年以降、BERTやGPT等のtransformerベースの学習が自然言語処理において高い性能をあげることが報告されたので、この研究ではtransformerベースの汎用モデルとも考えられるT5(Text To Text Transfer Transformer)を用いて証明支援系Coqによる定理証明の形式化を効率化・自動化することを目指した。まず技術的な課題として、CoqがOCamlで記述されており、他方でC++等で作成されPython等で使用されることが想定されているPyTorch、TensorFlow等の深層学習フレームワークとの連携が直接的には取れない点がある。これについては、当研究で開発したpicoqをHuggingFace社のTransformersと連携が取れるように調整した。これによって、既存の数学形式化coqライブラリについてはほぼ完全に学習データが作成できる状態になった。また学習データ作成における課題として、通常の自然言語学習のGPT等のようにビッグデータを収集するのみでは、数学的及び論理的に複雑な内容を学習できないと考えられる点、および、数学の形式化データ自身が少なく、受動的な学習では効果がないと考えられる点でがあげられる。そこで我々はcoqからのインターラクティブなレスポンスから学習データを作成するプログラムを作成した。これによって様々な数学形式化coqライブラリからT5学習データを作成することができた。