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

2023 年度 研究成果報告書

• 研究課題/領域番号: 20K20340
• 補助金の研究課題番号: 18H05321 (2018-2019)
• 研究種目: 挑戦的研究(開拓)
• 配分区分: 基金 (2020); 補助金 (2018-2019)
• 審査区分: 中区分11:代数学、幾何学およびその関連分野
• 研究機関: 千葉大学
• 研究代表者: 久我 健一 千葉大学, 大学院理学研究院, 名誉教授 (30186374)
• 研究期間 (年度): 2020-04-01 – 2024-03-31
• キーワード: 深層学習 / 証明支援系 / 形式化

研究成果の概要

証明支援ソフトウェアCoq/SSReflectを用いた証明ファイル(.vファイル）を処理し、証明ステップ(tactic)予想をタスクとする機械学習用のデータファイルを作成するpythonプログラムを作成し、これを用いて既存の.vファイルから400Mb程度の複数のデータセットを作成した。このデータセットを用いてtransformerタイプの深層学習モデルを訓練した。モデルとトークナイザの選択や、ハイパーパラメータの調整等で、予測精度の向上を目指しているが、topology等の数学定理の形式化が進行する精度には現時点ではまだ至っていない。

自由記述の分野

topology

研究成果の学術的意義や社会的意義

数学の電子化（機械による形式化）やソフトウェアの検証の自動化は科学の基盤を確固とする意味でも、またAI等のソフトウェアの信頼性のある実行のためにも意義がある。このための機械学習は、既存データの絶対数が少なく、またデータセットは証明支援システムと対話的に作成する必要があるので、汎用性が高く、かつ学習が理解しやすいデータセットを作成することが重要である。本研究で得られたデータセットはtopology等の現代数学の分野の定理の形式化に対して実用的な精度の予測の達成には到っていないが、簡明で可読性が高いので、実用的な自動証明・形式化につながる研究である。