ByteDanceのSeed-Prover、自動数学証明でSOTAを達成

大規模言語モデル（LLM）は、数学的推論において目覚ましい進歩を遂げており、MATHやAIMEなどのベンチマークで性能を向上させるために、その自然言語能力を活用することがよくあります。しかし、強化学習（RL）でこれらのモデルを訓練する際の主要な課題は、自然言語による証明の正確性を検証することの難しさです。これは通常、各ステップを綿密に手動でチェックする必要があるためです。この制約は、数学定理証明モデルの開発におけるRLのより広範な応用を妨げています。Leanのような形式言語は自動的な正確性検証を提供しますが、現在のLLMベースの形式証明器にはまだ限界があります。例えば、ステップレベルの証明器はコードを段階的に生成しますが、多くの場合、特定の構造的サポートを必要とし、高レベルの推論に苦慮します。

これに対し、ByteDanceのSeedチームは、新しい補題スタイルの全証明推論モデルであるSeed-Proverを発表しました。Seed-Proverは、Leanからのフィードバックを取り入れ、以前に確立された補題を活用し、自己要約を用いることで、証明を反復的に洗練させます。テスト時には3つの専門的な推論戦略を統合し、国際数学オリンピック（IMO）で見られるような複雑な問題に取り組むための深く幅広い推論能力を可能にします。その核となる革新は、推論プロセスを従来のステップバイステップまたはモノリシックな全証明生成方法ではなく、補題を中心に据える補題スタイルの証明アプローチを採用している点にあります。これを補完するものとして、Seed-Geometryも導入されました。これは、幾何学的な問題の処理におけるLeanの限界を克服するために設計された、専門的な幾何学推論エンジンです。

Seed-ProverとLean間の相互作用は、VAPOに基づく多段階・多タスク強化学習フレームワークによって促進されます。訓練データセットは、公開されているデータセットとByteDance社内の形式的問題を組み合わせています。「提案者」コンポーネントは、難しいタスクのより単純なバリエーションを生成するために使用され、過度に単純な問題（証明率が25%を超えるもの）は除外されます。Seed-Geometryのバックエンドは大規模な問題生成をサポートしており、7日間で2億3000万以上のユニークな問題を特定し、検索効率が8倍向上したことを示しています。個別のポリシーモデルと価値モデルが訓練されますが、広範なテストでは、価値モデルが推定誤差のためにパフォーマンスを低下させる場合があることが示され、分散設定ではビームサーチによるステップバイステップ生成が採用されました。

Seed-Proverは、いくつかの数学ベンチマークで最先端の結果を達成しました。IMO 2025では、Seed-Proverは6問中5問の解決に成功しました。具体的には、Seed-Geometryが問題2を即座に解決し、Seed-Proverはさまざまな推論設定を使用して残りの問題の証明を導き出しました。過去のIMO問題では、155問中121問を証明し、すべての難易度レベルで78.1%の成功率を達成しました。このパフォーマンスには、簡単な問題55問中47問、中程度の問題56問中47問、難しい問題44問中27問の解決が含まれます。科目別の成功率も高く、代数では85問中72問、数論では55問中42問、組み合わせ論では14問中7問でした。

MiniF2Fベンチマークでは、研究者らは中程度の設定で検証セットとテストセットの両方で99.6%の証明率を報告し、IMO 1990 P3のような挑戦的な問題の解決に成功しました。PutnamBenchの結果は、ライトな推論設定からミディアムにアップグレードした際に、657問中解決問題数が201問から331問へと大幅に改善したことを示し、これまでの学部レベルの数学的推論システムを上回る顕著な性能向上を記録しました。Seed-ProverはCombiBenchで組み合わせ論の問題100問中30問を解決し、既存の手法を上回りましたが、その結果は組み合わせ論的推論における継続的な課題も浮き彫りにしました。さらに、Seed-ProverはMiniCTX-v2で81.8%の成功率を達成し、競技特有の問題を超えた強力な汎化能力を示し、Pass@8でのo4-miniベースラインの44.3%を上回りました。

要約すると、ByteDanceのSeedチームは、LLMの能力を効果的に統合する2つの形式的推論手法、Seed-GeometryとSeed-Proverを導入しました。Seed-Geometryは幾何学的な問題に対して高速な検証と強化された検索メカニズムを提供し、Seed-Proverは反復的な洗練と複雑なテスト時推論戦略を一般的な数学的証明に活用します。IMO 2025で6問中5問を解決したという成果は、これらの手法がエリート数学競技会に取り組む上での実用的な有効性を裏付けています。Leanのような形式言語の採用は、人間の専門家よりも費用対効果が高く、LLMベースの評価者よりも信頼性の高い迅速な証明検証を提供します。将来の研究は、未解決の数学的予想に取り組むために、形式システムとLLMをさらに組み合わせることに焦点を当てていきます。