The widespread adoption of language models for code generation makes the enforcement of formal guarantees on their outputs ever more important. Recent constrained decoding techniques are promising, but when applied to practical programming languages they typically face a trade-off between soundness and completeness, either permitting some invalid programs or rejecting some valid ones. We argue that invalid programs should be excluded entirely, yet find that overly restrictive acceptance criteria can significantly impair a model’s ability to follow human intent and generate functionally correct code. We attribute this degradation to a mismatch between the model’s internal representation of the language and the constrained language induced by the formal guarantees. To better align the two, we propose reducing variability through training-set preprocessing, language design, or neural architecture design.

I am a PhD student in the Programming Group at the University of St. Gallen. I am primarily working on optimizations for theorem provers. I am also interested in formal methods for AI.