Intent-aligned Formal Specification Synthesis via Traceable Refinement

TL;DR

VeriSpecGen is a traceable refinement framework that synthesizes formal specifications from natural language requirements, enabling targeted repairs and improving synthesis accuracy significantly.

Contribution

It introduces a requirement-level attribution and localized repair approach for synthesizing intent-aligned specifications in Lean from natural language.

Findings

Achieved 86.6% accuracy on VERINA SpecGen task, outperforming baselines by up to 31.8 points.

Generated 343K training examples from refinement trajectories, boosting synthesis performance by 62-106%.

Demonstrated transfer of gains to general reasoning abilities.

Abstract

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.