一句话：提出首个可编程框架 ChopChop，通过对程序前缀的可实现性做共归纳分析，对语言模型生成施加语义约束。
语言模型能生成代码但无法保证正确性，常违反类型安全、程序不变式等语义性质。约束解码可将生成限定在满足用户定义性质的程序上，但现有方法仅支持语法约束，或依赖针对 token 序列的脆弱且 ad hoc 的语义性质编码，而非程序结构。本文提出 ChopChop，首个可编程的语义约束解码框架：通过分析某个前缀所代表的程序空间来构造约束解码器，并将该分析形式化为可实现性问题，用余归纳求解，从而把 token 级生成与程序的结构化推理连接起来。作者以其强制与参考程序等价以及类型安全，在多种模型与任务上验证了通用性，结果显示成功率提升且解码延迟保持实用。
Language models (LMs) can generate code but cannot guarantee its correctness—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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{NagyZPD26,
title = {ChopChop: A Programmable Framework for Semantically Constraining the Output of Language Models},
author = {Shaan Nagy and Timothy Zhou and Nadia Polikarpova and Loris D'Antoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776708}
}