# 面向软件工程的受约束代码生成

规范 HTML：https://aogavrilov.com/zh/research-notes/constrained-code-generation-software-engineering/
英文版本：https://aogavrilov.com/research-notes/constrained-code-generation-software-engineering/
文档语言：zh-Hans
来源论文：https://aogavrilov.com/zh/publications/inspectable-control/
英文论文全文：https://aogavrilov.com/publications/inspectable-control/full-text/
DOI：https://doi.org/10.1145/3803437.3807386

区分语法约束、类型约束、保持边界和行为级验收检查，明确每种机制真正能够保证什么，避免把可解析输出误当成功能正确。

## 直接回答

### 受约束代码生成在软件工程流程中能够保证什么？

它只能保证被显式执行的属性。语法约束解码可以保证输出属于某个语法；类型感知方法可以以类型有效性为目标；但两者都不能单独证明任务正确、语义等价、行为保持或编辑局部性。

## 为什么这一区分重要

如果没有说明受约束的具体属性，“受约束”这个词是不完整的。解码器可以执行语法约束，类型检查器可以限制有效续写，编辑器可以保护指定区域，修复流程则可以只接受通过测试的候选。这些机制解决的是不同问题。

因此，有效评估必须让控制机制与所声称的保证一致。通过解析器是语法方面的证据，但不是程序满足请求或在编辑区外保持行为的证据。

## 实用步骤

1. **命名所需属性。** 明确要求涉及语法、类型、API、源代码局部性、结构不变量、测试行为，还是其他可观察契约。
2. **选择约束执行位置。** 在可能时于解码期间施加约束；如果属性只能在生成后检查，则采用“提出候选—验证候选”的流程。
3. **保留独立验收检查。** 即使解码器已经保证语法或类型，也必须另行检查任务成功和受保护属性。
4. **报告拒绝与失败行为。** 说明候选被拒绝的频率、有效解是否仍然可达，以及哪些属性仍未被检查。

## 应要求哪些证据

- 用可观察的术语声明被约束的属性。
- 区分约束执行机制与生成后的验收检查。
- 不把语法或类型有效性描述成功能正确性。
- 如果声称未变代码得到保持，则直接测量局部性。
- 报告约束失败、拒绝率和任务成功率。

## 相关研究实际报告了什么

- 相关分层潜在研究锁定选定的学习式码，并测量解码后的解析率、编辑自由度和多样性。
- 这是一个可检查的部分控制实验，不是形式语法、类型、语义或行为保证。
- 它对受约束流程的价值在于显式控制界面和测量纪律，而不是声称潜在码锁定可以替代形式验证。

## 适用边界

- 不同约束可能相互冲突；更强的限制可能排除有效解或降低生成多样性。
- 生成后测试只能为其覆盖到的行为提供证据。
- 相关论文没有评估形式约束解码或仓库级软件修复。

完整研究指南：https://aogavrilov.com/zh/projects/discrete-latent-generation/#comparison

## 主要与邻近来源

- [Inspectable Control for Structure-Preserving Software Regeneration](https://aogavrilov.com/publications/inspectable-control/)：关于分层潜在空间中可检查部分控制的主要站内论文。
- [Constrained Decoding of Diffusion LLMs with Context-Free Grammars](https://arxiv.org/abs/2508.10111)：在扩散语言模型解码期间执行形式语法约束。
- [Type-Constrained Code Generation with Language Models](https://doi.org/10.1145/3729274)：面向语言模型代码生成的类型感知约束。

这篇维护型笔记只总结已有证据，不添加超出引用来源的新实验结果。