Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
This addresses the problem of reducing manual effort in formal verification for software correctness, security, and reliability, though it is incremental as it builds on existing LLM and grammar induction techniques.
The paper tackles the challenge of automatically generating formal programming specifications from natural language rules, which is costly to do manually, and presents Doc2Spec, a multi-agent framework using LLMs to induce a specification grammar and generate formal specifications, achieving competitive results on benchmarks across three programming languages.
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.