FormulaOne: Measuring the Depth of Algorithmic Reasoning Beyond Competitive Programming

基本情報

• arXiv ID: 2507.13337v1 (https://arxiv.org/abs/2507.13337v1)
• 著者: Gal Beniamini 他12名（AAI所属）
• 所属: AAI
• 投稿日: 2025年7月18日
• カテゴリ: cs.AI, cs.LG

簡単に説明すると

この論文は、現在のAI（OpenAI o3など）のアルゴリズム推論能力の限界を明らかにする新しいベンチマーク「FormulaOne」を提案しています。グラフ理論、論理学、アルゴリズムの交差点にある非常に難しい動的計画問題120問から構成されています。AIモデルの成功率は1%未満という驚くべき結果を示しています。

GitHubで完全なデータセットと評価フレームワークが公開されています：
https://github.com/double-ai/formulaone-dataset-release

1. 研究概要

1.1 背景と動機

現在のAIベンチマークは、AIの推論能力の深さを十分に評価できていないという問題があります。OpenAI o3がCodeForcesで2724レーティングを達成するなど、競技プログラミングでの成功は目覚ましいものの、これらの成果は実世界の大規模な研究問題に必要な推論能力を反映していません。

サプライチェーン最適化、電力網管理、ネットワーク設計などの実世界の問題は、競技プログラミングの問題よりも桁違いに難しいです。これらの問題には、より深いアルゴリズム的洞察が必要です。また、既存のReinforcement Learning with Verifiable Rewards（RLVR）ベンチマークは限定的です。概念的深さが低い問題（学校レベルの数学など）か、静的で限定的なデータセットのいずれかに限られています。

この研究は、Courcelle（1990）のアルゴリズムメタ定理に基づいています。MSO論理を使用して、数学的に深く、かつ自動的に検証可能な問題を無限に生成できるフレームワークを構築しました。

1.2 主要な貢献

本研究の主要な貢献は次の3点です。

第一に、アルゴリズム推論の深さを測定する新しいベンチマーク「FormulaOne」を導入しました。120の難問と100の入門問題（FormulaOne-Warmup）から構成され、最先端AIモデルがほぼすべて失敗する難易度を持ちます。

第二に、MSO論理に基づく半自動的な問題生成フレームワークを開発しました。これにより、数学的に深い問題を無限に生成でき、将来のRLVR環境構築への道を開きます。

第三に、理論CS学との深い関連性を明らかにしました。多くの問題がStrong Exponential Time Hypothesis（SETH）と関連しており、AIによる新しいアルゴリズムの発見が理論的に重要な含意を持つ可能性があります。

2. 提案手法

2.1 手法の概要

FormulaOneは、グラフ上の動的計画問題の大規模コーパスを半自動的に生成するフレームワークです。その理論的基盤は、Courcelleのアルゴリズムメタ定理にあります。

この定理は次のことを保証します。十分に木のような構造を持つグラフに対して、MSO論理で定義可能な任意の問題は線形時間で解けます。動的計画法アルゴリズムを使用します。

各問題は次の形式で与えられます。

• 入力：木のようなグラフG=(V,E)、Gの木分解T、重み関数w:V→N
• 目的：特定のMSO論理式を満たす頂点部分集合の重みの総和を計算

2.2 技術的詳細

MSO論理式は、グラフの性質を表現する形式論理における文です。この論理では、頂点、辺、頂点集合、辺集合に対する量化（二階）を含む条件を定義できます。

各問題は単項開放式（unary open formula）で定義されます。入力集合のプレースホルダーとして機能する自由変数を1つ持ちます。問題の核心的な目的はWeighted Model Counting（WMC）です。与えられた論理式を満たすすべての部分集合の総重みを計算します。

木分解（tree decomposition）は、グラフを木構造に分解する補助的な構造です。線形時間での動的計画アルゴリズムの実行を可能にします。評価では、木分解上の単一のポストオーダー走査が許可されます。

2.3 新規性

既存のベンチマークとの主な違いは以下の通りです。

第一に、問題の深さです。FormulaOneの問題は、解法に15以上の相互依存する複雑な数学的推論ステップを必要とし、これは競技プログラミング問題とは質的に異なります。

第二に、半自動生成の能力です。MSO論理フレームワークを使用することで、数学的に深い問題を原理的に無限生成できます。静的なベンチマークの限界を克服します。

第三に、理論的保証です。Courcelleの定理により、生成されるすべての問題が線形時間で解けることが保証されています。しかし、その解を発見することは極めて困難です。

3. 実験結果

3.1 実験設定

評価では、4つの推論モデルを使用しました。OpenAI o3 high、OpenAI o3-Pro high、Google DeepMind Gemini 2.5 Pro、xAI Grok 4 Heavy。

各モデルには以下の支援を提供しました。

• 動的計画法の一般的アプローチを説明する詳細なプロンプト
• 問題記述と実装すべき4つの遷移関数の説明
• グラフクエリ用のユーティリティクラス
• モデルが苦手な領域から選んだ3つの多様なfew-shot例。

o3とGemini 2.5 Proには問題ごとに10回の独立した試行を許可し、o3-ProとGrok 4 Heavyには1回の試行を許可しました（後者は内部で複数サンプルを集約）。

3.2 主要な結果

FormulaOneデータセットでの成功率は驚くほど低く、120問中、次の結果となりました。

• Grok 4 Heavy：0問解決（0%）
• Gemini 2.5 Pro：1問解決（0.8%）
• OpenAI o3：1問解決（0.8%）
• OpenAI o3-Pro：1問解決（0.8%）

この低い性能は、提供された実質的な支援を考慮すると特に注目に値します。支援には多様なfew-shotプロンプト、入力解析、グラフ表現、木分解の構築と走査の自動処理が含まれます。

一方、FormulaOne-Warmupでは良い性能を示し、MSO論理に基づく問題の複雑性スペクトラムを明確に示しています。

3.3 既存手法との比較

他のベンチマークとの比較は以下の通りです。

• CodeForcesでは、o3が2724レーティングを達成するなど、AIは人間レベルの性能を示す
• ALE-BenchとCodeEloでは、トップモデルは急速に性能上限に近づいている
• ARCは明示的にout-of-distributionタスクを評価するが、FormulaOneはin-distribution

FormulaOneの特徴は、アルゴリズムコーディングというAIの得意分野でありながら、実世界の研究問題に必要な深い推論を要求する点です。競技プログラミングで人間専門家レベルの性能を示すモデルが、FormulaOneでは1%未満の成功率しか達成できません。これは現在のAIの限界を如実に示しています。

4. 実用性評価

4.1 実装の容易性

FormulaOneフレームワークは、研究者が使いやすいように設計されています。

GitHubで公開されている評価フレームワークには、問題生成、モデル評価、結果分析のための完全なツールセットが含まれています。MSO論理式から問題を生成する仕組みは半自動化されています。新しい問題の追加も比較的容易です。

ただし、問題自体の難易度は極めて高く、人間の専門家でも解くのは困難です。

4.2 計算効率

生成される問題はすべて、木幅パラメータに関して固定パラメータ線形時間（FPL）で解けます。これは理論的に保証されています。

しかし、実際の解法を発見することは極めて困難です。最適な動的計画の状態設計には深い洞察が必要です。評価環境では、木分解の構築と走査は自動的に処理されます。モデルは純粋にアルゴリズム設計に集中できます。

4.3 応用可能性

FormulaOneの応用可能性は多岐にわたります。

第一に、将来のRLVR環境の構築に適しています。無限の問題生成能力と自動検証により、深い推論を必要とする強化学習環境を構築できます。

第二に、AI研究の新しい方向性を示唆します。現在のモデルの失敗は、より構造化されたアプローチ（体系的な探索など）の必要性を示しています。

第三に、理論CS学への貢献の可能性があります。SETHと関連する問題での画期的なアルゴリズムの発見は、理論的に重要な意味を持ちます。

5. まとめと所感

5.1 論文の意義

この研究は、現在のAIの推論能力の限界を明確に示す重要な成果です。競技プログラミングで人間を凌駕するAIが、より深い推論を要求する問題では失敗するという結果は、現在のベンチマークの不十分さを浮き彫りにしています。

MSO論理に基づく問題生成フレームワークは、理論的に健全でありながら実用的に困難な問題を無限に生成できる点で画期的です。これは、AIの推論能力を測定し、向上させるための新しい道を開きます。

特に注目すべきは、問題の難しさが単なるパズル的な複雑さではなく、実世界の研究問題に特徴的な推論の深さから来ている点です。

5.2 今後の展望

将来の展望として、以下の方向性が考えられます。

第一に、より構造化されたアプローチの開発です。現在のモデルの失敗は、体系的な探索や階層的な推論など、新しいアーキテクチャの必要性を示唆しています。

第二に、FormulaOneの拡張です。現在のデータセットはMSO論理の一部（MSO1）のみを使用しています。MSO2や他の拡張、異なる目的関数、複数パス走査など、多くの拡張可能性があります。

第三に、理論と実践の橋渡しです。AIがSETH関連の問題で新しいアルゴリズムを発見すれば、理論CS学に大きな影響を与える可能性があります。