← Derniers articles
💻 computer science

Decode-Time Grammars: Constrained LLM Generation over a Refinement Order of Grammar Fragments

Cet article introduit les « grammaires de décodage » (decode-time grammars), une méthode qui instancie dynamiquement des fragments de grammaire à partir d'un environnement d'exécution lors de la génération afin de garantir que les grands modèles de langage produisent du code sémantiquement correct et exempt de références indéfinies à travers diverses surfaces de programmation.

Auteurs originaux : Shuoming Zhang, Ruiyuan Xu, Haofeng Li, Qiuchu Yu, Yangyu Zhang, Chunwei Xia, Xiaobing Feng, Chenxi Wang, Huimin Cui, Jiacheng Zhao

Publié 2026-07-22
📖 1 min de lecture☕ Lecture pause café

Auteurs originaux : Shuoming Zhang, Ruiyuan Xu, Haofeng Li, Qiuchu Yu, Yangyu Zhang, Chunwei Xia, Xiaobing Feng, Chenxi Wang, Huimin Cui, Jiacheng Zhao

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Résumé Technique : Grammaires de Décodage (Decode-Time Grammars)

1. Énoncé du Problème

Les grands modèles de langage (LLM) sont de plus en plus utilisés pour générer du code pour des agents et des systèmes de service où la sortie générée est compilée ou exécutée sans revue humaine. Bien que cela fonctionne pour les langages courants, cela reste fragile pour les surfaces de programmation à faibles ressources telles que les langages spécifiques au domaine (DSL), les API de bibliothèques personnalisées et les outils en ligne de commande.

Un mode de défaillance récurrent dans ces environnements est la référence fantôme (ghost reference) : un jeton syntaxiquement valide (par exemple, un nom de variable, une colonne, une fonction API ou une option CLI) qui n'existe pas dans l'environnement d'exécution actuel Γ\Gamma.

  • Exemples : Référencer un tampon jamais déclaré dans un noyau TileLang, sélectionner une colonne absente d'un schéma SQL, ou appeler une fonction intrinsèque non disponible dans une version spécifique d'une bibliothèque.
  • Cause Racine : Ces erreurs découlent souvent d'un transfert négatif, où le modèle applique des connaissances d'un dialecte voisin, d'une version plus ancienne d'une API ou d'une interface d'outil différente au contexte cible.
  • Limites des Remèdes Existants :
    • Grammaires Fixes : Le décodage contraint par grammaire standard (ex: CFG) assure la validité syntaxique mais traite les positions de référence comme des classes ouvertes (ex: identificateur), acceptant ainsi des noms valides et invalides.
    • Remèdes Côté Modèle : Le prompting, le fine-tuning ou les mécanismes de tentative (retry) peuvent réduire la probabilité d'erreurs, mais ne peuvent pas supprimer les continuations invalides de l'ensemble de support du modèle. Ils reposent sur la capacité du modèle à « préférer » le bon chemin, ce qui est insuffisant lorsque le mauvais chemin est fluide et de haute probabilité.

2. Méthodologie : Grammaires de Décodage

Le papier introduit les grammaires de décodage, un cadre où les fragments de grammaire sont instanciés dynamiquement pendant la génération en fonction d'un environnement d'exécution Γ\Gamma.

