論文の概要: AGDecode: Semantic Attribute Grammar Derivatives for Safety-Constrained Decoding of Large Language Models
- arxiv url: http://arxiv.org/abs/2610.36105v1
- Date: Mon, 26 Oct 2026 18:18:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-28 21:04:31.399105
- Title: AGDecode: Semantic Attribute Grammar Derivatives for Safety-Constrained Decoding of Large Language Models
- Title（参考訳）: AGDecode: 大規模言語モデルの安全性制約付き復号化のためのセマンティック属性文法デリバティブ
- Abstract要約: 制限された復号化は、トークンの選択を少なくとも1つの有効な完了を認めるものに制限することで、生成中の正しさを強制する。
我々は,最小固定点意味論に基づく意味制約デコーディングのためのプログラム可能なフレームワーク AGDecode を提案する。
- 参考スコア（独自算出の注目度）: 6.037300555559242
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models (LLMs) are increasingly used for code generation, motivating techniques that guarantee the structural and semantic correctness of generated programs. Constrained decoding enforces correctness during generation by restricting token choices to those that admit at least one valid completion. While existing approaches can enforce syntactic constraints and selected semantic properties such as type safety, they either target specific properties or rely on operational pruning mechanisms that are difficult to generalize to data-dependent, inductive program properties. We present AGDecode, a programmable framework for semantic constrained decoding based on least-fixed-point semantics. AGDecode extends attribute grammars to partially constructed syntax trees, and reduces semantic constrained decoding to a realizability problem over such trees. The framework compiles semantic specifications into systems of relational constraints that are discharged by external verification oracles, such as SMT and CHC solvers, cleanly separating language semantics from constraint-solving machinery. We prove that our approach is sound and complete relative to an ideal verification oracle. In practice, solvers inevitably encounter uncertain queries; conservatively, our system can reject tokens for soundness or speculatively continue to generate until later queries resolve the entire generation. We mechanize the core metatheory in Rocq and evaluate the framework on semantic-constrained generation of C programs, enforcing path-sensitive safety properties including null-pointer safety, division-by-zero freedom, and initialized-variable usage. Our results demonstrate that solver-backed semantic constrained decoding can enforce rich semantic guarantees while incurring modest computational overhead at regular program boundaries.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、コード生成や、生成されたプログラムの構造的および意味的正当性を保証するテクニックのモチベーションに、ますます使われるようになっている。
制限された復号化は、トークンの選択を少なくとも1つの有効な完了を認めるものに制限することで、生成中の正しさを強制する。
既存のアプローチでは、型安全性のような構文制約や選択されたセマンティックプロパティを強制することができるが、特定のプロパティをターゲットにするか、データ依存のインダクティブなプログラムプロパティへの一般化が難しい運用プルーニングメカニズムに依存している。
我々は,最小固定点意味論に基づく意味制約デコーディングのためのプログラム可能なフレームワーク AGDecode を提案する。
AGDecodeは属性文法を部分的に構築された構文木に拡張し、意味制約付きデコーディングをそのような木上の実現可能性問題に還元する。
このフレームワークは、セマンティック仕様を、SMTやCHCソルバといった外部の検証オラクルによって排出されるリレーショナル制約のシステムにコンパイルし、制約解決機械から言語セマンティックスをきれいに分離する。
我々は,本手法が理想的な検証オラクルに対して健全かつ完全であることを証明した。
保守的に、我々のシステムは、音質のトークンを拒否したり、投機的に、後続のクエリが全生成を解決するまで生成し続けることができる。
我々は,Rocqのコアメタセトリーを機械化し,Cプログラムのセマンティック制約発生の枠組みを評価し,ヌルポインターの安全性,ディビジョン・バイ・ゼロ自由度,初期化可能な使用法などのパスセンシティブな安全性を強制する。
提案手法は,正規プログラム境界における計算オーバーヘッドを最小限に抑えつつ,よりリッチなセマンティック保証を強制できることを示す。
関連論文リスト
- ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。
ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。
1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
論文 参考訳（メタデータ） (2026-07-01T09:58:59Z) - The Illusion of High Utility in Safety Alignment of Text-to-Image Diffusion Models [49.67749928542536]
テキスト・ツー・イメージ(T2I)拡散モデルの安全性の確保は,有害な世代を抑えることを目的としている。
近年の手法は高いユーティリティで高い安全性を提供するように思われるが、この結論は主に粗いグローバルユーティリティメトリクスに依存している。
構造的評価で実用性を測定すると、この錯覚は壊れる:OnA(質問回答を用いたテキストから画像への忠実度評価)
本研究では,組込み拡散とプロンプト間関係構造を明示的に保存する安全アライメント目標であるStructureAware Geometric Regularization (SAGE)を提案する。
論文 参考訳（メタデータ） (2026-07-01T04:00:27Z) - Weave of Formal Thought [51.56484100374058]
WoFT(Weave of Formal Thought)は、厳密な構文的検証と学習された構造的表現を結合したパラダイムである。
本稿では,非終端文法記号を直接生成にインターリーブするために,言語モデルを訓練する潜時可変微調整法を提案する。
Pythonでは、RWS目的のStarCoder2-3Bを微調整することで、テキストのみのSFTベースラインと比較して、トーケン毎のクロスエントロピーが14.3%削減される。
論文 参考訳（メタデータ） (2026-06-24T15:58:11Z) - Repository-Level Solidity Code Generation with Large Language Models: From Prompting to Fine-Tuning [10.22195567763592]
Solidityスマートコントラクトは、生成されたコードが厳格な言語レベル、セキュリティ、ソフトウェアエンジニアリングの制約を満たす必要がある、高度なドメインを表している。
既存のベンチマークとメトリクスは、リポジトリレベルのSolidity生成には不十分です。
今回紹介するSolidityBenchは,5,470のリポジトリレベルのSolidityスマートコントラクトを,自然言語記述と組み合わせたベンチマークだ。
論文 参考訳（メタデータ） (2026-06-18T09:28:30Z) - CoFi-UCGen: Coarse-to-Fine Unsupervised Conditional Generation without Label Priors [62.68085528259169]
教師なし条件付き画像生成(UCGen)は、手動でアノテートされたラベルに頼ることなく生成を制御することを目的としている。
本研究では,大域的意味論を微粒なバリエーションから明確に切り離す,より粗いUCGenフレームワーク(CoFi-UCGen)を提案する。
我々のCoFi-UCGenは、画像の品質、セマンティック一貫性、制御精度において、既存のUCGenメソッドよりも一貫して優れています。
論文 参考訳（メタデータ） (2026-06-04T03:29:29Z) - Projectional Decoding: Towards Semantic-Aware LLM Generation [7.143305283235514]
大規模言語モデル(LLM)は、多くのソフトウェア工学(SE)タスクでソフトウェアアーチファクトを生成するためにますます使われています。
既存の制約付き復号法は、構文的正しさを強制し、場合によっては特定の意味規則を強制することができる。
本稿では,ドメインのセマンティクスを直接生成プロセスに統合する新しい概念的フレームワークであるプロジェクショナルデコーディングを提案する。
論文 参考訳（メタデータ） (2026-05-28T15:05:53Z) - Provably Secure Agent Guardrail [89.79561918065122]
既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。
本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
論文 参考訳（メタデータ） (2026-05-28T02:12:41Z) - Compile-time Security Analysis and Optimization of Sensitive String Producers [0.0]
本稿では,コンテンツ言語にまたがるセキュアなコンテンツ構成のための汎用フレームワークを提案する。
文字列式構文への追加的な変更を通じて、汎用プログラミング言語に直接統合する。
論文 参考訳（メタデータ） (2026-05-15T19:04:02Z) - Completion by Comprehension: Guiding Code Generation with Multi-Granularity Understanding [37.78627994991325]
CoCoは、大規模なコードリポジトリから複数の粒度コンテキストでコード補完を可能にする新しいフレームワークである。
CrossCodeEvalとRepoEvalベンチマークの実験は、CoCoが最先端のベースラインを一貫して上回っていることを示している。
論文 参考訳（メタデータ） (2025-12-04T07:37:59Z) - Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
Cacoは、高品質で検証可能な多様な命令-CoT推論データの合成を自動化する新しいフレームワークである。
我々の研究は、人間の介入なしに自己持続的で信頼できる推論システムを構築するためのパラダイムを確立します。
論文 参考訳（メタデータ） (2025-10-05T07:59:24Z) - Correctness-Guaranteed Code Generation via Constrained Decoding [11.531496728670746]
本稿では,意味論的に正しいプログラムを生成するための制約付き実行時復号アルゴリズムを提案する。
提案手法は,任意の所定のスクリプティングAPIに従って,意味的に正しいプログラムを生成することができることを示す。
さらに、慎重に設計することで、我々のセマンティック保証が正当性にまで拡張され、ローグライクなビデオゲームにゲームメカニクスを発生させることで検証されることを示す。
論文 参考訳（メタデータ） (2025-08-20T20:48:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。