| 研究課題/領域番号 |
20K19863
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分61030:知能情報学関連
|
|---|
| 研究機関 | 山口大学 |
|---|
研究代表者 |
中正 和久 山口大学, 大学院創成科学研究科, 准教授 (40780242)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2022年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2021年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2020年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
|---|
| キーワード | 定理証明支援系 / 自動定理証明 / 情報検索 / 数学知識管理 / 定理検索 / 形式化数学 / 論理的類似度 / 情報源モデル / Mizarシステム / 類似度 / 情報量 |
|---|
| 研究開始時の研究の概要 |
本研究は定理証明支援系によって構築された大規模ライブラリにおける情報抽出技術の確立を目指し，論理的な意味に根ざした定理の類似度推定アルゴリズムを構築するものである．そのため，本研究では，（1）最短証明情報量を用いた定理同士の論理的な類似度の定式化，（2）最短証明情報量を高速・高精度に推定するアルゴリズムの構築，（3）大規模定理ライブラリの検索・分類・クラスタリングにおける類似度推定アルゴリズムの適用と有用性の実証，に関する研究を実施する．
|
| 研究成果の概要 |
(1)定理間の類似度を計測する枠組みを提案した．この枠組みでの機械学習実験で平均絶対誤差率0.330を達成した．(2)潜在意味解析に基づいた定理検索アルゴリズムを，型情報を考慮するように改良し，Mean Average Precisionを53%向上させた．(3)定理証明支援系Mizarの入力補完アルゴリズムを開発し，提案10候補において90%以上の精度での入力補完を実現した．(4)前述のアルゴリズム群を搭載したVSCode拡張機能と形式化数学ライブラリ統合Webアプリケーションを構築し，Web上で一般公開した．
|
| 研究成果の学術的意義や社会的意義 |
近年，定理証明支援系による形式化数学ライブラリの開発が活発化しており，本研究におけるMizar数学ライブラリのWeb統合アプリの研究開発は，ライブラリ開発の効率化に一石を投じ，他のシステムに対しても同様の環境を構築する強いモチベーションを与えたものと考える．また現在進行形で，大規模言語モデル（LLM）が自動定理証明器に大幅な性能向上をもたらしつつあるが，本研究で提案した定理間の類似度を計測する情報理論的枠組みは，LLMのファインチューニングに対する良質な学習コーパスを人手に依らず生成する能力を有するため，今後，自動定理証明器に革命的な性能向上をもたらす可能性がある．
|
