metaDecode: Meta Constrained Decoder

Constrained decoding (CSD) algorithms draw structurally valid output strings from an LLM's output distribution with provable correctness: given a formal description of the valid output set, they mask or resample tokens at each decoding step so that the final string always satisfies the constraint. No single constrained decoding strategy works well across all tasks, models, and budgets, and poor choices can reduce accuracy below unconstrained generation. Hand-designing a decoder per task requires substantial expert effort and does not scale. We propose metaDecode, which reduces constrained decoder design to a verified program synthesis problem: given a task, model, and token-step budget, it searches the space of strategies made from composition of formally verified primitives through a greedy hill climb. metaDecode synthesizes reusable task-specific constrained decoders with Dafny-verified correctness proofs, reaching the best score in 6 of 6 held-out symbolic mathematics and text-to-SQL settings and in 7 of 9 molecular generation settings, with gains over the strongest expert-designed decoder of up to 30 percentage points. The same framework can automate the discovery of other LLM inference strategies wherever formal correctness guarantees are needed.