BFS-Prover - ByteDanceが開発した自動定理証明システム。

BFS-Proverとは何ですか？

ByteDanceのDoubao Big Model Teamが開発したBFS-Proverは、大規模言語モデル（LLM）に基づく自動定理証明システムです。従来の幅優先探索（BFS）アルゴリズムを改良し、エキスパート反復と直接選好最適化（DPO）技術を組み込むことで、非常に効率的な証明探索を実現しています。その核となるのは、長さ正規化スコアリングヒューリスティックであり、累積対数確率を用いて証明パスの優先順位付けを行い、探索効率を最適化します。エキスパート反復フレームワークを採用することで、複雑な定理の解決に重点を置き、DPOを用いてコンパイラのフィードバックに基づいてポリシーモデルを最適化し、無効な推論パスを回避します。BFS-Proverは、分散アーキテクチャによって大規模な並列証明探索を実現し、高並行タスクをサポートします。

BFS-Proverの主な機能

• 効率的な証明検索BFS-Proverは、改良された幅優先探索（BFS）アルゴリズムを採用し、長さ正規化スコアリングメカニズムを通じて深い推論パスを探索する能力を最適化しています。また、探索プロセス中に計算リソースを動的に割り当て、探索と利用のバランスを取ることができます。
• 継続的な改善とデータ蓄積このシステムは、LLM生成戦略 → LeanDojo実行 → フィードバック取得 → トレーニングデータ生成 → LLM最適化という閉ループを形成します。反復処理により、モデルはより多様な証明戦略を学習できます。

BFS-Proverの技術的原理

• 長さ正規化スコアリングメカニズムBFS-Proverは、長さ正規化スコアリング関数を採用しており、パスの累積対数確率をパスの長さのべき乗（α∈[0,1]）で割ることによって、従来のBFSが深いパスに課すペナルティを軽減し、複雑な証明をより効果的に探索することができます。
• 専門家による反復と自己フィルタリングこのシステムは、専門家による反復的なフレームワークを採用し、証明対象としてより複雑な定理を段階的に選択していきます。各反復において、ビームサーチを用いて容易に解ける定理を除外し、これらの単純な問題を訓練データから削除して、より難易度の高い定理の解決に集中します。反復が進むにつれて、モデルは徐々に複雑な証明戦略を学習し、証明の長さの分布は短い戦略から長い戦略へと変化していきます。
• 直接選好最適化（DPO）BFS-Proverは、コンパイラからのDPO（深度点エラー分析）フィードバックに基づいてポリシーモデルを最適化します。同じ状態における成功したポリシーと失敗したポリシーを比較することで、モデルは無効な推論パスを回避し、探索効率を向上させることができます。
• 分散型証明アーキテクチャ大規模な並列証明を実現するため、BFS-Proverは分散システム設計を採用し、Rayフレームワークを用いて複数のマシン上で動作します。各マシンには複数のGPUとCPUコアが搭載されています。これにより、ほぼ線形のスケーラビリティが実現され、ハードウェアの利用率が最大化されます。
• Lean4との緊密な統合BFS-ProverはLeanDojoおよびLean4と連携して、数学の問題を形式体系にエンコードし、検証可能な機械証明を生成し、証明の論理的な正しさを保証します。

BFS-Proverプロジェクトの住所

• ハギングフェイスモデルライブラリ：https://huggingface.co/bytedance-research/BFS-Prover
• arXiv技術論文：https://arxiv.org/pdf/2502.03438

BFS-Proverの応用シナリオ

• 形式的な数学問題の自動証明BFS-Proverは、数学の問題を形式言語（Lean4など）にエンコードし、様々な数学分野における定理証明に適用可能な検証可能な機械証明を生成することができます。
• 数学コンテストの問題を解く複雑な国際数学オリンピック（IMO）の問題を解くことができ、複雑な数学的推論における高い能力を示すことができる。
• 学部および大学院レベルでの数学研究BFS-Proverは、学部生および大学院生レベルの数学的定理証明問題の解決を支援します。
• 自動定理証明技術の開発を促進するBFS-ProverはMiniF2Fテストセットにおいて精度記録を更新し、自動定理証明の分野に新たな手法と技術的なアイデアを提供した。