ABS: Enforcing Constraint Satisfaction On Generated Sequences Via Automata-Guided Beam Search

TL;DR

ABS tackles the challenge of enforcing formal constraints in autoregressive sequence generation by embedding a compiled DFA into a model-agnostic, inference-time beam search. The Ramp Push-Up mechanism adaptively biases decoding toward accepting DFA states, ensuring constraint satisfaction without retraining while preserving naturalness. The authors prove soundness and demonstrate that ABS achieves perfect constraint compliance across constrained image sequence classification, constrained text generation, and text infilling, while matching or surpassing baselines on standard quality metrics and improving efficiency. This approach broadens the applicability of constrained generation to any regular language (including LTL_f and regex) and offers practical benefits for high-stakes and safety-critical deployments.

Abstract

Sequence generation and prediction form a cornerstone of modern machine learning, with applications spanning natural language processing, program synthesis, and time-series forecasting. These tasks are typically modeled in an autoregressive fashion, where each token is generated conditional on the preceding ones, and beam search is commonly used to balance exploration and fluency during decoding. While deep learning models and Large Language Models (LLMs) excel at capturing statistical patterns in this setting, they remain ill-equipped to guarantee compliance with formal constraints. In this paper, we introduce ABS: a general and model-agnostic inference-time algorithm that guarantees compliance with any constraint that can be compiled into a Deterministic Finite Automaton (DFA), without requiring retraining. ABS leverages the DFA to guide a constrained variant of beam search: at each decoding step, transitions leading to violations are masked, while remaining paths are dynamically re-ranked according to both the model's probabilities and the automaton's acceptance structure. We formally prove that the resulting sequences are guaranteed to satisfy the given constraints, and we empirically demonstrate that ABS also improves output quality. We validate our approach on three distinct tasks: constrained image-stream classification, controlled text generation, and text infilling. In all settings, ABS achieves perfect constraint satisfaction, while outperforming or matching state-of-the-art baselines on standard quality metrics and efficiency.

Figures (3)

• Figure 1: DFA (left) and corresponding state transition table with the distances to the closest accepting states (right) for the constraint: " Generate a sentence that contains coffee, cat, and toy in that order" (note how this constraint can be easily expressed as a regex or $\text{LTL}_f$ formula). The deadlock state is $q_1$, the accepting state is $q_5$ while the initial state is $q_0$.
• Figure 2: (Cont.'ed from Figure \ref{['fig:dfa_and_table']}). Real generation using ABS, with 2 beams, $\alpha_{\min}$=0.25, $\gamma$=1, and T=9. The selected sequence is shaded in green. Above each token are the relative logits, before and after modification, while the arcs represent the state transitions inside the automaton. The same model without ABS generates " The cat was playing with a toy while the", breaking the order constraints on word generation (cat before coffee). After generating "The", the model prefers "cat" at $t=2$, violating the requirements.
• Figure 3: Performance on Ordered Fashion MNIST.

Theorems & Definitions (5)

• Definition 1
• Theorem 1: Soundness of Automata-guided Beam Search with Ramping $\alpha$
• Theorem 2: Complexity of Markov Chains MAP Inference with Unary Constraint
• proof : Proof of Theorem \ref{['theorem:soundness']}. (Soundness of the ABS algorithm)
• proof : Proof of Theorem \ref{['theorem:MCMAP']}