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

• 研究課題/領域番号: 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

研究開始時の研究の概要

数学データをコンピューターが理解できる電子データとするために、数学を「形式化」することが必要になる。現代のコンピューター技術を持っても、これは大変困難な作業である。この研究では、現代数学に広範な基礎を与えるトポロジーの形式化に、機械学習の一分野である深層学習と、強化学習を適用する可能性を探る研究である。

研究実績の概要

2023年度は生成AIや大規模言語モデル(LLM)の開発と利用が世界的に急速に進展した。昨年度我々が利用対象としたT5もその一つであるが、GPT4やLLama3等、次々に規模と性能を拡大、向上させている現状と、このようなLLMの構築と事前学習は当該研究の規模では不可能であることとから、さまざまなモデルでの転移学習（あるいはファインチューニング）を見据えて、特定のモデルや特殊なプロトコルによらない数学証明の動的なデータセットの作成手法と作成が現時点で最も重要であると考えるに至った。通常のプログラミング汎用言語の学習データと異なり、Coqのような証明支援系の言語では、作成の難しさから、ファイル自体の量が少ないことに加え、プログラミング段階で、証明状態を対話的に使用する必要がある。そのような観点から作成したCoqデータセットと、これを作成するプログラム等を　GitHub上で公開した。
https://github.com/kenkuga/picoq
ここに公開したデータの一つは441Mbのcsvファイルで、各行は２項目からなり、第１項目はCoqをemacs上で利用するときに対話的に返される情報であり、第２項目はそれに対するTacticとそれに与えられるパラメータである。また第１項目には、現れる各項のタイプ情報も付与されているが、これはShow Allで得られる情報であり、特殊なプロトコルを用いないため、利用が容易である。
LLM等を用いた数学定理の形式化の実用化のためには、通常の数学証明を直ちに形式化できるわけではないため、まず証明を数学言語で細かいステップに分解する段階が必要である。その観点からの利用を想定して、ウェブ上のProofwikiやn Lab等の証明データベースを作成した。
http://163.43.192.18:8000/proofs/index3（PWは下記）

研究成果

• [学会発表] Let Transformers speak Coq (2022)
  • 著者名/発表者名: Kenichi Kuga
  • 学会等名: RE:BIT
  • 国際学会 / 招待講演
• [学会発表] Training Transformers to formalize Topology in Coq (2022)
  • 著者名/発表者名: 久我健一
  • 学会等名: トポロジーとコンピュータ２０２２
• [学会発表] 有限幾何の形式化と深層学習 (2019)
  • 著者名/発表者名: 久我健一、井上健太
  • 学会等名: 第３回情報理論および符号理論とその応用ワークショップ(ICA2019)
• [学会発表] Some experiments of formalizing finite/projective geometry using Monte Carlo tree search (2019)
  • 著者名/発表者名: Ken'ichi Kuga
  • 学会等名: American Mathematical Society, Central and Western Joint Sectional Meeting
  • 国際学会
• [備考] picoq
  • URL: https://github.com/kenkuga/picoq
• [備考] 数学証明検索データベース
  • URL: http://163.43.192.18:8000/proofs/index3
• [備考] 定理証明検索サイト（仮題）
  • URL: http://163.43.192.18:8000/proofs
• [備考] 仮称：定理検索データベース
  • URL: http://163.43.192.18:8000/coqapp/index
• [備考] 仮称：定理形式化サイト
  • URL: https://163.43.192.18:8000/static/jscoq_test/index2.html