講演情報
[2Yin-B-51]大規模言語モデルの純粋な証明生成能力の評価命題論理のヒルベルトシステムに基づくベンチマーク
〇安東 里沙子1、山田 鈴太2、山﨑 紗紀子1、秋吉 亮太2、峯島 宏次1 (1. 慶應義塾大学、2. 電気通信大学)
キーワード：
論理的推論、定理証明、大規模言語モデル
本研究では、大規模言語モデル（LLM）に命題論理の証明生成を行わせることにより、LLMが有する「純粋な」証明能力を体系的に評価するための新たなベンチマークを提案する。近年、LLMは外部の自動証明ツールや数学ライブラリと組み合わせることで高い性能を示しているが、それらの補助なしにどの程度、形式的体系に基づく証明構成を行えるのかは十分に明らかではない。そこで本研究では、自動定理証明が一般に困難とされる課題設定として命題論理のヒルベルトシステムに着目し、形式的証明を生成する課題を設定する。提案ベンチマークを用いて、現状の推論特化型LLMを評価し、どの程度複雑な証明が生成できるかを検証する。生成された証明の正しさは証明支援系Leanにより検証する。さらに、人間にとっては容易な証明構築方針をLLMに試行させ、証明生成に与える影響を比較・分析する。その結果、LLMの証明生成能力の特徴を明らかにするとともに、正確で信頼できる論理推論能力の実現に向けた課題を示す。