mlsanityData to 7 Oct 2026

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

arXiv 2602.04892 ↗First posted 30 Jan 2026cs.PL cs.AI cs.SEcited by 2

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). Builds on 39 of its 65 references that are in the map. First posted on arXiv 30 Jan 2026.

Builds on

39 of 65 references.

References · 39

  1. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  2. 2023Large Language Models Can Be Easily Distracted by Irrelevant Contextcited by 820
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  4. 2023Llemma: An Open Language Model For Mathematicscited by 385
  5. 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 379
  6. 2022Autoformalization with Large Language Modelscited by 252
  7. 2023Large Language Models are Versatile Decomposers: Decompose Evidence and Questions for Table-based Reasoningcited by 177
  8. 2025Which Agent Causes Task Failures and When? On Automated Failure Attribution of LLM Multi-Agent Systemscited by 170
  9. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 161
  10. 2023Multilingual Machine Translation with Large Language Models: Empirical Results and Analysiscited by 156
  11. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  12. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
27 more
  1. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  2. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  3. 2023NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Modelscited by 57
  4. 2024Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verificationcited by 55
  5. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  6. 2024SpecGen: Automated Generation of Formal Program Specifications via Large Language Modelscited by 51
  7. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  8. 2024Offline Training of Language Model Agents with Functions as Learnable Weightscited by 47
  9. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  10. 2023Finding Inductive Loop Invariants using Large Language Modelscited by 35
  11. 2022Formal Specifications from Natural Languagecited by 33
  12. 2019TypeWriter: Neural Type Prediction with Search-based Validationcited by 32
  13. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 31
  14. 2024Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoningcited by 27
  15. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  16. 2024LOGIC-LM++: Multi-Step Refinement for Symbolic Formulationscited by 14
  17. 2023Leveraging Large Language Models for Automated Proof Synthesis in Rustcited by 11
  18. 2025ClassInvGen: Class Invariant Synthesis using Large Language Modelscited by 11
  19. 2024Laurel: Unblocking Automated Verification with Large Language Modelscited by 10
  20. 2025VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Veruscited by 8
  21. 2025Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMscited by 8
  22. 2024Evaluating Large Language Models in Semantic Parsing for Conversational Question Answering over Knowledge Graphscited by 7
  23. 2020Towards making formal methods normal: meeting developers where they arecited by 2
  24. 2025SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Modelscited by 2
  25. 2017Automating Deductive Verification for Weak-Memory Programscited by 1
  26. 2019Towards A Broader Acceptance Of Formal Verification Tools: The Role Of Educationcited by 1
  27. 2019What should I document? A preliminary systematic mapping study into API documentation knowledgecited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 2.

2 papers.

  1. 2026Faithful Autoformalization of Natural Language Assertionscited by 0
  2. 2026Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guaranteescited by 0