通过可追踪的细化进行与意图一致的形式规范合成

大语言模型 越来越多地用于从自然语言生成代码，但确保正确性仍然具有挑战性。形式验证提供了一种通过证明程序满足形式规范来获得此类保证的原则性方法。然而，现实世界的代码库中经常缺少规范，并且编写高质量的规范仍然昂贵且需要大量专业知识。我们推出了 VeriSpecGen，这是一个可追踪的细化框架，它通过需求级归因和本地化修复来综合精益中符合意图的规范。 VeriSpecGen 将自然语言分解为原子需求，并生成具有显式可追溯性映射的针对需求的测试，以验证生成的规范。当验证失败时，可追溯性将属性失败映射到特定要求，从而实现有针对性的子句级修复。 VeriSpecGen 使用 Claude Opus 4.5 在 VERINA SpecGen 任务上取得了 86.6% 的成绩，在不同模型系列和规模上比基线提高了高达 31.8 个百分点。除了推理时间增益之外，我们还从 VeriSpecGen 细化轨迹中生成了 343K 个训练示例，并证明对这些轨迹进行训练可显着提高规范合成相对值 62-106%，并将增益转移到一般推理能力。