Study on Logical Similarity between Theorems

2022 Fiscal Year Final Research Report

• Project/Area Number: 20K19863
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 61030:Intelligent informatics-related
• Research Institution: Yamaguchi University
• Principal Investigator: Nakasho Kazuhisa 山口大学, 大学院創成科学研究科, 准教授 (40780242)
• Project Period (FY): 2020-04-01 – 2023-03-31
• Keywords: 定理証明支援系 / 自動定理証明 / 情報検索 / 数学知識管理

Outline of Final Research Achievements

(1) We proposed a framework for measuring the similarity between theorems. We achieved a Mean Absolute Percentage Error of 0.330 in machine learning experiments using this framework. (2) We improved the theorem search algorithm based on latent semantic indexing to take type information into account, and improved the Mean Average Precision by 53%. (3) We developed an auto completion algorithm for Mizar, an interactive theorem prover, and achieved over 90% accuracy in the proposed 10 candidates. (4) We built a VSCode extension for Mizar and a web application integrating the formalized mathematics library with the aforementioned algorithms, and made it available on the web.

Free Research Field

数学知識管理

Academic Significance and Societal Importance of the Research Achievements

近年，定理証明支援系による形式化数学ライブラリの開発が活発化しており，本研究におけるMizar数学ライブラリのWeb統合アプリの研究開発は，ライブラリ開発の効率化に一石を投じ，他のシステムに対しても同様の環境を構築する強いモチベーションを与えたものと考える．また現在進行形で，大規模言語モデル（LLM）が自動定理証明器に大幅な性能向上をもたらしつつあるが，本研究で提案した定理間の類似度を計測する情報理論的枠組みは，LLMのファインチューニングに対する良質な学習コーパスを人手に依らず生成する能力を有するため，今後，自動定理証明器に革命的な性能向上をもたらす可能性がある．