Applying deep learning to formalization of Topology

2023 Fiscal Year Final Research Report

• 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
• Keywords: 深層学習 / 証明支援系 / 形式化

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.

Free Research Field

topology

Academic Significance and Societal Importance of the Research Achievements

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