2021 Fiscal Year Research-status Report
Study on Logical Similarity between Theorems
| Project/Area Number |
20K19863
|
|---|
| Research Institution | Yamaguchi University |
|---|
Principal Investigator |
中正 和久 山口大学, 大学院創成科学研究科, 准教授 (40780242)
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Keywords | 定理検索 / 定理証明支援系 / 形式化数学 / 論理的類似度 / 情報源モデル / Mizarシステム |
|---|
| Outline of Annual Research Achievements |
本研究では，定理間の類似度を情報理論的に定式化して，新たな定理検索アルゴリズムを提案することを目的としている．2年目となる令和3年度は，定理間の類似度を計測する実験環境の構築，定理検索データを収集するためのシステムのアップデート，論理的類似度を利用するアプリケーションの開発を行った．主な実績を以下に列挙する．
・定理間の類似度を計測するための実験環境を構築中である．本環境では自動定理証明器に命題（TPTP言語）を入力し，出力された証明（TSTP言語）を解析することにより，定理が有する情報量を計測する．現在，TPTP/TPSP言語の構文解析器の開発，命題と証明のグラフ化，自動定理証明器Vampireとの結合を実装したが，命題グラフの簡略化が課題として残っている．
・Web公開中の定理検索システムを，幾つかのライブラリ閲覧アプリケーションと統合し，システム利用者の利便性を向上させた．これらには，形式化数学ライブラリの依存関係を可視化するツール，ライブラリ内のシンボルおよびアーティクルをインクリメンタル検索するツールなどが含まれる．
・定理証明支援系Mizarの入力補完アルゴリズムを開発した．本アルゴリズムはn-gramを精緻化したもので，学習データが小規模な場合でも比較的高い精度を実現できる点が特徴的である．実験では80MB程度のテキストデータを学習したときに，提案10候補において90%以上の精度での入力補完を実現した．
・数学ライブラリを分野毎に分類して複合グラフとして表現する研究に着手している．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
今年度に完成予定であった定理間の類似度を計測するための実験環境の構築が遅れているが，その他は順調に推移しているため，「やや遅れている」と判断した．
|
| Strategy for Future Research Activity |
3年目となる令和4年度は，まずは実験環境の構築を最優先し，その後，定理間の類似度に関して理論と実験の摺り合わせを行う．その他は当初の計画通りに進める予定である．現時点では，研究を遂行する上での課題は発生していないが，必要が生じた際には，応募時の申請書に記載している「研究が当初の計画通りに進まない時の対応策」に沿って対応する．
|
| Causes of Carryover |
一部の研究遅れに伴い，国際会議での発表を次年度へスライドした．
|
Research Products
(8 results)
