SubgoalXL: 定理証明のためのサブゴールドベースの専門家学習

数学とコンピュータサイエンスの交差点にある形式的定理証明の分野は、大規模言語モデル（LLMs）の進歩により再び注目を集めています。本論文では、Isabelle環境における形式的定理証明を強化するため、部分目標ベースの証明と専門家学習をシナジーさせる新しい手法であるSubgoalXLを紹介します。SubgoalXLは、専門的な数学や定理証明データの不足と、LLMsの多段階推論能力向上の必要性という2つの重要な課題に取り組んでいます。データ効率を最適化し、部分目標レベルでの監督を用いることで、限られた人間生成の証明からより豊富な情報を抽出します。このフレームワークは、部分目標指向の証明戦略と専門家学習システムを統合し、形式的ステートメント、証明、および部分目標ジェネレーターを反復的に洗練していきます。Isabelle環境が部分目標ベースの証明において持つ利点を利用することで、SubgoalXLは標準的なminiF2Fデータセットで56.1%という新たな最先端性能を達成しました。これは絶対的な4.9%の改善を示しています。特に、SubgoalXLはminiF2Fから41問のAMC12問題、9問のAIME問題、3問のIMO問題を成功裏に解くことができました。これらの結果は、限られたデータの利用価値最大化と複雑な推論に対するターゲット指導が形式的定理証明において有効であることを示しており、AIの推論能力向上への継続的な貢献となっています。実装は \url{https://github.com/zhaoxlpku/SubgoalXL} で公開されています。