| 研究課題/領域番号 |
20K20340
|
|---|
| 補助金の研究課題番号 |
18H05321 (2018-2019)
|
|---|
| 研究種目 |
挑戦的研究(開拓)
|
| 配分区分 | 基金 (2020)
補助金 (2018-2019) |
|---|
| 審査区分 |
中区分11:代数学、幾何学およびその関連分野
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
久我 健一 千葉大学, 大学院理学研究院, 名誉教授 (30186374)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
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千円)
|
|---|
| キーワード | 深層学習 / 証明支援系 / 形式化 / 数学の形式化 / transformers / トポロジー / 機械学習 / 自動証明 / coq / ssreflect / 強化学習 / 証明支援システム / 有限射影平面 / Coq / SSReflect / TensorFlow |
|---|
| 研究開始時の研究の概要 |
数学データをコンピューターが理解できる電子データとするために、数学を「形式化」することが必要になる。現代のコンピューター技術を持っても、これは大変困難な作業である。この研究では、現代数学に広範な基礎を与えるトポロジーの形式化に、機械学習の一分野である深層学習と、強化学習を適用する可能性を探る研究である。
|
| 研究成果の概要 |
証明支援ソフトウェアCoq/SSReflectを用いた証明ファイル(.vファイル）を処理し、証明ステップ(tactic)予想をタスクとする機械学習用のデータファイルを作成するpythonプログラムを作成し、これを用いて既存の.vファイルから400Mb程度の複数のデータセットを作成した。このデータセットを用いてtransformerタイプの深層学習モデルを訓練した。モデルとトークナイザの選択や、ハイパーパラメータの調整等で、予測精度の向上を目指しているが、topology等の数学定理の形式化が進行する精度には現時点ではまだ至っていない。
|
| 研究成果の学術的意義や社会的意義 |
数学の電子化（機械による形式化）やソフトウェアの検証の自動化は科学の基盤を確固とする意味でも、またAI等のソフトウェアの信頼性のある実行のためにも意義がある。このための機械学習は、既存データの絶対数が少なく、またデータセットは証明支援システムと対話的に作成する必要があるので、汎用性が高く、かつ学習が理解しやすいデータセットを作成することが重要である。本研究で得られたデータセットはtopology等の現代数学の分野の定理の形式化に対して実用的な精度の予測の達成には到っていないが、簡明で可読性が高いので、実用的な自動証明・形式化につながる研究である。
|
