Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
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_ | 1866918323623559168 |
|---|---|
| author | Xia, Shihao He, Mengting Jia, Haomin Song, Linhai |
| author_facet | Xia, Shihao He, Mengting Jia, Haomin Song, Linhai |
| contents | Ensuring that API implementations and usage comply with natural language programming rules is critical for software correctness, security, and reliability. Formal verification can provide strong guarantees but requires precise specifications, which are difficult and costly to write manually. To address this challenge, we present Doc2Spec, a multi-agent framework that uses LLMs to automatically induce a specification grammar from natural-language rules and then generates formal specifications guided by the induced grammar. The grammar captures essential domain knowledge, constrains the specification space, and enforces consistent representations, thereby improving the reliability and quality of generated specifications. Evaluated on seven benchmarks across three programming languages, Doc2Spec outperforms a baseline without grammar induction and achieves competitive results against a technique with a manually crafted grammar, demonstrating the effectiveness of automated grammar induction for formalizing natural-language rules. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_04892 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction Xia, Shihao He, Mengting Jia, Haomin Song, Linhai Programming Languages Artificial Intelligence Software Engineering Ensuring that API implementations and usage comply with natural language programming rules is critical for software correctness, security, and reliability. Formal verification can provide strong guarantees but requires precise specifications, which are difficult and costly to write manually. To address this challenge, we present Doc2Spec, a multi-agent framework that uses LLMs to automatically induce a specification grammar from natural-language rules and then generates formal specifications guided by the induced grammar. The grammar captures essential domain knowledge, constrains the specification space, and enforces consistent representations, thereby improving the reliability and quality of generated specifications. Evaluated on seven benchmarks across three programming languages, Doc2Spec outperforms a baseline without grammar induction and achieves competitive results against a technique with a manually crafted grammar, demonstrating the effectiveness of automated grammar induction for formalizing natural-language rules. |
| title | Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction |
| topic | Programming Languages Artificial Intelligence Software Engineering |
| url | https://arxiv.org/abs/2602.04892 |