要約
大規模言語モデル（LLMs）は、形式的定理証明の分野において有望な研究テーマとして注目されている。しかし、特に証明例のフォーマットや構成に関するモデルの完全な活用は、まだ十分に検討されていない領域である。本研究では、LLMの効果を向上させるために、サブゴールに基づく証明例学習フレームワークを提案する。このフレームワークは、以下の2つの主要な要素から構成される。第一に、強化学習およびロボティクス分野におけるサブゴール学習の知見を活用し、各証明例に対して明確なサブゴールを構築し、サブゴール学習に関する適切な理論に基づいてこれらのサブゴールを精緻化する手法を提案する。第二に、最近の拡散モデル（diffusion models）の進展を応用し、証明例の最適な構成を予測する。これにより、証明構成に関する従来の困難な課題である「部分集合の選択」と「順序の決定」の両方を同時に解決する。サブゴールベースの学習手法を統合した結果、miniF2Fベンチマークにおいて、従来の証明精度38.9％を44.3％まで向上させることができた。さらに、証明例の構成に拡散モデルを導入することで、精度はさらに45.5％まで向上し、従来の最先端手法と比較してサンプリング効率が約5倍改善された。本研究のコードは、\url{https://github.com/HKUNLP/subgoal-theorem-prover} にて公開されている。