BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving

要約

大規模な言語モデル（LLMS）の最近の進歩は、実証検索スペースをナビゲートするために効果的なツリー検索方法が重要であるLEAN4を使用して証明する自動定理への関心の高まりに拍車をかけました。
既存のアプローチは主に値関数とモンテカルロツリー検索（MCTS）に依存していますが、ベストファースト検索（BFS）のようなより単純な方法の可能性は未定です。
このペーパーでは、BFSが大規模な定理証明タスクで競争力のあるパフォーマンスを達成できるかどうかを調査します。
3つの重要な革新を備えたスケーラブルな専門家イテレーションフレームワークである\ texttt {bfs-prover}を提示します。
まず、各エキスパートの反復ラウンドで戦略的データフィルタリングを実装します。ビーム検索ノード拡張を介して解決可能な問題を除き、より難しいケースに焦点を当てます。
第二に、コンパイラエラーフィードバックで自動的に注釈された状態タクシーなペアに適用される直接選好最適化（DPO）を通じてBFSのサンプル効率を改善し、生産的拡張を優先するためのLLMのポリシーを改善します。
第三に、BFSで長さの正規化を採用して、より深い証明経路の調査を促進します。
\ texttt {bfs-prover}は、Minif2Fテストセットで71.31ドルのスコアを達成し、したがって、複雑なツリー検索方法の知覚された必要性に挑戦し、BFSが適切にスケーリングされたときに競争力のあるパフォーマンスを達成できることを実証します。

要約(オリジナル)

Recent advancements in large language models (LLMs) have spurred growing interest in automatic theorem proving using Lean4, where effective tree search methods are crucial for navigating proof search spaces. While the existing approaches primarily rely on value functions and Monte Carlo Tree Search (MCTS), the potential of simpler methods like Best-First Search (BFS) remains underexplored. This paper investigates whether BFS can achieve competitive performance in large-scale theorem proving tasks. We present \texttt{BFS-Prover}, a scalable expert iteration framework, featuring three key innovations. First, we implement strategic data filtering at each expert iteration round, excluding problems solvable via beam search node expansion to focus on harder cases. Second, we improve the sample efficiency of BFS through Direct Preference Optimization (DPO) applied to state-tactic pairs automatically annotated with compiler error feedback, refining the LLM’s policy to prioritize productive expansions. Third, we employ length normalization in BFS to encourage exploration of deeper proof paths. \texttt{BFS-Prover} achieves a score of $71.31$ on the MiniF2F test set and therefore challenges the perceived necessity of complex tree search methods, demonstrating that BFS can achieve competitive performance when properly scaled.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google