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.

翻译：确保API实现与使用符合自然语言编程规则对软件正确性、安全性和可靠性至关重要。形式化验证虽能提供强有力保证，但需要精确的规范描述，而人工编写此类规范难度大、成本高。为应对这一挑战，我们提出Doc2Spec——一个基于大语言模型的多智能体框架，该框架通过语法归纳技术从自然语言规则中自动推导出规范语法，并依据推导出的语法生成形式化规范。该语法能够捕捉核心领域知识、约束规范空间并确保表示一致性，从而提升生成规范的可靠性与质量。在涵盖三种编程语言的七个基准测试中，Doc2Spec在无语法归纳的基线方法上表现更优，并与采用人工构建语法的技术取得相当的结果，这证明了自动化语法归纳在自然语言规则形式化方面的有效性。