Thor：言語モデルと自動定理証明器を統合するためのハンマーの使用

定理証明において、与えられた予想の証明を可能にするために、大規模な命題ライブラリから有用な前提を選択する作業は極めて重要である。この課題は、特に言語モデルに基づく定理証明器にとって大きな難題であり、テキスト形式で提示された膨大な量の前提に対して十分な推論が困難なためである。本論文では、言語モデルと自動定理証明器を統合する枠組み「Thor」を提案する。Thorでは、自動定理証明器の強力な能力を活用する「ハムマー（hammers）」と呼ばれる一連の手法を用いて前提選択を行う一方、その他のすべてのタスクは言語モデルに割り当てる。Thorにより、PISAデータセットにおける言語モデルの成功確率は39%から57%に向上し、かつ言語モデルおよび自動定理証明器のいずれも単独では解決できなかった問題の8.2%を解くことが可能になった。さらに、はるかに小さな計算リソースで運用可能なThorは、MiniF2Fデータセットにおいて、既存の最良手法と同等の成功確率を達成している。本研究で提示する簡単なプロトコルにより、Thorは多数の代表的な対話型定理証明器に容易に適用可能である。