神经程序综合：从规约到代码的开放问题

破除误解：会生成代码不等于会综合程序#

综合的古典含义是：给定规约，搜索满足规约的程序。SKETCH 把洞交给 SAT/SMT；FlashFill 从例子学字符串变换。LLM 生成的是高概率 token 序列。它可以碰巧满足测试，也可以生成看起来对、对隐藏输入失败的函数。把助手的成功率写成「程序综合已解决」，漏掉了规约这一头。

第二个误解是用竞赛题当通用能力。竞赛题有明确的输入输出与时间限制，接近综合问题的理想形态。公司代码库里的规约是 issue、注释、邻接模块的隐含不变式。AlphaCode 的数字不能平移成「能维护十年的遗留系统」。

第三个误解是验证可以事后全部补上。对生成代码跑测试能抓住一部分错误；测试通过不等于规约被满足。形式化那一条线仍然必要，而且更难接到自然语言上：你必须先得到可检查的规约。神经综合没有取消证明，它把「规约从哪来」变成了新的瓶颈。

2020s 的现场：搜索、样例与评价漏洞#

AlphaCode（Li 等，Science 2022）把大规模采样与过滤接到竞赛题上：生成许多候选，用公开测试筛，再聚类提交。关键机制是用搜索补模型的不可靠，不是单次采样就对。这与古典综合的「在程序空间里搜」同构，只是提议分布换成了网络。

代码助手把同一机制缩成交互：人提供规约的碎片，模型提供提议，人再当过滤器。责任在界面上模糊。经验软件工程在 2020 年代测量的是：助手是否加快任务、是否引入特定类别的漏洞、是否改变审查负担。结果依赖任务与测量方法，不支持单一广告句。

评价漏洞是开放问题的核心。训练数据含有竞赛题与 GitHub 上的解，基准泄漏会让数字虚高。隐藏测试、新题、执行沙箱，成为论文的必要章节。没有执行的「代码 BLEU」几乎不能当综合指标。

开放问题：规约、工具链、责任#

规约从自然语言抽出可测试的性质，本身是未解决问题。类型能挡住一类错误，挡不住错误的业务含义。测试生成（包括用模型生成测试）会与被测模型共享盲区。把生成器与检查器训练成同一家族，检查会共谋失败。

工具链方面，检索代码库、调用编译器、在循环里修编译错误，把综合做成智能体。开放的是：循环何时停、工具输出如何可信、以及是否在放大供应链风险（生成含糊依赖、复制不安全模式）。本页不讨论利用细节；只登记：生成代码进入构建图，就进入供应链。

与 Lean/CompCert 的汇合是研究前沿而不是产品现状：让模型写出带证明的程序，或写出要交给求解器的 SKETCH。成功案例仍窄。失败模式是流畅的错误证明或不可检的空洞。2020 年代的诚实状态是：神经提议 + 符号过滤，比单独任何一边都更像能工作的系统；端到端可靠综合仍未发生。

评价还必须处理版权与许可。训练语料含有受许可约束的代码，生成物可能复述。研究层要测量近似复制，工程层要决定生成代码的来源声明。这不是本页的法律意见，它是综合系统多出来的一条证据链：你不仅要说程序满足测试，还要说它不是某份训练样本的略改。开放问题包括：如何在不公开训练数据的情况下审计复制，以及测试通过是否被错误当成原创性证明。

人机循环里的停机条件同样未解决。助手可以无限修补编译错误，每次修补都可能引入新的语义漂移。古典综合有目标函数或规约作为停机；聊天没有。生产系统用超时、测试集与人工确认来停，其中人工确认又把「综合」变回「建议」。2020 年代真正进入仓库的，大多是这第三种。

古典综合给出对照。SKETCH 把程序写成带洞的模板，洞的域交给 SAT 或 SMT；反例引导归纳（CEGIS）用失败输入加约束，直到求解器找不到反例或放弃。规约是可执行的：输入输出例子、断言、或部分正确性条件。搜索空间爆炸时，综合失败是可见的——求解器超时，而不是生成一段流畅但未定义的函数。神经方法把提议分布换成网络，过滤仍可接到同一类检查上。开放问题是：检查器比生成器弱时，系统会收敛到「能通过当前测试的高概率文本」，而不是「满足未知规约的程序」。

