技術要約：デコード時文法 (Decode-Time Grammars)

1. 問題提起

大規模言語モデル（LLM）は、生成された出力が人間のレビューなしにコンパイルまたは実行されるエージェントやサービングシステムにおいて、コード生成のためにますます利用されています。これは主流のプログラミング言語においては機能しますが、低リソースなプログラミング・サーフェス（ドメイン固有言語（DSL）、カスタムライブラリAPI、コマンドラインツールなど）においては依然として脆弱です。

これらの環境における繰り返される失敗モードは、**ゴースト参照（ghost reference）**です。これは、構文的には有効なトークン（例：変数名、カラム、API関数、CLIオプション）でありながら、現在の実行環境 $\Gamma$ には存在しないものを指します。

• 例: TileLangカーネル内で宣言されていないバッファへの参照、SQLスキーマに存在しないカラムの選択、あるいは特定のライブラリバージョンでは利用できないイントリンジックの呼び出し。
• 根本原因: これらのエラーは多くの場合、**負の転移（negative transfer）**に起因します。モデルが、隣接する方言、古いAPIバージョン、あるいは異なるツールのインターフェースに関する知識をターゲット環境に適用してしまう現象です。
• 既存の救済策の限界:
  • 固定文法: 標準的な文法制約付きデコーディング（例：CFG）は、構文的な妥当性は保証しますが、参照位置を「開いたクラス」（例：identifier）として扱うため、有効な名前と無効な名前の両方を許容してしまいます。
  • モデル側の救済策: プロンプティング、ファインチューニング、またはリトライメカニズムは、エラーの確率を減少させることはできますが、モデルのサポート集合から無効な継続（continuation）を取り除くことはできません。これらは、モデルが正しいパスを「好む」ことに依存していますが、誤ったパスが流暢で高確率である場合には不十分です。

2. 手法：デコード時文法

本論文では、生成中に実行環境 $\Gamma$ に基づいて文法断片（grammar fragments）を動的にインスタンス化するフレームワークであるデコード時文法を導入しています。

コアメカニズム

1. 実行環境 ($\Gamma$): 現在の状態のスナップショットであり、スコープ内の名前、型（sorts）、形状（shapes）、スキーマのエントリ、APIメンバ、またはツールの状態を含みます。$\Gamma$ は宣言が生成されるにつれて進化します。
2. 文法断片と精緻化順序 (Grammar Fragments & Refinement Order): 単一の固定文法の代わりに、システムは精緻化（$\sqsubseteq$）によって順序付けられた文法断片のライブラリを使用します。
   • 断片は、粗いもの（例：任意の識別子を受け入れる）から緻密なもの（例：$\Gamma$ 内で宣言された名前のみを受け入れる）まで多岐にわたります。
   • 各リージョンのポリシー $\pi(s, \Gamma)$ は、期待される型 $s$ と現在の環境に基づいて、特定の「穴（hole）」（生成における型付きの位置）に対して適切な断片を選択します。
3. $\tau_\Gamma$ オペレータ（タイトニング）: これが極めて重要なメカニズムです。これは、断片内の開いた参照位置を$\Gamma$ 型スロットへと変換します。
   • スロットの候補セットは、まさに $\Gamma$ で利用可能な名前です（例：Gamma.names(sort=Buffer)）。
   • これらの候補は、エスケープされたオルタネーション（例："A" | "B" | "C"）へとコンパイルされ、そのリージョンをデコードする前にトークンレベルの認識器に注入されます。
4. 自己拡張型生成 (Self-Extending Generation): モデルが宣言を生成するにつれて、それらは抽出され、後続の参照の穴がデコードされる前に $\Gamma$ に追加されます。これにより、参照が既に生成されたプレフィックスによって制約されることが保証されます。

システムアーキテクチャ

実装である gproj は、2つのコンポーネントで構成されています。

• TemplateInductor (オフライン): アンチ・ユニフィケーション（anti-unification）を用いて、小さなコーパスから文法断片とポリシーを誘導します。これは、実行可能性と正確性を確保するために、コーパスのポジティブ例と自動生成されたネガティブ例（掘り出されたゴースト参照を含む）を用いて、「ハードゲート」に対して断片を検証します。
• gproj Executor (オンライン): $\Gamma$ を維持し、ポリシー $\pi$ をクエリし、$\tau_\Gamma$ を通じて断片をインスタンス化し、結果としての文法をLLMデコーダ（例：XGrammar）用のトークンマスクへとコンパイルする、オンライン・マスク実行器です。

3. 主要な貢献と形式的な結果

理論的貢献

