让代码大模型学会在程序中间插入可执行的断言，提升验证和修复代码的能力。
Teaching Code LLMs to Reason with Intermediate Formal Specifications
- 通过验证过的代码和错误变体训练模型，生成能检查中间状态的可执行断言。
- 在竞赛编程数据集上，正确性提升55.8%，完整性提高358.1%，断言有效性提升26.6%。
- 适合关注代码验证、自动修复与大模型推理能力的研究者和开发者。
与自然语言规范不同，可执行的正式规范提供了机器可验证的约束，可用于代码验证、调试与修复。然而，编写此类规范耗时费力，现有基于LLM的方法主要推断全程序的前置/后置条件，忽略了程序员在算法推理中依赖的中间语义承诺。我们的研究发现，当前提示代码大模型常生成语法错误、平凡或过于弱化的可执行断言。本文提出可执行检查点规范生成，即在程序有意义的内部节点插入断言以描述预期中间状态。我们引入SpecCoder，一个基于验证参考程序、行为改变的变异体及多轮规范精炼轨迹的验证引导式代码大模型训练框架。SpecCoder选择在正确执行中成立但拒绝错误执行的规范，使规范从被动注释变为可执行证据。为评估该设置，我们构建了HumanExec基准，基于近期Codeforces竞赛题目，包含测试套件、参考解法与人工引入的错误提交，支持三个任务：规范生成、程序正确性检查与程序修复。在HumanExec上的实验表明，SpecCoder显著优于基础代码大模型。在Qwen2.5-Coder系列模型上，SpecCoder将内联规范正确性提升至55.8%，完整性提升358.1%，可执行断言有效性提升26.6%。这些改进进一步转化为下游正确性推理与修复性能，证明可执行检查点提供了细粒度可靠的验证依据。
原文摘要 · Abstract (English)
Unlike natural-language specifications, executable formal specifications provide machine-checkable constraints for verifying, debugging, and repairing code. However, writing such specifications is labor-intensive, and existing LLM-based methods mainly infer whole-program pre/postconditions, missing the intermediate semantic commitments that programmers rely on when reasoning about an algorithm. Our study further shows that prompting current CodeLLMs often produces executable assertions that are syntactically invalid, trivial, or too weak to reject behavior-changing faults. In this paper, we study executable checkpoint specification generation, where assertions are inserted at meaningful internal program points to describe expected intermediate states. We introduce SpecCoder, a verification-guided CodeLLM training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces. SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence. To evaluate this setting, we introduce HumanExec, a benchmark built from recent Codeforces competitive programming problems with test suites, reference solutions, and human buggy submissions, supporting three tasks: specification generation, program correctness checking, and program repair. Experiments on HumanExec show that SpecCoder substantially improves checkpoint-specification quality over base CodeLLMs. Across Qwen2.5-Coder models, SpecCoder improves inline-specification correctness by up to 55.8%, completeness by up to 358.1%, and executable assertion validity by up to 26.6%. These gains further translate to downstream correctness reasoning and repair, showing that executable checkpoints provide fine-grained evidence for reliable verification.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。