コンパイルで圧縮する：コンパイラ出力で形式的定理証明器を強化する

要旨: 大規模言語モデル（LLM）は形式的定理証明において大きな可能性を示している一方で、最先端の性能を得るには、巨大なロールアウトや拡張されたコンテキストウィンドウによる、しばしば禁止的なテスト時計算が必要となることが多い。本研究では、形式的検証における有益な構造を活用することで、このスケーラビリティのボトルネックに取り組む。すなわち、コンパイラが、多様な証明試行の膨大な空間を、コンパクトな形で構造化された失敗モードの集合へと写像している、という観察である。我々は、この圧縮を利用して効率的な学習と証明探索を行う、learning-to-refine（洗練のための学習）フレームワークを提案する。明示的な検証器からのフィードバックに条件付けて、誤りを局所的に修正する木探索を行うことで、証明試行の長い履歴を蓄積することに伴うコストを回避する。大規模な評価により、本手法が、規模が異なる状況においても、基礎となる証明器の推論能力を一貫して増幅することを示す。特に我々のアプローチは、同程度のテスト時予算の下で、公に報告されている約8Bおよび約32Bパラメータのモデルにおいて、PutnamBenchで最先端の性能を達成し、次世代の検証器ガイド付き推論のためのスケーラブルなパラダイムを提供する。