Mécanisme Central

  1. Environnement d'Exécution (Γ\Gamma) : Un instantané de l'état actuel, contenant les noms en portée, les types (sorts), les formes, les entrées de schéma, les membres d'API ou l'état de l'outil. Γ\Gamma évolue à mesure que les déclarations sont générées.
  2. Fragments de Grammaire et Ordre de Raffinement : Au lieu d'une grammaire unique et fixe, le système utilise une bibliothèque de fragments de grammaire ordonnés par raffinement (\sqsubseteq).
    • Les fragments varient de grossiers (ex: acceptant n'importe quel identificateur) à étroits (ex: acceptant uniquement les noms déclarés dans Γ\Gamma).
    • Une politique par région π(s,Γ)\pi(s, \Gamma) sélectionne le fragment approprié pour un "trou" spécifique (une position typée dans la génération) basé sur le type attendu ss et l'environnement actuel.
  3. L'Opérateur τΓ\tau_\Gamma (Raffinement) : C'est le mécanisme critique. Il transforme une position de référence ouverte dans un fragment en un emplacement typé par Γ\Gamma.
    • L'ensemble des candidats du placement correspond exactement aux noms disponibles dans Γ\Gamma (ex: Gamma.names(sort=Buffer)).
    • Ces candidats sont compilés en une alternance échappée (ex: "A" | "B" | "C") et injectés dans le reconnaisseur de jetons avant de décoder cette région.
  4. Génération Auto-Extensible : À mesure que le modèle génère des déclarations, celles-ci sont extraites et ajoutées à Γ\Gamma avant que les trous de référence suivants ne soient décodés. Cela garantit que les références sont contraintes par le préfixe déjà généré.

Architecture du Système

L'implémentation, gproj, se compose de deux composants :

  • TemplateInductor (Hors-ligne) : Utilise l'anti-unification sur de petits corpus pour induire des fragments de grammaire et des politiques. Il valide les fragments contre une "barrière stricte" (hard gate) en utilisant des positifs du corpus et des négatifs auto-générés (incluant des références fantômes extraites) pour garantir l'exécutabilité et la correction.
  • Exécuteur gproj (En ligne) : Un exécuteur masqué en ligne qui maintient Γ\Gamma, interroge la politique π\pi, instancie les fragments via τΓ\tau_\Gamma, et compile la grammaire résultante en un masque de jetons pour le décodeur LLM (ex: XGrammar).

3. Contributions Clés et Résultats Formels

Contributions Théoriques

  • Absence de Références Fantômes (No-Ghost Soundness) : Le papier prouve que pour tout fragment où les positions de référence sont réalisées sous forme d'emplacements typés par Γ\Gamma, les chaînes générées sont garanties sans erreur de portée par construction. Chaque référence émise est garantie d'être dans dom(Γ)\text{dom}(\Gamma).
  • Préservation du Raffinement : Il est prouvé que si un fragment plus lâche est sain, tout raffinement plus étroit (via τΓ\tau_\Gamma) préserve cette santé. Cela permet au système de basculer entre des forces de fragments différentes dynamiquement sans réintroduire d'erreurs.
  • Nécessité du Support Dynamique (Proposition 3) : Le papier prouve qu'aucune famille finie de grammaires précompilées avec des supports de référence fixes ne peut être à la fois saine (pas de références fantômes) et non-bloquante (autorisant toutes les continuations valides) pour des espaces d'identificateurs non bornés.
    • Implication : Le support de référence exact doit être synthétisé pendant le décodage basé sur le préfixe. La précompilation statique est théoriquement insuffisante pour les langages cohérents avec les déclarations.

Contributions Pratiques

  • Division du Travail : L'approche sépare la correction liée à l'environnement (gérée par le masque) des décisions de programme ouvertes (gérées par le modèle). Le masque garantit que les références sont valides ; le modèle choisit l'algorithme, la stratégie ou l'intention.
  • Pipeline d'Induction : Une méthode pour générer automatiquement les fragments de grammaire et les politiques requis à partir de petits corpus, rendant l'approche applicable à de nouveaux DSL sans ingénierie de grammaire manuelle.

4. Résultats d'Évaluation

Le système a été évalué sur TileLang (DSL de noyau tensoriel), SQL (jeu de données Spider), P4 (langage de plan de données) et des outils CLI (git, FFmpeg), en utilisant des modèles allant de 0.6B à 236B de paramètres.

  • Élimination des Références Fantômes :
    • Sur toutes les surfaces, le bras typé par Γ\Gamma (utilisant τΓ\tau_\Gamma) a atteint 0 % de références fantômes par construction.
    • En revanche, les bras d'identificateurs ouverts (décodage libre) ont échoué en raison de références fantômes dans 100 % des cas pour TileLang, SQL et P4, quelle que soit la taille du modèle (0.6B à 236B).
    • Exemple : Sur SQL, les identificateurs ouverts ont entraîné 0 % de correspondance d'exécution ; le décodage contraint par Γ\Gamma a atteint 100 %.
  • Indépendance du Modèle : La garantie est transférable entre les tailles de modèles. Même le modèle frontal de 236B (DeepSeek-V4-Flash) a échoué à générer des références valides sans le masque, tandis que le modèle de 0.6B a réussi avec le masque.
  • Comparaison avec les Alternatives :
    • Prompting/Retry : Sur SQL, le prompting avec le schéma et jusqu'à 4 tentatives de réessai a atteint 90 % de correspondance d'exécution, mais a toujours produit 5 colonnes fantômes. Le masque a atteint 100 % de correspondance avec 0 fantôme en un seul passage.
    • Coût : L'approche impose un overhead modéré. Par rapport au décodage non contraint, la réduction du débit de bout en bout est en moyenne de 17,3 %. Par rapport au décodage contraint standard (XGrammar), gproj réduit le débit de 10,6 à 17,8 %.
  • Induction Hors-ligne : Le TemplateInductor a réussi à induire des fragments valides pour des surfaces complexes (ex: opérateurs AscendC, filtres FFmpeg) qui n'avaient pas été écrits à la main, validant le flux de travail "induction + barrière stricte".

5. Signification et Revendications

Le papier affirme que les grammaires de décodage fournissent une tranche de correction précise et stable qui est orthogonale à la capacité du modèle.

  • Garantie Mécanique : Elle transforme la sécurité des références d'un résultat probabiliste (dépendant de la qualité du modèle) en une garantie de construction.
  • Évolutivité : En séparant l'esquisse sémantique (travail du modèle) des références liées à l'environnement (travail du masque), le système permet à des modèles plus faibles de générer du code valide dans des environnements à faibles ressources où ils hallucineraient autrement.
  • Nécessité Théorique : La preuve qu'aucune grammaire statique ne peut être simultanément saine et non-bloquante pour les langages cohérents avec les déclarations établit la nécessité de l'approche de l'instanciation au runtime proposée.

Les auteurs positionnent ce travail non pas comme une solution pour la correction sémantique de l'ensemble du programme (ex: logique algorithmique ou terminaison), mais comme un mécanisme robuste pour éliminer la classe spécifique d'erreurs mécaniquement énumérables (symboles indéfinis) qui affectent la génération de code dans les environnements contraints.

Noyé(e) sous les articles dans votre domaine ?

Recevez des digests quotidiens des articles les plus récents correspondant à vos mots-clés de recherche — avec des résumés techniques, dans votre langue.

Essayer Digest →