| 研究課題/領域番号 |
20K19863
|
|---|
| 研究機関 | 山口大学 |
|---|
研究代表者 |
中正 和久 山口大学, 大学院創成科学研究科, 准教授 (40780242)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2023-03-31
|
| キーワード | 定理検索 / 定理証明支援系 / 形式化数学 / 論理的類似度 / 情報源モデル / Mizarシステム |
|---|
| 研究実績の概要 |
本研究では，定理間の類似度を情報理論的に定式化して新たな定理検索アルゴリズムを提案すること，さらにそのアルゴリズムを援用することにより定理証明支援系とその周辺ツールの利便性を向上させることを目的としている．研究初年度となる令和2年度は，定理間の類似度を計測するアイデアを提案するとともに，定理検索データを収集するためのシステムの構築，論理的類似度を利用するアプリケーションの構築を行った．主な実績を以下に列挙する．
1. 定理間の類似度を計測する情報理論的な枠組みを提案した．特に，この枠組みが準距離公理を満たすための条件ならびに，この枠組みの定理検索以外への応用について検討し，議論を深めた．
2. Latent Semantic Indexingに基づいた定理検索システムを構築してWeb上に一般公開した．本システムを通じて利用者が定理を検索した結果はデータベースに集積され，今後定理検索アルゴリズムの機械学習および性能評価に利用される．
3. 定理証明支援系MizarのVisual Studio Code（以下VSCode）上で動作する拡張機能を開発してVSCode Market Placeに一般公開した．今後，定理検索アルゴリズムを援用して，証明中で引用するべき定理の候補を提案する機能を組み込む計画である．
4. 形式化数学ライブラリの依存関係を可視化するツールを構築してWeb上に一般公開した．今後，定理間の類似度計算アルゴリズムを援用してアーティクル同士の類似度を算出し，類似度が近いアーティクル同士がより近い位置に配置されるような自動レイアウト機能を組み込む計画である．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
定理間の類似度を計測する枠組みについては，証明中のバイアスに関する理論面での検討が不十分であり，さらに議論を深める必要がある．その反面，各種アプリケーションの実装については当初予定よりも早く進行しており，全体としては概ね順調に進展しているものと判断した．
|
| 今後の研究の推進方策 |
2年目となる令和3年度は，まず定理間の類似度を計測する理論的な枠組みについて，証明中のユニフィケーションでのバイアスの取り方の議論を深めることを優先し，当初からの遅れを挽回する計画である．その他は申請書記載の研究計画に沿って研究を進める．現時点では，研究を遂行する上での課題は発生していないが，必要が生じた際には，応募時の申請書に記載している「研究が当初計画通りに進まない時に対応策」に沿って対応する．
|
| 次年度使用額が生じた理由 |
初年度の令和2年度に計画していた，定理間の類似度を計測する枠組みについての理論面での検討が不十分であるため，当初予定していた国際学会参加などのスケジュールに遅れが生じた．
2年目となる令和3年度以降に当理論を練り直し，国際学会ならびに論文誌への投稿を進める．
|
