用自然语言生成编程规范，自动提炼语法规则提升准确性
Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
- 通过多智能体框架从自然语言中自动归纳语法规则
- 在7个基准上优于无语法诱导的基线，接近人工语法规则效果
- 适合需要高可靠性的软件验证与自动化规范生成场景
确保API实现与使用符合自然语言编程规则对软件正确性、安全性和可靠性至关重要。形式化验证虽能提供强保证，但需精确规范，而手动编写成本高且困难。为此，我们提出Doc2Spec，一种基于大模型的多智能体框架，通过自然语言规则自动归纳出规格语法规则，并以此引导生成形式化规范。该语法规则捕捉关键领域知识，约束规范空间并统一表示，从而提升生成规范的可靠性与质量。在三种编程语言的七个基准上评估，Doc2Spec优于无语法诱导的基线，且达到与人工构建语法规则相当的性能，证明了自动化语法归纳在形式化自然语言规则中的有效性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。