Conditional Deontics Over Terminals: A Cross-subtree Reference Mechanism for Efficient yet Expressive Constrained Decoding

As recent work has improved expressiveness in constrained decoding, a common component has begun to emerge: user-defined functions that read and modify a constrainer's internal state. However, permissive access to a constrainer's internal state makes efficiency optimization difficult. In this work we offer a sharpened contract for such user-defined functions, decomposing them into simpler functions that require minimal access to the constrainer's internal state, which we call deontic functions, and providing mechanisms for aggregating and anchoring deontic functions within grammar structures. Using our formalism, we implement the unit-propagation algorithm within a chain of thought, enabling a smaller model to achieve a high solve rate and reduced token consumption on a SAT-style logic puzzle called “Knights and Knaves”. Utilizing a GPU-based backend for our formalism, we replicate constrainers such as type checking and e-graph enforcement found in prior works and achieve substantial efficiency gain.