Doc2Spec: 通过语法归纳从自然语言生成形式化编程规范
Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
AI总结：
Doc2Spec通过语法归纳自动从自然语言生成形式化编程规范，提升了规范生成的可靠性和质量。
摘要：
确保API实现和使用符合自然语言编程规则对于软件正确性、安全性和可靠性至关重要。形式化验证可以提供强有力的保证，但需要精确的规范，而手动编写这些规范是困难且昂贵的。为了解决这一挑战，我们提出了Doc2Spec，一个多智能体框架，利用大语言模型自动归纳自然语言规则中的规范语法，然后根据归纳出的语法生成形式化规范。该语法捕捉了关键的领域知识，约束了规范空间，并强制一致的表示，从而提高了生成规范的可靠性和质量。在三种编程语言的七个基准测试中评估，Doc2Spec优于没有语法归纳的基线方法，并在与手动编写的语法技术竞争中取得具有竞争力的结果，证明了自动化语法归纳在形式化自然语言规则中的有效性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
