技術サマリー：GameGen-Verifier

問題定義

大規模言語モデル（LLM）に基づくゲーム生成システムの急速な進展は、信頼性の高い自動検証の欠如という重大なボトルネックに直面している。従来のコード生成では、正しさが静的なテストケースや短期間の入出力ペアによって決定されることが多いのに対し、ゲームの正しさは長期的な相互作用を通じて定義される。生成されたゲームは、正常にビルドされ視覚的に正しく見える場合でも、状態更新、相互作用ルール、フェーズ遷移といった中核的なメカニズムに違反している可能性がある。

既存の検証パラダイム、特に**検証者としてのエージェント（Agent-as-a-Verifier: AaaV）**は、自律エージェントに生成されたゲームをプレイさせ、仕様との照合を行うことでこの問題を解決しようとする。しかし、本論文は、AaaV がスケーラブルなゲーム検証には不十分であると主張する。その理由は以下の通りである：

1. 到達性の問題：検証者は特定のメカニズムに到達するために、長く開放的なゲームプレイの軌跡を探索する必要があり、検証に時間がかかり、カバレッジが制限される。
2. 状態空間の複雑性：ゲームの状態空間は指数関数的に成長するため、完全なカバレッジの実現は非現実的である。
3. エージェントの信頼性：検証はエージェント自身のゲームプレイ能力に依存することになり、複雑なシナリオではその能力がしばしば不安定となる。
4. ミスマッチ：ゲームプレイは探索を促進するのに対し、検証には体系的なカバレッジと失敗の因果帰属が必要である。

手法：GameGen-Verifier

著者らは、GameGen-Verifierを提案する。これは、検証を開放的な軌跡探索から、仕様由来のキーポイントに対する状態に基づく検証へと転換するパラダイムである。核心的な洞察は、仕様レベルの失敗は、ゲーム履歴全体を探索することなく、衝突処理、報酬の精算、フェーズ遷移などの局所的な重要行動の疎なセットによって露呈し得るという点にある。

この手法は、以下の 3 つの主要なコンポーネントで構成される：

1. 検証可能キーポイントの抽出と帰属

システムは、自然言語で記述されたゲーム仕様から「検証可能キーポイント」を抽出する。キーポイントは、自然言語によるホア式トリプル $\phi = (P, a, Q)$ として定義される：

• $P$（事前条件）：直接構築可能なゲーム状態。
• $a$（相互作用）：有界で有限の行動系列。
• $Q$（事後条件）：明確な期待結果。

これらのキーポイントは、構築可能性、有界性、検証可能性を確保する制約の下で LLM エージェントによって抽出される。その後、システムは判定結果を元の仕様要素に帰属させる。失敗したキーポイントは、それがカバーする仕様要素に対する「反証となる証拠」として機能し、依存する要素へと失敗を伝播させる。

2. パラメータベースの状態構築とランタイム注入

キーポイントを実行するには、事前条件 $P$ をインスタンス化する必要がある。ゲームプレイを通じてこの状態に到達するアプローチ（これは到達性の問題を再導入する）に代わり、GameGen-Verifier はゲームをデータ駆動型の状態機械として扱う。

• ホワイトボックスアクセス：LLM によって生成されたゲーム（特に Web スタックのゲーム）はソースコードを公開するという事実に基づき、検証者は内部状態（エンティティ、変数、フラグ）を支配するパラメータ構造を特定する。
• 状態パッチング：システムは $P$ を満たすターゲット状態のスナップショットを合成し、それをランタイム環境に直接注入する。これにより、動的な探索が静的な状態構築に変換される。
• 検証ユニット：各キーポイントは、注入された状態 $s_k$、有界な相互作用スクリプト $i_k$、期待結果 $y_k$ からなる具体的な検証ユニット $u_k = (s_k, i_k, y_k)$ にマッピングされる。

3. GGV-HARNESS：スケーラブルなエージェント検証ハーツ

これらの検証ユニットの実行を管理するため、著者らはGGV-HARNESSを実装する。これは、オーケストレーション層とワーカー層からなる 2 層構造である：

