用可追溯的细化方法自动生成对齐意图的形式化规范。
Intent-aligned Formal Specification Synthesis via Traceable Refinement
- 将自然语言拆解为原子需求，生成带追踪标记的测试用例。
- 在验证失败时定位到具体需求，支持精准修复，准确率达86.6%。
- 适合需要高可靠性代码生成的开发者和形式化验证研究者。
大型语言模型日益用于从自然语言生成代码，但确保正确性仍具挑战。形式化验证通过证明程序满足形式化规范来提供可靠保证。然而，真实代码库中规范常缺失，且编写高质量规范成本高、需专业知识。我们提出VeriSpecGen，一种基于可追溯细化的框架，通过需求级归因与局部修复，在Lean中合成对齐意图的规范。该框架将自然语言分解为原子需求，生成目标特定的测试用例，并建立显式追踪映射以验证生成的规范。当验证失败时，追踪映射可将错误归因至具体需求，实现条款级修复。VeriSpecGen在VERINA SpecGen任务上取得86.6%准确率（使用Claude Opus 4.5），相比基线提升达31.8个百分点，覆盖不同模型家族与规模。此外，我们从精炼轨迹中生成34.3万条训练数据，基于这些数据训练使规范生成性能提升62%-106%，并显著增强通用推理能力。
原文摘要 · Abstract (English)
Large language models are increasingly used to generate code from natural language, but ensuring correctness remains challenging. Formal verification offers a principled way to obtain such guarantees by proving that a program satisfies a formal specification. However, specifications are frequently missing in real-world codebases, and writing high-quality specifications remains expensive and expertise-intensive. We present VeriSpecGen, a traceable refinement framework that synthesizes intent-aligned specifications in Lean through requirement-level attribution and localized repair. VeriSpecGen decomposes natural language into atomic requirements and generates requirement-targeted tests with explicit traceability maps to validate generated specifications. When validation fails, traceability maps attribute failures to specific requirements, enabling targeted clause-level repairs. VeriSpecGen achieve 86.6% on VERINA SpecGen task using Claude Opus 4.5, improving over baselines by up to 31.8 points across different model families and scales. Beyond inference-time gains, we generate 343K training examples from VeriSpecGen refinement trajectories and demonstrate that training on these trajectories substantially improves specification synthesis by 62-106% relative and transfers gains to general reasoning abilities.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。