2022 Fiscal Year Research-status Report
| Project/Area Number |
20K20340
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
久我 健一 千葉大学, 大学院理学研究院, 名誉教授 (30186374)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Keywords | トポロジー / 数学の形式化 / 証明支援系 / 機械学習 |
|---|
| Outline of Annual Research Achievements |
証明支援系を用いた数学の形式化は一般に非常に困難であるので、この研究では位相幾何学を起点とする数学の形式化において、深層学習を適用することを目標においている。
そのために、自然言語処理の深層学習アーキテクチャーである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学習データを作成することができた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
数学的に実用的な位相幾何学の形式化は当初予期していたよりも困難であった。世界的にみても、現状では、カテゴリカル（ホモトピカル）な数学の基礎づけや離散数学、組み合わせ論等から様々な形式化が行われているが、未だ基礎的な数学の形式化に留まり、実用的な数学を全般的に形式化する見通しが立つ状況にない。そこで当研究の力点はいっそう深層学習の積極的な利用に向けて、証明支援系Coqと深層学習モデルとの連携に置くこととなった。
具体的には証明支援系システムCoqとTransformerベースの自然言語処理モデルの一つであるT5(Text To Text Trensfer Transformer)を連携させ、数学証明のコンテクストから次のアクションとしてのTacticsを予測するタスクを学習させるプログラム群を作成した。
ここでの問題はどのような学習データを抽出するかという点であり、学習データはインターラクティブなcoqからの応答から作成されるもので、例えばGPT(Generative Pre-trained Transformer)がインターネット上のビッグデータをそのまま学習データに使用するようには進まない。そこで我々はCogが応答して返す証明図とともに、そこに出現する項の型情報も付与した入力からTacticとその引数を予想する学習データを作成することとした。インターネット上に公開されているCoq/SSReflectによる数学定理証明の（プログラムextraction型でない）形式化ライブラリー群では、ほぼ学習データが抽出できることを確かめた。
上述の通り、世界的に見ても実用的な数学を全般的に形式化する見通しが立たない状況の中で、実用的数学定理形式化への深層学習の利用に向けた重要な一歩であると考えている。
|
| Strategy for Future Research Activity |
これまでの研究から、証明支援系Coqとインターラクティブに連携して応答から学習データを作ることができるようになってきているが、数学の形式化のデータは、インターネット上で集めてもビッグデータと呼べるものにはならず、そのままT5のようなTransformerを訓練して成果をあげることは期待できない。したがって、強化学習の研究に進むことが不可避である。この強化学習におけるaction空間はタクティックの引数として得られた定理に加え、直前に得られた定理も含まれることを考えると、膨大かつ動的であり、深層Q学習のようなバリューベースの強化学習のみでは対応できない。そこで、ポリシーベースの強化学習をどのように併用していくかを研究する必要がある。このような強化学習として、たとえばActor-Criticの手法があるが、我々の状況では証明中も使用可能な定理が動的に増えていくことに対応する必要がある。また、Coq の応答は非常に遅いので、Coq とTransformer (T5)とのインターラクションをできるだけ抑え、Coq のみでランダムに試行して結果を記録していくといった工夫が必要になってくると考えている。
|
| Causes of Carryover |
申請者は令和4年8月にHawaiiで開催された国際研究集会RE:BITにおいて深層学習モデルであるTransformerを用いた証明支援システムの使用についての講演を行なったが, コロナ感染症の拡大で極力短期の出張としたため、証明支援システムLeanに詳しい現地の研究者との共同研究に十分な時間が持てなかった。また同年10月に国内講演を行なったが、Zoomを用いたハイブリッド配信となり、十分な反応を得ることが難しかった。このような状況で研究費使用額が少なくなった。
現時点で最新の深層学習モデルTransformer(T5)を用いた証明支援システム(Coq)の使用は可能となっているため、より高い性能をあげ、目標とする数学証明の形式化を自動化するためにハードウェアの調整、Transformer のトレーニングに使用することを計画している。
|
Research Products
(2 results)