仓库级综合把问题再放大一档。函数级基准假设签名与单文件上下文已知；真实修改要读邻接模块、构建脚本、隐藏不变式与代码所有权。检索能把局部片段送进窗口，不能把十年的架构判断送进窗口。智能体循环调用编译器与测试，是在用工具输出当廉价规约。工具输出可信，当且仅当构建是可重复的、测试不是被生成器写出来的共谋套件。供应链风险在这里会合：生成的依赖声明、复制的不安全模式、以及「测试绿了所以可以合并」的审查短路，都是同一类证据不足。本页不讨论具体漏洞写法；只登记机制：生成物一旦进入构建图，就继承构建图的审计义务。

评价污染是另一条必须单独记账的机制。HumanEval 一类基准的题面在训练语料里出现过，数字会把记忆写成能力。新题、隐藏测试、执行沙箱因此不是论文装饰，而是综合主张的可证伪条件。没有执行的 n-gram 重叠几乎不能当指标：它奖励表面像代码的文本。AlphaCode 用大规模采样加公开测试过滤，等于承认单次解码不可靠；过滤集合一旦泄漏，成绩同样虚高。2020 年代诚实的前沿表述是：神经提议已经进入生产，作为「建议」；作为「给定规约则返回满足程序」的综合，规约一端仍空着。

与类型系统、编译器的接口决定提议能被自动挡掉多少。类型能拒绝一整类形状错误，挡不住错误的业务含义；编译器能拒绝语法与一部分未定义行为，挡不住静默的错算法。把这两层过滤器写进产品，会让成功率上升，也会让用户误以为剩下的错误更少、更浅。实际分布往往相反：留下来的错误更像合法程序。审查负担因此从「看懂语法」转到「看懂是否是对的程序」。经验软件工程若只报告速度，不报告这一类残留错误的密度，会把过滤器的选择效应写成能力跃迁。

FlashFill 一类从例子学变换的系统说明：当规约是短的输入输出对、域又窄（字符串、表格），综合可以产品化。竞赛编程把域换成算法题，规约变成公开测试。仓库维护把域换成隐式社会合同。三种域不能共用一个成功率。把助手在注释补全上的命中率写成「程序综合已解决」，是把最窄的域当成了最宽的域。开放问题应按域分开立案：例子综合、竞赛综合、仓库综合、带证明综合。2020 年代进入生产的，几乎都停在前两档与第三档的建议层。

跨域连接#

• 证明：测试是弱证明，类型是中等证明，形式化是强证明。神经综合把提议从人换成模型，没有把证明义务从世界上撤走。开放问题是如何让模型输出可检查的对象（断言、不变量、Lean 草稿），而不是只输出看起来像代码的文本。证明助手那一篇给出强端；本篇给出弱端为何在生产里占上风：规约太贵。
• 信息不对称：开发者看见自然语言需求，模型看见训练数据里的类似题。两边都不看见对方的全部。助手界面若把生成代码打扮成「已理解需求」，就是在用流畅度掩盖不对称。代码审查重新变成披露机制：人必须证明自己看过。
• 范畴论：规约与实现之间应当有一种满足关系，像对象之间的箭头可组合。测试集只检查箭头在有限个点上的表现。综合系统若不能说出满足关系的种类（类型、契约、定理），就无法把生成步骤合成更大的正确程序。这不是要用范畴语写助手，而是说明「拼起来仍正确」需要代数结构，概率采样不提供这个结构。
• 国家能力：关键软件的采购若接受「模型生成、测试过了」作为合格证明，等于降低了可审计标准。能力体现在能否要求可重复构建、来源与规约痕迹。生成式工具可以加快文书，也可以让责任在厂商、模型与操作员之间蒸发。政策争论应落在证据标准，而不是落在禁不禁助手。

参考文献#

• Solar-Lezama, A. "Program Synthesis by Sketching." PhD thesis, UC Berkeley, 2008; 及后续 SKETCH 系统论文。
• Gulwani, S. "Automating String Processing in Spreadsheets Using Input-Output Examples." POPL, 2011. （FlashFill）
• Li, Y. et al. "Competition-Level Code Generation with AlphaCode." Science 378(6624):1092–1097, 2022.
• Chen, M. et al. "Evaluating Large Language Models Trained on Code." arXiv:2107.03374, 2021. （Codex / HumanEval，注意评价局限）
• Pearn, D. 等关于基准泄漏与数据污染的后续测量工作（2023–2025 软件工程会议，读时核对是否新题）。

延伸阅读#

• Gulwani, S., Polozov, O. & Singh, R. Program Synthesis. Foundations and Trends in Programming Languages, 2017. （古典综合地图）
• 本站 形式化验证与程序合成：Lean、CompCert 与证明对象；与本篇的神经提议路径对照着读。