Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction

TL;DR

Doc2Spec leverages large language models to automatically induce grammar from natural language rules, enabling the generation of formal specifications that improve software correctness and security.

Contribution

The paper introduces a novel multi-agent framework that automates grammar induction from natural language, enhancing formal specification generation without manual grammar crafting.

Findings

Outperforms baseline without grammar induction

Achieves competitive results with manual grammar methods

Effective across multiple programming languages and benchmarks

Abstract

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.