|
数学的推論における人工知能の重要な応用として、形式的な数学定理の自動証明が挙げられます。このようなタスクでは、数学的な命題と証明手順をコンピュータで検証可能なコードに変換する必要があります。これにより、推論プロセスの絶対的な厳密性が保証されるだけでなく、再利用可能な数学的知識ベースの構築が可能になり、科学研究のための強固な基盤が提供されます。 20世紀半ばには、デイビスやミンスキーといった多くの論理学者、数学者、そして人工知能の先駆者たちが、すでに関連する問題を研究していました。その中には、王浩や呉文軍といった中国の著名人もいました。 近年、LLM 機能のサポートにより、自動定理証明システムは、検索プロセスをガイドするために複雑なモンテカルロ ツリー検索 (MCTS) や値関数にますます依存するようになりました。 ただし、これらの方法では追加の計算コストが発生し、システムの複雑さが増し、大規模な推論タスクにおけるモデルのスケーラビリティが制限されます。 ByteDance の Doubao Big Model チームによって立ち上げられた BFS-Prover は、この従来のパラダイムに挑戦します。 よりシンプルで軽量でありながら、非常に競争力のある自動定理証明システムとして、1) エキスパート反復と適応型データフィルタリング、2) Lean4 コンパイラフィードバックと組み合わせた直接選好最適化 (DPO)、3) BFS での長さの正規化という 3 つの主要テクノロジを導入しています。 結果によると、BFS-Prover は正式な数学テストセット MiniF2F で 72.95% の精度を達成し、この分野で新記録を樹立しました。 この結果はまた、合理的な最適化戦略の下では、単純な BFS 法がモンテカルロ ツリー検索 (MCTS) や値関数などの主流の複雑な検索アルゴリズムよりも優れていることを初めて実証しています。 論文の成果は公開されており、モデルは最近オープンソース化されました。関係する研究者とのさらなる交流を楽しみにしています。
パート 1: 主流の方法であるモンテカルロ ツリー検索と価値関数は本当に必要ですか?正式な数学的証明の分野では、抽象的な数学的概念をコンピューターで検証できる厳密な形式に変換することは、極めて困難な作業です。 このプロセスでは、推論の各ステップが厳密な形式論理ルールに準拠する必要があり、各ステップは Lean 証明アシスタントによって検証される必要があります。 形式定理の自動証明プロセスにおいて、コンピュータが直面する中心的な課題は、広大かつ高度に構造化された証明空間内で効率的な経路を見つけることです。この困難は、従来の探索問題とは根本的に異なり、具体的には以下のようになります。
DeepSeek-Prover-V1.5、InterLM2.5-StepProver、HunyuanProver などの既存の自動定理証明システムは、主に複素モンテカルロ木探索 (MCTS) と値関数に依存して上記の問題を解決しています。 これらのAlphaZeroに似たアルゴリズムフレームワークは、ゲーム、特に囲碁において非常に優れたパフォーマンスを発揮し、強化学習の概念を主流へと押し上げました。しかし、自動定理証明の分野では、前述の主流の手法は、状態空間が非常に複雑であることと、明示的なプロセス報酬シグナルが欠如していることから、理想的とは言えません。さらに、複雑な探索アルゴリズムは、計算コストの増大とシステムの複雑性の増大にもつながります。 パート2：複雑さの単純化：機械で数学の定理を簡単に証明する人間は問題に直面したとき、その問題を解決する可能性が最も高い方法を優先する傾向があります。この点では、最良優先木探索（BFS）も同様です。 これは、木やグラフ内のノードを探索するアルゴリズムです。基本的な考え方は、ヒューリスティック関数に基づいて各ノードの優先度を評価し、優先度に従ってノードを訪問することです。制約充足問題や組合せ最適化問題、特に近似最適解を迅速に求める必要がある場合によく使用されます。 これまで多くの研究者は、単純なBFSアルゴリズムには効果的な探索メカニズムが欠けており、特に深い経路の探索には不十分で、大規模な定理証明タスクの処理が困難であると考えていました。しかし、Doubao Big Modelチームの研究者たちは画期的な発見をし、BFS-Proverシステムを提案しました。 以下の図は、BFS-Prover システムの全体的なアーキテクチャとワークフローを示しています。 右側には、教師あり微調整用の SFT データ (パス上の状態とポリシーのペアを正常に証明する) と直接的な好みの最適化用の DPO データ (同じ状態から開始して正しいポリシーと誤ったポリシーを比較する) を含むトレーニング データ生成プロセスが表示されます。 左側は、LeanDojo環境を介してLean4と連携するBFSメカニズムを示しています。ルートノードから開始し、優先度順（1→2→3…）に証明パスを探索し、証明が完了するまで（緑の点A）、証明パスを探索します。 システム全体は、LLM が戦略を生成 → LeanDojo が実行 → フィードバックを取得 → トレーニング データを生成 → LLM を最適化 → 再度戦略を生成という閉ループを形成し、継続的な改善エキスパート反復メカニズムを実現します。 チームは、BFS-Proverシステムは、最適化されたBFS法が複雑なMCTSや価値関数よりも性能面で優れていることを実証するだけでなく、アーキテクチャのシンプルさと計算効率も維持していると考えています。その技術的特徴は次のとおりです。
BFS-Proverはエキスパート反復フレームワークを採用しており、複数の反復処理を通じてLLM機能を継続的に強化します。各反復処理において、システムはまず決定論的ビーム探索法を用いて容易に解ける定理を除外し、「複雑な問題」に取り組む前に、これらの「単純な問題」をトレーニングデータから除去します。 このデータ フィルタリング メカニズムは非常に革新的で、トレーニング データが徐々により困難な定理証明タスクへと移行し、LLM がより多様な証明戦略を学習できるようになります。 以下の実験データに示されているように、反復により、システムは証明の平均長が増加し、カバレッジが広くなることを検出でき、この方法の有効性が証明されます。 同時に、LLM によって生成されるポリシー分布も進化します。 下の図に示すように、複数回の反復後、モデルによって生成されたポリシーの長さの分布は大幅に変化しました。非常に短いポリシー (1〜10 トークン) の割合は減少し、中程度の長さのポリシー (11〜50 トークン) の割合は増加しました。 この分布の変化は、LLM の「深い思考能力」が強化され、強化学習によって発生する一般的な分布崩壊問題を回避し、より複雑で情報量の多い証明戦略を徐々に習得していることを示しています。 同時に、簡潔な戦略を生成するモデルの能力も放棄されたわけではありません。多様な戦略を生成するこの能力を維持することは、効率的な定理証明にとって非常に重要です。なぜなら、証明状態によって、単純な項書き換えから複雑な代数演算に至るまで、様々な複雑さの戦略が必要となるからです。
証明検索プロセス中に、LLM によって生成された特定の戦略が Lean4 コンパイラーでエラーを引き起こす場合、システムはこれらの無効な戦略を成功した戦略と組み合わせて、負のフィードバック信号を形成します。 BFS-Proverは、このデータを革新的に活用し、直接選好最適化（DPO）手法に基づいて政策LLMを最適化します。この手法により、効果的な政策を特定するモデルの能力が大幅に向上し、政策配分が最適化され、BFSのサンプリング効率が向上します。 以下の実験結果が示すように、DPO 最適化モデルはさまざまな計算スケールにわたってパフォーマンスの向上を達成し、定理証明における負の信号の重要な価値を実証しました。
深い推論パスにおける BFS の固有の制限に対処するために、BFS-Prover システムは調整可能な長さ正規化スコアリング関数を導入します。 ここで、Lはパス長を表し、αは調整可能な長さ正規化パラメータです。αの値を適切に調整することで、システムは高確率パスの利用と深いパスの探索のバランスをとることができ、BFSは長鎖証明をより効果的に探索できるようになります。 パート3: BFS-ProverがMiniF2Fの新しいSOTAを取得 チームは、MiniF2Fテストセットを用いてBFS-Proverの包括的な評価を実施しました。このテストセットは形式数学におけるベンチマークとして認められており、非常に難易度の高い競技レベルの数学問題が含まれており、自動定理証明システムの能力を測定するために広く使用されています。
BFS-Prover は、主要な定理証明システムと比較して大きな利点を示します。 固定のポリシー生成計算負荷（2048×2×600回の推論呼び出し）で、BFS-Proverは70.83％の精度を達成し、価値関数を使用するInternLM2.5-StepProver（65.9％）とHunyuanProver（68.4％）、MCTSに基づくDeepSeek-Prover-V1.5（63.5％）を含む既存のすべてのシステムを上回りました。 累積評価では、BFS-Prover は精度をさらに 72.95% まで向上させ、形式定理証明の分野で最先端技術 (SOTA) となりました。 この結果は、BFS 方式の可能性を示すだけでなく、慎重に設計することで、単純なアルゴリズムでも複雑なアルゴリズムよりも優れたパフォーマンスを発揮できることを示しています。
BFS-Prover は、imo_1959_p1、imo_1960_p2、imo_1962_p2、imo_1964_p2、imo_1983_p6 など、MiniF2F テストでいくつかの IMO 問題を正常に証明したことは注目に値します。 これらの証明は、数論、不等式、幾何学的関係を含む複雑な数学的推論を処理するシステムの強力な能力を実証しています。 たとえば、imo_1983_p6 不等式問題の場合、BFS-Prover は簡潔でエレガントな形式証明を生成できます。 結論はチームは、BFS-Prover の成功は、自動定理証明の分野への重要な洞察を意味すると考えています。簡潔なアルゴリズムと適切に設計された最適化戦略を組み合わせることで、AI4Math の境界を拡大することもできます。 大規模言語モデル機能が継続的に改善されるにつれ、BFS-Prover が先駆けとなった簡潔で効率的なアプローチにより、自動形式定理証明の分野の発展がさらに促進され、数学研究をサポートするより強力な自動ツールが提供されることが期待されます。 今後、研究チームはBFS法の能力をさらに強化し、特に学部・大学院レベルの数学定理など、より複雑な数学問題への対応力を強化する予定です。同時に、推論モデルやその他の最先端のアプローチに基づいて、このモデルの可能性をさらに探求していきます。 チームは、データとトレーニング戦略を継続的に最適化することで、関連ツールが数学研究に強力な支援を提供し、数学の発見のプロセスを加速し、最終的には最先端の数学の課題を解決するための人間と機械のコラボレーションのビジョンを実現できることを期待しています。 |
