| 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 |
Completed (Fiscal Year 2023)
|
| 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 | 数学の形式化 / 証明支援系 / transformers / トポロジー / 機械学習 / 形式化 / 自動証明 / 深層学習 / coq / ssreflect / 強化学習 / 証明支援システム / 有限射影平面 / Coq / SSReflect / TensorFlow |
|---|
| Outline of Research at the Start |
数学データをコンピューターが理解できる電子データとするために、数学を「形式化」することが必要になる。現代のコンピューター技術を持っても、これは大変困難な作業である。この研究では、現代数学に広範な基礎を与えるトポロジーの形式化に、機械学習の一分野である深層学習と、強化学習を適用する可能性を探る研究である。
|
| Outline of Annual Research Achievements |
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は下記）
|
Report
(6 results)
Research Products
(9 results)
