定理証明の探索予算に合わせて言語モデルを学習する
Direct Optimization of Generators for Search in Automated Theorem Proving
この論文をやさしく読む
ひとことで言うと
定理証明で木探索を行う言語モデルを、探索の成功と計算予算に合うよう学習する方法を調べた。
何に役立つ？
Leanでの自動証明システムを設計する際、探索に使うモデルの学習目標を選ぶ参考になる。実験では6種類の探索戦略で証明成功率を比較した。
この研究の面白いところ
探索方式に依存する損失に加え、共通のアダプターで使える一様割当損失も提案し、どちらも交差エントロピーを上回った。少ない展開回数で改善幅が大きい。
どこまで分かった？
結果は要旨に記載されたLeanベンチマークと探索予算に基づく。正解経路外の振る舞いは学習上の難点であり、近似誤差が消えるのは示された条件の下である。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
微調整した大規模言語モデル（LLM）は自動定理証明を大きく前進させたが、1回で証明を生成するより、木探索を導く方策として使われることが多い。最近の研究は、候補の集約や絞り込みのような平坦な探索戦略でLLMを用いる場合、交差エントロピーが最適ではないことを示し、このずれを修正する損失関数を開発した。しかし、木探索に合わせて学習させるのはより難しい。証明の発見は、教師ありの実演には現れない、正解経路から外れた状態での探索や立て直しにも依存するためである。 著者らは、方策で導く探索の抽象化を通じてCompute-Aligned Training（CAT）を木探索へ拡張し、探索の軌跡で裏付けられ、計算可能な損失を導く。探索を考慮したこれらの損失に加え、具体的な探索方式を指定せずに計算予算を考慮する、探索非依存の一様割当（UA）損失も導入する。どちらも、各証明戦術の交差エントロピー勾配にスカラーの重みを与える。著者らは、正解経路外の振る舞いが探索を考慮した重みにどう影響するかを特徴付け、大きな予算で近似誤差が消える条件も示す。 Leanのベンチマークでは、両手法とも6種類の探索戦略すべてで、交差エントロピー学習より観測された証明成功率が高かった。共通のUAアダプター1つでも良好な結果が得られた。予算を変えた実験では、交差エントロピーに対する改善幅は展開回数256回より16回で大きく、CATの効果が推論時の計算量に応じて変わることを示唆した。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-22（UTC）
- 最新改訂
- 2026-09-22 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-22 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Fine-tuned Large Language Models (LLMs) significantly advance Automated Theorem Proving (ATP), but are often deployed as guiding policies within tree search rather than for single-attempt generation. Recent work shows cross entropy is suboptimal for an LLM used in flat search strategies such as aggregation or filtering and that work has developed new loss functions to correct this misalignment. Extending this alignment to tree search is more challenging: proof discovery depends on exploration and recovery through off-trace states that supervised demonstrations do not reveal. We extend Compute-Aligned Training (CAT) to this setting through an abstraction of policy-guided search, deriving tractable, trace-supported losses. Alongside these search-aware losses, we introduce a search-agnostic uniform-allocation (UA) loss that accounts for the budget without specifying the specific search. Both induce scalar weights on per-tactic cross-entropy gradients. We characterize how off-trace behavior affects the search-aware weights, including conditions for vanishing approximation error at large budgets. On a Lean benchmark, both approaches achieve higher observed proof-success rates than cross-entropy across six search strategies, with strong results from a single shared UA adapter. Budget sweeps show larger gains over cross-entropy at 16 than at 256 expansions, implying CAT scales with test time compute.
arXiv ID: 2609.25575 ／ 要約の誤りについて