ニューラル定理証明のためのHyperTree Proof Search

我々は、Transformerベースの自動定理証明器向けのオンライン学習プロシージャを提案する。本手法は、AlphaZeroの最近の成功に着想を得た新たな探索アルゴリズム、HyperTree Proof Search（HTPS）を活用している。モデルはオンライン学習を通じて過去の証明探索から学習し、訓練分布から大きく離れたドメインに対しても一般化できる。本研究では、複雑度が増す三つの環境において、パイプラインの主要構成要素の詳細なアブレーションを実施し、性能を評価した。特に、HTPSを用いることで、注釈付き証明データ上で訓練されたモデルが、保留されたメタマス（Metamath）定理の65.4％を証明することに成功した。これは、GPT-fによる従来の最良手法（56.5％）を著しく上回るものである。これらの未証明定理に対するオンライン学習を実施することで、正確性はさらに82.6％まで向上した。同程度の計算リソースを用いた場合、LeanベースのminiF2Fカリキュラムデータセットにおいて、定理証明精度は従来の31％から42％へと向上し、新たな最良性能を達成した。