• オーケストレーション層（Python）：ユニットキューの管理、並行性の制限の強制、タイムアウト/リトライポリシーの適用、チェックポイントの永続化、および判定の集約を行う。
• ワーカー層：単一の検証ユニットにスコープされた短命の LLM エージェント呼び出しで構成される。ワーカーは、状態構築、相互作用スクリプトの生成、結果の判定（ビジョン・言語モデルとプログラム的なアサーションを使用）などのタスクを実行する。
• 保証：このハーツは、並行性の管理、ランタイムの分離（共有シードや状態による干渉の防止）、およびフォールト回復（全体を無効化することなく失敗したユニットを再試行可能にする）を提供する。

主要な貢献

1. 検証ボトルネックの特定：本論文は、到達性とカバレッジの制限により、既存の AaaV パラダイムがスケーラブルなゲーム検証には不十分であることを実証する。
2. GameGen-Verifier パラダイム：ゲーム検証を、仕様由来のキーポイントに対する状態に基づく有界なチェックへと再定式化する新しい検証フレームワーク。これにより、長期的な探索の必要性が排除される。
3. GGV-HARNESS：明示的な並行性制御、ランタイムの分離、およびフォールト回復を通じて、信頼性が高く再現性のある大規模検証を可能にするスケーラブルな実行ハーツ。
4. VERIGAME データセット：7 つのジャンル（アクション、アドベンチャー、カジュアル、パズル、シミュレーション、ストラテジー、ボード）にわたる 100 のゲーム生成タスクと自然言語仕様を含むデータセットの作成。これは自動検証ベンチマークのために特別に設計されたものである。

結果

システムは、VERIGAME 上で人間の専門家による判断および 2 つの AaaV ベースライン（AaaV-Direct と、TODO リストによるカバレッジ強制を行う AaaV-CE）に対して評価された。

• 精度：GameGen-Verifier は、人間の判断に対して最大92.2% の精度（Acc@5）および95.4% の F1@5を達成した。対照的に、カバレッジ強制型の AaaV-CE ベースラインは58.8% の精度しか達成できなかった。
• 効率性：GameGen-Verifier は、AaaV-CE に対して最大16.6 倍のウォールクロック時間の短縮を実現した（例：Codex バックエンドの場合、約 443 秒対約 7356 秒）。
• 堅牢性：システムは、異なる基盤エージェントバックエンド（Codex、Claude Code Opus、Claude Code Kimi）全体で高いパフォーマンスを維持し、一貫して AaaV ベースラインを上回った。
• ハーツのパフォーマンス：GGV-HARNESS は、エージェントネイティブなハーツと比較して実行時間を**66.4%**削減しつつ、ランタイムの分離とフォールト回復に必要な保証を提供した。

意義と主張

本論文は、GameGen-Verifier を、ゲーム生成を定性的なデモンストレーションから明確に定義された研究課題へと転換するための前提条件として位置づける。信頼性が高く、スケーラブルで、自動化された検証のメカニズムを提供することにより、この研究は以下のことを可能にする：

• ベンチマークの構築：ゲーム生成のための標準化されたベンチマークの作成。
• データキュレーション：高品質なトレーニングデータの生産規模の拡大。
• モデルの改善：ゲーム生成モデルのトレーニングフライホイールを維持するための信頼できるフィードバック信号（報酬信号）の提供。

著者らは、現在の実装が LLM 生成パイプラインの成熟度と、ブラウザ環境におけるランタイム状態パッチングの容易さから、Web スタックのゲーム（JavaScript/TypeScript/HTML）に焦点を当てていると指摘している。また、このパラダイムは理論的には Godot、Unity、Unreal Engine などのエンジンにも適用可能であるが、それらのパイプラインはこの特定のワークフローに対しては未成熟であると認めている。このアプローチは明示的に反証指向である。「PASS」という判定は、実行されたキーポイントのいずれも違反を露呈しなかったことを示すものであり、完全な正しさの形式的証明ではない。