| Project/Area Number |
20K20340
|
|---|
| Project/Area Number (Other) |
18H05321 (2018-2019)
|
|---|
| Research Category |
Grant-in-Aid for Challenging Research (Pioneering)
|
| Allocation Type | Multi-year Fund (2020)
Single-year Grants (2018-2019) |
|---|
| Review Section |
Medium-sized Section 11:Algebra, geometry, and related fields
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
久我 健一 千葉大学, 大学院理学研究院, 名誉教授 (30186374)
|
|---|
| Project Period (FY) |
2020-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥20,800,000 (Direct Cost: ¥16,000,000、Indirect Cost: ¥4,800,000)
Fiscal Year 2021: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2020: ¥7,800,000 (Direct Cost: ¥6,000,000、Indirect Cost: ¥1,800,000)
Fiscal Year 2019: ¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2018: ¥6,500,000 (Direct Cost: ¥5,000,000、Indirect Cost: ¥1,500,000)
|
|---|
| Keywords | トポロジー / 数学の形式化 / 証明支援系 / 機械学習 / 形式化 / 自動証明 / 深層学習 / coq / ssreflect / 強化学習 / 証明支援システム / 有限射影平面 / Coq / SSReflect / TensorFlow |
|---|
| Outline of Research at the Start |
数学データをコンピューターが理解できる電子データとするために、数学を「形式化」することが必要になる。現代のコンピューター技術を持っても、これは大変困難な作業である。この研究では、現代数学に広範な基礎を与えるトポロジーの形式化に、機械学習の一分野である深層学習と、強化学習を適用する可能性を探る研究である。
|
| 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 のみでランダムに試行して結果を記録していくといった工夫が必要になってくると考えている。
|
Report
(5 results)
Research Products
(7 results)
