教学代码 LLM 使用中级形式规范进行推理

与自然语言规范不同，可执行形式规范为验证、调试和修复代码提供了机器可检查的约束。然而，编写此类规范是劳动密集型的，并且现有的基于 LLM 的方法主要推断整个程序的前置/后置条件，缺少程序员在推理算法时所依赖的中间语义承诺。我们的研究进一步表明，提示当前的 CodeLLM 通常会产生语法上无效、微不足道或太弱而无法拒绝行为改变错误的可执行断言。在本文中，我们研究可执行检查点规范的生成，其中在有意义的内部程序点插入断言以描述预期的中间状态。我们引入了 SpecCoder，这是一种验证引导的 CodeLLM 训练框架，可以从经过验证的参考程序、行为改变突变体和多轮规范细化跟踪中学习。 SpecCoder 选择保持正确执行的规范，同时拒绝错误执行，将规范从被动注释转变为可执行证据。为了评估此设置，我们引入了 HumanExec，这是一个根据最近的 Codeforces 竞争性编程问题（包括测试套件、参考解决方案和人为错误提交）构建的基准，支持三项任务：规范生成、程序正确性检查和程序修复。 HumanExec 上的实验表明，SpecCoder 比基本 CodeLLM 显着提高了检查点规范质量。在 Qwen2.5-Coder 模型中，SpecCoder 将内联规范正确性提高了 55.8%，完整性提高了 358.1%，可执行断言有效性提高了 26.6%。这些成果进一步转化为下游正确性推理和修复，表明可执行检查点为可靠验证提供了细粒度的证据。