aiqbench analysis
Doc2Spec advances AI-assisted software engineering by using multi-agent systems and grammar induction to automatically generate formal specifications from natural language API rules. This approach significantly improves precision and recall over baseline methods while enabling symbolic execution tools to detect previously unknown security and correctness violations in Solidity and Rust code. The work demonstrates a practical pathway for leveraging LLMs to bridge the gap between informal requirements and rigorous formal verification.
Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
arXiv:2602.04892v2 Announce Type: replace-cross 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 automatically induces a domain-specific grammar from natural-language API rules and uses it to guide specification generation. Doc2Spec fixes a domain-agnostic logical skeleton as a grammar template, prompts LLMs to infer domain-specific predicates and sorts, and formalizes each rule within the resulting grammar, turning an unreliable one-shot translation into a sequence of constrained, checkable steps. Across six benchmarks spanning Solidity and Rust, Doc2Spec improves precision by 0.28 and recall by 0.37 over baselines that lack grammar induction or perform it in one unstaged step, demonstrating the benefits of grammar-guided formalization and the staged pipeline. Moreover, its formalized rules enable symbolic-execution tools to uncover 142 previously unknown rule violations, confirming the rules' correctness and practical usefulness.
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 automatically induces a domain-specific grammar from natural-language API rules and uses it to guide specification generation. Doc2Spec fixes a domain-agnostic logical skeleton as a grammar template, prompts LLMs to infer domain-specific predicates and sorts, and formalizes each rule within the resulting grammar, turning an unreliable one-shot translation into a sequence of constrained, checkable steps. Across six benchmarks spanning Solidity and Rust, Doc2Spec improves precision by 0.28 and recall by 0.37 over baselines that lack grammar induction or perform it in one unstaged step, demonstrating the benefits of grammar-guided formalization and the staged pipeline. Moreover, its formalized rules enable symbolic-execution tools to uncover 142 previously unknown rule violations, confirming the rules' correctness and practical usefulness.
Programming Languages (cs.PL); Artificial Intelligence (cs.AI); Software Engineering (cs.SE)
arXiv:2602.04892 [cs.PL]
(or arXiv:2602.04892v2 [cs.PL] for this version)
https://doi.org/10.48550/arXiv.2602.04892 Focus to learn more arXiv-issued DOI via DataCite
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 261 words
Related coverage
Rewrite All the Code, All the Time
LessWrong · Aug 4, 2026
Position: Natural Language Should Not Fully Replace Formal Languages
arXiv · Jul 25, 2026
Subversion-Resistance for Free from Formal Verification
LessWrong · Jun 9, 2026
claimcheck: Measuring and Improving Specification Faithfulness
arXiv · Oct 15, 2026