cs.LGApr 12, 2026
SaveIntent-aligned Formal Specification Synthesis via Traceable Refinement
Organizations: UC Berkeley · Amazon Web Services · Harvard University
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.
Figures & tables
Figure 1: VeriSpecGen traceable refinement workflow. Given a natural language problem description (e.g., “Find the most frequent element…”), VeriSpecGen synthesizes formal specifications through three stages: (1) Atomic Requirement Decomposition : An LLM decomposes the description into testable atomic requirements (AR1: non-empty input, AR2: frequency constraint, AR3: tie-breaking rule). (2) Requirement-targeted Test Generation : For each requirement, the system generates positive tests (valid input-output pairs), negative-output tests (invalid outputs for valid inputs), and negative-input tests (invalid inputs), creating an explicit traceability map linking each test to its validating requirements. (3) Specification Synthesis & Traceable Refinement : An LLM generates an initial Lean specification from the atomic requirements. A Lean prover validates the specification against all tests. When validation fails (e.g., test incorrectly accepted), the traceability map attributes the failure to specific requirements (AR3 via ), enabling localized repair that modifies only the affected postcondition clause rather than rewriting the entire specification. This process iterates until all tests pass, producing intent-aligned specifications.
| Dataset | #Instances |
|---|---|
| Source and Processing | |
| TACO-verified (decontaminated) | 12,901 |
| Translated to Lean with test suites | 11,981 |
| Successfully synthesized specifications | 6,842 |
| Distilled Training Examples | |
| SFT Full | 343,827 |
Table 1: Dataset statistics from trajectory distillation. Starting from 12,901 TACO-verified problems (decontaminated with zero 10-gram overlap with Verina ), we successfully translate 11,981 to Lean and synthesize 6,842 specifications, from which we distill three SFT dataset variants.
| Model | Baseline | VeriSpecGen | Abs. (Rel.) |
| Closed-Source Models | |||
| Claude Opus 4.5 | 59.0 | 86.6 | 27.6 (+46.8%) |
| Claude Sonnet 4.5 | 50.7 | 72.0 | 21.3 (+42.0%) |
| Open-Weight Models | |||
| Qwen3-Coder-480B-A35B | 36.7 | 68.5 | 31.8 (+86.7%) |
| Qwen3-Coder-30B-A3B | 29.3 | 50.3 | 21.0 (+71.7%) |
Table 2: Specification synthesis results on Verina . VeriSpecGen consistently outperforms Verina baseline across all models, achieving 42–87% relative improvement.
| Claude Opus 4.5 | Qwen3-Coder-30B-A3B | |||
| Variant | Score | Abs. (Rel.) | Score | Abs. (Rel.) |
| Direct generation | 59.0 | – | 29.3 | – |
| Direct refinement | 72.2 | 13.2 (+22.4%) | 27.0 | 2.3 (-7.8%) |
| Test-driven refinement | 73.8 | 14.8 (+25.1%) | 20.9 | 8.4 (-28.7%) |
| w/o adversarial testing | 81.0 | 22.0 (+37.3%) | 48.9 | 19.6 (+66.9%) |
| VeriSpecGen | 86.6 | 27.6 (+46.8%) | 50.3 | 21.0 (+71.7%) |
Table 3: Ablation study on Verina . All variants improve over direct generation on Opus 4.5, and removing the decomposer causes the largest performance drop, showing that decomposition is critical for effective specification synthesis.
| Qwen3-4B-Instruct-2507 | Qwen3-Coder-30B-A3B | ||||||||
| CodeGen | SpecGen | CodeGen | SpecGen | ||||||
| Training Variants | Pass@1 | Pass@10 | Pass@1 | Pass@10 | Pass@1 | Pass@10 | Pass@1 | Pass@10 | |
| Base Model | 25.3 | 28.3 | 14.7 | 16.3 | 39.7 | 53.5 | 29.4 | 41.7 | |
| SFT Spec-Only | 18.0 | 26.7 | 9.5 | 16.6 | 41.5 | 68.4 | 30.4 | 50.0 | |
| Abs. (Rel.) | 7.3 (-28.9%) | 1.6 (-5.7%) | 5.2 (-35.4%) | 0.3 (+1.8%) | 1.8 (+4.5%) | 14.9 (+27.9%) | 1.0 (+3.4%) | 8.3 (+19.9%) | |
| SFT Full | 43.5 | 72.7 | 22.8 | 38.8 | 61.2 | 79.7 | 43.5 | 58.0 | |
Table 4: Evaluation of trajectory-distilled training variants on Verina . Training on specification synthesis trajectories improves both CodeGen and SpecGen tasks. SFT No-Test achieves the best specification performance (+15.6–18.2 SpecGen@1), while SFT Full yields the strongest code generation transfer (+18.2–21.5 CodeGen@1). shows both absolute and relative improvements over the base model.
| Math Reasoning | Coding | Verina | |||||
| Model variant | GSM8K | AIME24 | AIME25 | HumanEval | MBPP | CodeGen | SpecGen |
| Base Model | 66.3 | 60.0 | 46.7 | 63.7 | 75.2 | 25.3 | 14.7 |
| Merged ( ) | 68.3 | 63.3 | 50.0 | 76.1 | 78.2 | 22.9 | 15.6 |
| Abs. (Rel.) | 2.0 (+3.0%) | 3.3 (+5.5%) | 3.3 (+7.1%) | 12.4 (+19.5%) | 3.0 (+4.0%) | 2.4 (-9.5%) | 0.9 (+6.1%) |
| SFT No-Test | 80.7 | 40.0 | 23.3 | 70.1 | 70.2 | 35.4 | 30.3 |
| Abs. (Rel.) | 14.4 (+21.7%) | 20.0 (-33.3%) | 23.4 (-50.1%) | 6.4 (+10.0%) | 5.0 (-6.6%) | 10.1 (+39.9%) | 15.6 (+106.1%) |
Table 5: Transfer to out-of-domain benchmarks for Qwen3-4B-Instruct-2507 . Linear merging ( ) successfully transfers specification-synthesis capabilities to math reasoning and general code generation tasks.
Appendix figures & tables7 assets
Supplementary material from the paper’s appendix.
Appendix
| Task | Count | % | Description |
| Core Specification Tasks | |||
| ar_decomposition | 6,927 | 2.0 | Decompose description into atomic requirements |
| direct_specgen | 6,842 | 2.0 | End-to-end specification generation |
| spec_refinement | 55,270 | 16.1 | Repair failed specifications with localized feedback |
| feedback_generation | 42,330 | 12.3 | Generate requirement-attributed failure analysis |
| signature_generation | 10,162 | 3.0 | Generate Lean function signatures |
Table 6: Task distribution in the full SFT dataset. Test-related tasks comprise 64.6% of the dataset, while core specification tasks account for 35.4%.
| Variant | Examples | Description |
|---|---|---|
| SFT Full | 343,827 | All 11 tasks, complete refinement pipeline |
| SFT No-Test | 121,531 | 5 core specification tasks only |
| SFT Spec-Only | 6,842 | End-to-end NL-to-specification pairs only |
Table 7: Training dataset variants. All variants are derived from the same high-quality checkpoints but differ in which tasks are included.
| Task | Full | No-Test | Spec-Only |
|---|---|---|---|
| direct_specgen | 2.0% | 5.6% | 100% |
| ar_decomposition | 2.0% | 5.7% | — |
| signature_generation | 3.0% | 8.4% | — |
| spec_refinement | 16.1% | 45.5% | — |
| feedback_generation | 12.3% | 34.8% | — |
| positive_test_gen | 2.3% | — | — |
Table 8: Task inclusion and percentage composition across training variants. Percentages show the proportion of each task within its variant. SFT No-Test concentrates supervision on refinement tasks (80.3%), while SFT Spec-Only provides only end-to-end targets.
Figure 2: Temperature vs. Spec Pass@1 for different SFT configurations. Lower temperatures consistently yield better performance across all configurations. SFT Spec-Only drops below the base model at higher temperatures for the 30B model, demonstrating that single-task training provides insufficient learning signal and multi-task supervision from trajectory distillation is essential for robust specification synthesis.
Figure 3: Code Pass@1 vs. Spec Pass@1 at . Each point represents a training epoch (e1–e5). SFT No-Test achieves the best specification performance while maintaining competitive code generation capability. SFT Spec-Only clusters in the lower-left quadrant, exhibiting degraded performance on both tasks despite being trained specifically for specification generation.
Figure 4: Spec Pass@1 (%) across epochs and temperatures for SFT No-Test. Performance improves consistently with additional training epochs, with diminishing returns after epoch 3–4. At , the best configuration achieves 30.3% for the 4B model and 47.6% for the 30B model, representing 15.6 and 18.2 points absolute improvement over the respective base models (14.7% and 29.4%).
| Math Reasoning | Coding | Verina | |||||
| Model variant | GSM8K | AIME24 | AIME25 | HumanEval | MBPP | CodeGen | SpecGen |
| Base Model | 66.3 | 60.0 | 46.7 | 63.7 | 75.2 | 25.3 | 14.7 |
| Merged ( ) | 67.6 | 56.7 | 53.3 | 74.2 | 76.1 | 21.4 | 15.5 |
| Abs. (Rel.) | 1.3 (+2.0%) | 3.3 (-5.5%) | 6.6 (+14.1%) | 10.5 (+16.5%) | 0.9 (+1.2%) | 3.9 (-15.4%) | 0.8 (+5.4%) |
| Merged ( ) | 68.3 | 63.3 | 50.0 | 76.1 | 78.2 | 22.9 | 15.6 |
| Abs. (Rel.) | 2.0 (+3.0%) | 3.3 (+5.5%) | 3.3 (+7.1%) | 12.4 (+19.5%) | 3.0 (+4.0%) | 2.4 (-9.5%) | 0.9 (+6.1%) |
Table 9: Transfer to out-of-domain benchmarks for Qwen3-4B-Instruct-2507 . Linear merging with varying values transfers specification-synthesis capabilities to math reasoning and general code generation tasks. achieves the best balance across out-of-domain benchmarks.