约束代码生成中的对齐问题

大语言模型 (LLM) 在代码生成方面表现出了强大的能力，但其输出经常包含导致编译失败的语法或类型错误。约束解码已被提出作为一种解决方案，通过构造来减少编译错误，并作为副产品提高功能正确性。然而，以前的工作忽略了约束解码的一个关键方面：约束器（例如类型）、语言模型和目标规范语言（例如 TypeScript）之间的对齐。未对准是由于约束器不完整（拒绝属于目标的程序）或不健全（允许不属于目标的程序）引起的。不完整性造成的偏差会扭曲语言模型的分布，并且可能不利于代码生成。我们使用七种语言模型、两种目标语言、两种约束条件、解码过程中的强制类型和语法来评估这一假设，并研究语言模型如何对不同程度的不完整性做出反应。在三个基准测试中，当约束器不完整时，无约束解码在功能正确性方面显着优于约束解码。不完整性将模型推入程序空间的低概率区域，导致生成频繁超时，并使功能正确性降低高达 97%。这些贡献使社区意识到约束解码中未对准的负面影响，并提供了关于如何设计有利于具有形式保证的代码生成系统的约束器的定量见解。