# ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models

## TL;DR

ChopChop is a novel programmable framework that constrains language model outputs to satisfy semantic properties like type safety and program equivalence, improving correctness without sacrificing efficiency.

## Contribution

It introduces a principled, structure-aware decoding method based on program analysis and coinduction, enabling semantic constraints beyond syntactic restrictions.

## Key findings

- Improves success rates in constrained program generation
- Maintains practical decoding latency
- Enforces semantic properties like type safety and equivalence

## Abstract

Language models (LMs) can generate code but cannot guarantee its correctness$\unicode{x2014}$often producing outputs that violate type safety, program invariants, or other semantic properties. Constrained decoding offers a solution by restricting generation to only produce programs that satisfy user-defined properties. However, existing methods are either limited to syntactic constraints or rely on brittle, ad hoc encodings of semantic properties over token sequences rather than program structure. We present ChopChop, the first programmable framework for constraining the output of LMs with respect to semantic properties. ChopChop introduces a principled way to construct constrained decoders based on analyzing the space of programs a prefix represents. It formulates this analysis as a realizability problem which is solved via coinduction, connecting token-level generation with structural reasoning over programs. We demonstrate ChopChop's generality by using it to enforce (1) equivalence to a reference program and (2) type safety. Across a range of models and tasks, ChopChop improves success rates while maintaining practical decoding latency.