| 研究課題/領域番号 |
20K20340
|
|---|
| 補助金の研究課題番号 |
18H05321 (2018-2019)
|
|---|
| 研究種目 |
挑戦的研究(開拓)
|
| 配分区分 | 基金 (2020)
補助金 (2018-2019) |
|---|
| 審査区分 |
中区分11:代数学、幾何学およびその関連分野
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
久我 健一 千葉大学, 大学院理学研究院, 名誉教授 (30186374)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
20,800千円 (直接経費: 16,000千円、間接経費: 4,800千円)
2021年度: 3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
2020年度: 7,800千円 (直接経費: 6,000千円、間接経費: 1,800千円)
2019年度: 3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
2018年度: 6,500千円 (直接経費: 5,000千円、間接経費: 1,500千円)
|
|---|
| キーワード | トポロジー / 数学の形式化 / 証明支援系 / 機械学習 / 形式化 / 自動証明 / 深層学習 / coq / ssreflect / 強化学習 / 証明支援システム / 有限射影平面 / Coq / SSReflect / TensorFlow |
|---|
| 研究開始時の研究の概要 |
数学データをコンピューターが理解できる電子データとするために、数学を「形式化」することが必要になる。現代のコンピューター技術を持っても、これは大変困難な作業である。この研究では、現代数学に広範な基礎を与えるトポロジーの形式化に、機械学習の一分野である深層学習と、強化学習を適用する可能性を探る研究である。
|
| 研究実績の概要 |
証明支援系を用いた数学の形式化は一般に非常に困難であるので、この研究では位相幾何学を起点とする数学の形式化において、深層学習を適用することを目標においている。
そのために、自然言語処理の深層学習アーキテクチャーである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学習データを作成することができた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
数学的に実用的な位相幾何学の形式化は当初予期していたよりも困難であった。世界的にみても、現状では、カテゴリカル（ホモトピカル）な数学の基礎づけや離散数学、組み合わせ論等から様々な形式化が行われているが、未だ基礎的な数学の形式化に留まり、実用的な数学を全般的に形式化する見通しが立つ状況にない。そこで当研究の力点はいっそう深層学習の積極的な利用に向けて、証明支援系Coqと深層学習モデルとの連携に置くこととなった。
具体的には証明支援系システムCoqとTransformerベースの自然言語処理モデルの一つであるT5(Text To Text Trensfer Transformer)を連携させ、数学証明のコンテクストから次のアクションとしてのTacticsを予測するタスクを学習させるプログラム群を作成した。
ここでの問題はどのような学習データを抽出するかという点であり、学習データはインターラクティブなcoqからの応答から作成されるもので、例えばGPT(Generative Pre-trained Transformer)がインターネット上のビッグデータをそのまま学習データに使用するようには進まない。そこで我々はCogが応答して返す証明図とともに、そこに出現する項の型情報も付与した入力からTacticとその引数を予想する学習データを作成することとした。インターネット上に公開されているCoq/SSReflectによる数学定理証明の（プログラムextraction型でない）形式化ライブラリー群では、ほぼ学習データが抽出できることを確かめた。
上述の通り、世界的に見ても実用的な数学を全般的に形式化する見通しが立たない状況の中で、実用的数学定理形式化への深層学習の利用に向けた重要な一歩であると考えている。
|
| 今後の研究の推進方策 |
これまでの研究から、証明支援系Coqとインターラクティブに連携して応答から学習データを作ることができるようになってきているが、数学の形式化のデータは、インターネット上で集めてもビッグデータと呼べるものにはならず、そのままT5のようなTransformerを訓練して成果をあげることは期待できない。したがって、強化学習の研究に進むことが不可避である。この強化学習におけるaction空間はタクティックの引数として得られた定理に加え、直前に得られた定理も含まれることを考えると、膨大かつ動的であり、深層Q学習のようなバリューベースの強化学習のみでは対応できない。そこで、ポリシーベースの強化学習をどのように併用していくかを研究する必要がある。このような強化学習として、たとえばActor-Criticの手法があるが、我々の状況では証明中も使用可能な定理が動的に増えていくことに対応する必要がある。また、Coq の応答は非常に遅いので、Coq とTransformer (T5)とのインターラクションをできるだけ抑え、Coq のみでランダムに試行して結果を記録していくといった工夫が必要になってくると考えている。
|
