Intent-aligned Formal Specification Synthesis via Traceable Refinement
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917401209077760 |
|---|---|
| author | Ye, Zhe Yang, Aidan Z. H. Su, Huangyuan Liao, Zhenyu Tenka, Samuel Qin, Zhizhen Ghai, Udaya Song, Dawn Kong, Soonho |
| author_facet | Ye, Zhe Yang, Aidan Z. H. Su, Huangyuan Liao, Zhenyu Tenka, Samuel Qin, Zhizhen Ghai, Udaya Song, Dawn Kong, Soonho |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_10392 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Intent-aligned Formal Specification Synthesis via Traceable Refinement Ye, Zhe Yang, Aidan Z. H. Su, Huangyuan Liao, Zhenyu Tenka, Samuel Qin, Zhizhen Ghai, Udaya Song, Dawn Kong, Soonho Machine Learning Artificial Intelligence Logic in Computer Science Programming Languages Software Engineering 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. |
| title | Intent-aligned Formal Specification Synthesis via Traceable Refinement |
| topic | Machine Learning Artificial Intelligence Logic in Computer Science Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2604.10392 |