| 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 |
Kuga Kenichi 千葉大学, 大学院理学研究院, 名誉教授 (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 Final Research Achievements |
We created python programs that execute .v files of proof assistant Coq/SSReflect and produce datasets for machine learning tasks of predicting next proof steps, i.e.,tactics in theorem formalization. We apply these programs on existing .v files and produced couple of datasets of size about 400Mb. We trained deep learning models of transformer types using these datasets. Although we aimed at improving prediction accuracy through the choices of deep learning models and tokenizers and through the choices of hyper parameters, we haven't reached a practical accuracy that make the actual formalization of mathematical theorems from topology e.t.c. proceed, at the time of writing this report.
|
| Academic Significance and Societal Importance of the Research Achievements |
数学の電子化（機械による形式化）やソフトウェアの検証の自動化は科学の基盤を確固とする意味でも、またAI等のソフトウェアの信頼性のある実行のためにも意義がある。このための機械学習は、既存データの絶対数が少なく、またデータセットは証明支援システムと対話的に作成する必要があるので、汎用性が高く、かつ学習が理解しやすいデータセットを作成することが重要である。本研究で得られたデータセットはtopology等の現代数学の分野の定理の形式化に対して実用的な精度の予測の達成には到っていないが、簡明で可読性が高いので、実用的な自動証明・形式化につながる研究である。
|
