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

arXiv: https://arxiv.org/abs/2602.04892 · HTML: https://mlsanity.com/paper/2602.04892/

## Key facts

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

## Builds on (most cited first, 30 of 39)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Large Language Models Can Be Easily Distracted by Irrelevant Context](https://mlsanity.com/paper/2302.00093/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Which Agent Causes Task Failures and When? On Automated Failure Attribution of LLM Multi-Agent Systems](https://mlsanity.com/paper/2505.00212/) (2025)
- [Large Language Models are Versatile Decomposers: Decompose Evidence and Questions for Table-based Reasoning](https://mlsanity.com/paper/2301.13808/) (2023)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Multilingual Machine Translation with Large Language Models: Empirical Results and Analysis](https://mlsanity.com/paper/2304.04675/) (2023)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models](https://mlsanity.com/paper/2305.07766/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [Offline Training of Language Model Agents with Functions as Learnable Weights](https://mlsanity.com/paper/2402.11359/) (2024)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [TypeWriter: Neural Type Prediction with Search-based Validation](https://mlsanity.com/paper/1912.03768/) (2019)
- [Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning](https://mlsanity.com/paper/2410.08047/) (2024)
- [Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming](https://mlsanity.com/paper/2405.01787/) (2024)
- [LOGIC-LM++: Multi-Step Refinement for Symbolic Formulations](https://mlsanity.com/paper/2407.02514/) (2024)
- [Leveraging Large Language Models for Automated Proof Synthesis in Rust](https://mlsanity.com/paper/2311.03739/) (2023)
- [Laurel: Unblocking Automated Verification with Large Language Models](https://mlsanity.com/paper/2405.16792/) (2024)

## Built on by (most cited first, 2 of 2)

- [Faithful Autoformalization of Natural Language Assertions](https://mlsanity.com/paper/2607.13303/) (2026)
- [Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees](https://mlsanity.com/paper/2608.05493/) (2026)

## 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.