2022 Fiscal Year Annual Research 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 |
本研究では，定理間の類似度を情報理論的に定式化して，新たな定理検索アルゴリズムを提案することを目的としている．最終年度となる令和4年度の主な実績を以下に2点列挙する．①定理間の類似度を計測するための実験環境を構築してデータベース化した．今年度は機械学習モデルの入力向けに論理式のベクトル化（トークン分割，term walk，グラフ表現）し，TPTPライブラリに収録されている定理から証明をグラフ化して抽出するプログラムを実装した．また，証明難易度を予測する機械学習モデルを複数提案し，それらの性能を比較した．機械学習モデルには，3層NN，CNN，RNN，LSTM，GCNを用いた．実験の結果，ベクトル化にはTerm Walkを，機械学習モデルにLSTMを用いたときに，最も高い予測精度が得られ，平均絶対誤差率0.330を達成した．②前年度に開発した定理検索システムで用いられている検索アルゴリズムを，型情報を考慮するように改良した．その結果，型情報を考慮しない従来のアルゴリズムと比較して，Mean Average Precisionが53%向上した．特に，検索対象の定理の対偶のような本質的に意味が同値なクエリに対しては，Mean Average Precisionが1523%向上し，提案アルゴリズムの頑強性が明らかとなった．
研究期間を通じて実施した主な研究成果を以下に4点列挙する．
③Mizar数学ライブラリの統合Webプラットフォームを構築した．本サイトは定理検索モジュールの他にも，ライブラリの依存関係を可視化するツール，ライブラリ内のシンボルおよびアーティクルをインクリメンタル検索するツール等を提供する．④定理間の類似度を計測するフレームワークを定義し，その有用性を②で実証した．⑤MizarのVSCode拡張機能を開発した．⑥論文7本分のMizar数学ライブラリの拡充を行った．
|
