|
近年，定理証明支援系による形式化数学ライブラリの開発が活発化しており，本研究におけるMizar数学ライブラリのWeb統合アプリの研究開発は，ライブラリ開発の効率化に一石を投じ，他のシステムに対しても同様の環境を構築する強いモチベーションを与えたものと考える．また現在進行形で，大規模言語モデル（LLM）が自動定理証明器に大幅な性能向上をもたらしつつあるが，本研究で提案した定理間の類似度を計測する情報理論的枠組みは，LLMのファインチューニングに対する良質な学習コーパスを人手に依らず生成する能力を有するため，今後，自動定理証明器に革命的な性能向上をもたらす可能性がある．
|
