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

• URL: http://arxiv.org/abs/2602.04892v1
• Date: Fri, 30 Jan 2026 02:58:27 GMT
• Title: Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction
• Authors: Shihao Xia, Mengting He, Haomin Jia, Linhai Song,
• Abstract summary: Doc2Spec is a framework that automatically induces a specification grammar from natural-language rules.<n>It generates formal specifications guided by the induced grammar.<n>The grammar captures essential domain knowledge, constrains the specification space, and enforces consistent representations.
• Score: 3.13621719351502
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• 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.

Related papers

• Synthesizing Precise Protocol Specs from Natural Language for Effective Test Generation [42.582977261473324]
  AutoSPEC recovers on average 92.8% of client and 80.2% of server message types, and 81.5% message acceptance across diverse real-world systems.<n>Prototype successfully demonstrated the feasibility of our approach on five widely used.<n>internet-based protocols.
  arXiv  Detail & Related papers  (2025-11-22T08:39:52Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• NoviCode: Generating Programs from Natural Language Utterances by Novices [59.71218039095155]
  We present NoviCode, a novel NL Programming task which takes as input an API and a natural language description by a novice non-programmer. We show that NoviCode is indeed a challenging task in the code synthesis domain, and that generating complex code from non-technical instructions goes beyond the current Text-to-Code paradigm.
  arXiv  Detail & Related papers  (2024-07-15T11:26:03Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• DECIDER: A Dual-System Rule-Controllable Decoding Framework for Language Generation [57.07295906718989]
  Constrained decoding approaches aim to control the meaning or style of text generated by pre-trained large language (Ms also PLMs) for various tasks at inference time.<n>These methods often guide plausible continuations by greedily and explicitly selecting targets.<n>Inspired by cognitive dual-process theory, we propose a novel decoding framework DECIDER.
  arXiv  Detail & Related papers  (2024-03-04T11:49:08Z)
• SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
  SpecGen is a novel technique for formal program specification generation based on Large Language Models.<n>We evaluate SpecGen on two datasets, including the SV-COMP 279 benchmark and a manually constructed dataset.
  arXiv  Detail & Related papers  (2024-01-16T20:13:50Z)
• Large Language Models Based Automatic Synthesis of Software Specifications [3.081650600579376]
  SpecSyn is a framework that automatically synthesizes software specifications from natural language sources. Our approach formulates software specification synthesis as a sequence-to-sequence learning problem.
  arXiv  Detail & Related papers  (2023-04-18T01:22:44Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  We present nl2spec, a framework for applying Large Language Models (LLMs) derive formal specifications from unstructured natural language. We introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization.
  arXiv  Detail & Related papers  (2023-03-08T20:08:53Z)
• Benchmarking Language Models for Code Syntax Understanding [79.11525961219591]
  Pre-trained language models have demonstrated impressive performance in both natural language processing and program understanding. In this work, we perform the first thorough benchmarking of the state-of-the-art pre-trained models for identifying the syntactic structures of programs. Our findings point out key limitations of existing pre-training methods for programming languages, and suggest the importance of modeling code syntactic structures.
  arXiv  Detail & Related papers  (2022-10-26T04:47:18Z)
• The Whole Truth and Nothing But the Truth: Faithful and Controllable Dialogue Response Generation with Dataflow Transduction and Constrained Decoding [65.34601470417967]
  We describe a hybrid architecture for dialogue response generation that combines the strengths of neural language modeling and rule-based generation. Our experiments show that this system outperforms both rule-based and learned approaches in human evaluations of fluency, relevance, and truthfulness.
  arXiv  Detail & Related papers  (2022-09-16T09:00:49Z)
• Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
  We develop an automated framework for extracting a first-pass grammatical specification from raw text. We focus on extracting rules describing agreement, a morphosyntactic phenomenon at the core of the grammars of many of the world's languages. We apply our framework to all languages included in the Universal Dependencies project, with promising results.
  arXiv  Detail & Related papers  (2020-10-02T18:31:45Z)
• SPECTER: Document-level Representation Learning using Citation-informed Transformers [51.048515757909215]
  SPECTER generates document-level embedding of scientific documents based on pretraining a Transformer language model. We introduce SciDocs, a new evaluation benchmark consisting of seven document-level tasks ranging from citation prediction to document classification and recommendation.
  arXiv  Detail & Related papers  (2020-04-15T16:05:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.