| 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
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2022: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2021: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2020: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 定理証明支援系 / 自動定理証明 / 情報検索 / 数学知識管理 / 定理検索 / 形式化数学 / 論理的類似度 / 情報源モデル / Mizarシステム / 類似度 / 情報量 |
|---|
| Outline of Research at the Start |
本研究は定理証明支援系によって構築された大規模ライブラリにおける情報抽出技術の確立を目指し，論理的な意味に根ざした定理の類似度推定アルゴリズムを構築するものである．そのため，本研究では，（1）最短証明情報量を用いた定理同士の論理的な類似度の定式化，（2）最短証明情報量を高速・高精度に推定するアルゴリズムの構築，（3）大規模定理ライブラリの検索・分類・クラスタリングにおける類似度推定アルゴリズムの適用と有用性の実証，に関する研究を実施する．
|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
近年，定理証明支援系による形式化数学ライブラリの開発が活発化しており，本研究におけるMizar数学ライブラリのWeb統合アプリの研究開発は，ライブラリ開発の効率化に一石を投じ，他のシステムに対しても同様の環境を構築する強いモチベーションを与えたものと考える．また現在進行形で，大規模言語モデル（LLM）が自動定理証明器に大幅な性能向上をもたらしつつあるが，本研究で提案した定理間の類似度を計測する情報理論的枠組みは，LLMのファインチューニングに対する良質な学習コーパスを人手に依らず生成する能力を有するため，今後，自動定理証明器に革命的な性能向上をもたらす可能性がある．
|
