LEGO-Prover：拡張可能なライブラリを備えたニューラル定理証明

大規模言語モデル（LLM）の成功にもかかわらず、定理証明というタスクは依然として最も困難な推論課題の一つであり、完全に解決されたとは言えない状況にある。従来の言語モデルを用いたアプローチは有望な結果を示しているものの、中学校レベルの定理でさえ証明に苦労しているのが現状である。これらの手法に共通する限界の一つは、定理証明プロセス全体を通じて固定された定理ライブラリを前提としている点である。しかし、誰もが知るように、新たな有用な定理、あるいは新しい理論の構築は、数学の進展を促進し、より難しく深い結果を証明するために、単なる補助にとどまらず、極めて重要かつ不可欠である。本研究では、検証済みの補題（lemmas）を「スキル」として含む拡張可能なスキルライブラリを活用し、定理証明に用いるLLMの能力を拡張する「LEGO-Prover」を提案する。LEGO-Proverは、証明をモジュール化して構築することで、LLMがライブラリから既存のスキルを取得し、証明過程中に新たなスキルを生成することができる。これらのスキルは、さらにLLMを用いたプロンプトによって進化させられ、ライブラリの質と量の両面で拡充される。モジュール化され再利用可能なスキルが継続的にライブラリに追加されることで、次第に複雑化する数学的問題に対処可能となる。さらに、学習されたスキルライブラリは、人間による証明と形式的証明の間のギャップを埋める役割も果たす。特に、証明途中で欠落しているステップを補完しやすくなる。LEGO-Proverは、miniF2F-validのパッセート率を48.0%から57.0%へ、miniF2F-testでは45.5%から47.1%へと向上させ、現状の最先端性能を大きく更新した。証明プロセス中には、2万件を超えるスキル（定理・補題）が生成され、成長するライブラリに追加された。アブレーションスタディの結果、新たに追加されたスキルが定理証明に実際の貢献を果たしており、成功確率が47.1%から50.4%まで向上したことが明らかになった。本研究では、コードおよび生成されたすべてのスキルを公開する。