• ゴースト不在の健全性 (No-Ghost Soundness): 参照位置が $\Gamma$ 型スロットとして実現されているあらゆる断片において、生成された文字列は**構成上、スコープに対して安全（scope-safe）**であることを証明しています。すべての放出された参照は、必ず $\text{dom}(\Gamma)$ に含まれます。
• 精緻化の保存 (Refinement Preservation): 緩い断片が健全であれば、より緻密な精緻化（$\tau_\Gamma$ による）もこの健全性を保持することを証明しています。これにより、エラーを再導入することなく、動的に断片の強度を切り替えることが可能になります。
• 動的サポートの必要性 (Proposition 3): 固定された参照サポートを持つ有限の事前コンパイル済み文法ファミリーでは、無制限の識別子空間に対して、健全（ゴースト参照がない）かつ非ブロッキング（すべての有効な継続を許容する）の両立は不可能であることを証明しています。
  • 示唆: 正確な参照サポートは、デコード中にプレフィックスに基づいて合成されなければなりません。静的な事前コンパイルだけでは、宣言一貫性のある言語に対して理論的に不十分です。

実践的貢献

• 役割の分担: このアプローチは、環境に拘束された正当性（マスクが担当）と、開かれたプログラム上の決定（モデルが担当）を分離しています。マスクは参照が有効であることを保証し、モデルはアルゴリズム、戦略、または意図を選択します。
• 誘導パイプライン: 小さなコーパスから必要な文法断片とポリシーを自動的に生成する手法を提供しており、手動の文法エンジニアリングなしに新しいDSLへ適用可能です。

4. 評価結果

システムは、TileLang（テンソルカーネルDSL）、SQL（Spiderデータセット）、P4（データプレーン言語）、およびCLIツール（git, FFmpeg）を用いて、0.6Bから236Bパラメータに及ぶモデルで評価されました。

• ゴースト参照の排除:
  • すべてのサーフェスにおいて、$\Gamma$ 型アーム（$\tau_\Gamma$ を使用）は、構成上0%のゴースト参照を達成しました。
  • 対照的に、オープン識別子アーム（自由デコーディング）は、モデルのサイズ（0.6Bから236B）に関わらず、TileLang、SQL、P4において100%のケースでゴースト参照が発生しました。
  • 例: SQLにおいて、オープン識別子は実行一致率0%となりましたが、$\Gamma$ 制約付きデコーディングは100%を達成しました。
• モデルへの独立性: この保証はモデルサイズ間で転移します。236Bの最先端モデル（DeepSeek-V4-Flash）であっても、マスクなしでは有効な参照を生成できませんでしたが、0.6Bのモデルはマスクを用いることで成功しました。
• 代替手法との比較:
  • プロンプティング/リトライ: SQLにおいて、スキーマを用いたプロンプティングと最大4回のリトライを行った結果、実行一致率は90%に達しましたが、依然として5つのゴーストカラムが発生しました。マスクを用いた手法は、1回のパスでゴーストなしの100%一致を達成しました。
  • コスト: このアプローチは適度なオーバーヘッドを伴います。非制約デコーディングと比較して、エンドツーエンドのスループット低下は平均**17.3%でした。標準的な制約付きデコーディング（XGrammar）と比較した場合、gprojによるスループット低下は10.6–17.8%**でした。
• オフライン誘導: TemplateInductorは、手書きされていない複雑なサーフェス（例：AscendCオペレータ、FFmpegフィルタ）に対しても有効な断片を正常に誘導し、「誘導 ＋ ハードゲート」のワークフローの妥当性を証明しました。

5. 意義と主張

著者らは、デコード時文法が、モデルの能力とは独立した、正確性の精密かつ安定したスライスを提供すると主張しています。

• 機械的な保証: これは、参照の安全性を、モデルの品質に依存する確率的な結果から、構成レベルの保証へと変貌させます。
• スケーラビリティ: 「意味的なスケッチ」（モデルの仕事）と「環境に拘束された参照」（マスクの仕事）を分離することで、本来であれば幻覚を起こしてしまうような低リソース環境においても、弱いモデルが有効なコードを生成することを可能にします。
• 理論的必然性: 静的な文法では、宣言一貫性のある言語に対して健全かつ非ブロッキングであることは同時に成立しないという証明は、提案された実行時インスタンス化アプローチの必要性を確立しています。

著者らは、本研究をプログラム全体の意味的な正当性（例：アルゴリズムの論理や停止性）のための解決策としてではなく、制約された環境におけるコード生成を悩ませる、特定のクラスの機械的に列挙可能なエラー（未定義のシンボル）を排除するための堅牢なメカニズムとして位置づけています。