# Formal Specifications from Natural Language

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

## Key facts

- Cited by 33 papers in the map (data through 14 Oct 2026).
- Builds on 31 of its 96 references that are in the map.
- First posted on arXiv 4 Jun 2022.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [An Image is Worth 16x16 Words: Transformers for Image Recognition at Scale](https://mlsanity.com/paper/2010.11929/) (2020)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [PaLM: Scaling Language Modeling with Pathways](https://mlsanity.com/paper/2204.02311/) (2022)
- [A Broad-Coverage Challenge Corpus for Sentence Understanding through Inference](https://mlsanity.com/paper/1704.05426/) (2017)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Unsupervised Translation of Programming Languages](https://mlsanity.com/paper/2006.03511/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [A Survey on Semantic Parsing](https://mlsanity.com/paper/1812.00978/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Enhancing the Transformer with Explicit Relational Encoding for Math Problem Solving](https://mlsanity.com/paper/1910.06611/) (2019)
- [Neural Generation of Regular Expressions from Natural Language with Minimal Domain Knowledge](https://mlsanity.com/paper/1608.03000/) (2016)
- [CoDesc: A Large Code-Description Parallel Dataset](https://mlsanity.com/paper/2105.14220/) (2021)
- [Learning a natural-language to LTL executable semantic parser for grounded robotics](https://mlsanity.com/paper/2008.03277/) (2020)
- [DeepSTL -- From English Requirements to Signal Temporal Logic](https://mlsanity.com/paper/2109.10294/) (2021)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [Exploring Neural Models for Parsing Natural Language into First-Order Logic](https://mlsanity.com/paper/2002.06544/) (2020)
- [Learning Structured Natural Language Representations for Semantic Parsing](https://mlsanity.com/paper/1704.08387/) (2017)
- [Robust Incremental Neural Semantic Graph Parsing](https://mlsanity.com/paper/1704.07092/) (2017)
- [Semantic Parsing with Semi-Supervised Sequential Autoencoders](https://mlsanity.com/paper/1609.09315/) (2016)
- [Sketch-Driven Regular Expression Generation from Natural Language and Examples](https://mlsanity.com/paper/1908.05848/) (2019)

## Built on by (most cited first, 30 of 33)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation](https://mlsanity.com/paper/2305.15541/) (2023)
- [Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification](https://mlsanity.com/paper/2303.08006/) (2023)
- [Towards a Mathematics Formalisation Assistant using Large Language Models](https://mlsanity.com/paper/2211.07524/) (2022)
- [Learning to Follow Instructions in Text-Based Games](https://mlsanity.com/paper/2211.04591/) (2022)
- [Fine-Tuning Language Models Using Formal Methods Feedback](https://mlsanity.com/paper/2310.18239/) (2023)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [TR2MTL: LLM based framework for Metric Temporal Logic Formalization of Traffic Rules](https://mlsanity.com/paper/2406.05709/) (2024)
- [HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement](https://mlsanity.com/paper/2505.15740/) (2025)
- [Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite](https://mlsanity.com/paper/2507.00877/) (2025)
- [Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision](https://mlsanity.com/paper/2508.18675/) (2025)
- [Learning Temporal Logic Predicates from Data with Statistical Guarantees](https://mlsanity.com/paper/2406.10449/) (2024)
- [SR-LLM: Rethinking the Structured Representation in Large Language Model](https://mlsanity.com/paper/2502.14352/) (2025)
- [Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software](https://mlsanity.com/paper/2411.13269/) (2024)
- [From Hypothesis to Premises: LLM-based Backward Logical Reasoning with Selective Symbolic Translation](https://mlsanity.com/paper/2512.03360/) (2025)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach](https://mlsanity.com/paper/2312.17353/) (2023)
- [Integrating Explanations in Learning LTL Specifications from Demonstrations](https://mlsanity.com/paper/2404.02872/) (2024)
- [Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformers](https://mlsanity.com/paper/2507.07808/) (2025)
- [Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation](https://mlsanity.com/paper/2606.05792/) (2026)
- [Faithful Autoformalization of Natural Language Assertions](https://mlsanity.com/paper/2607.13303/) (2026)
- [Semiotic logical hexagon theory for LLM logical reasoning](https://mlsanity.com/paper/2607.21933/) (2026)
- [MCP2OSC: Parametric Control by Natural Language](https://mlsanity.com/paper/2508.10414/) (2025)
- [CP-Model-Zoo: A Natural Language Query System for Constraint Programming Models](https://mlsanity.com/paper/2509.07867/) (2025)
- [GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation](https://mlsanity.com/paper/2512.16770/) (2025)

## Abstract (arXiv)

We study the generalization abilities of language models when translating natural language into formal specifications with complex semantics. In particular, we fine-tune language models on three datasets consisting of English sentences and their corresponding formal representation: 1) regular expressions (regex), frequently used in programming and search; 2) First-order logic (FOL), commonly used in software verification and theorem proving; and 3) linear-time temporal logic (LTL), which forms the basis for industrial hardware specification languages. Our experiments show that, in these diverse domains, the language models maintain their generalization capabilities from pre-trained knowledge of natural language to generalize, e.g., to new variable names or operator descriptions. Additionally, they achieve competitive performance, and even outperform the state-of-the-art for translating into regular expressions, with the benefits of being easy to access, efficient to fine-tune, and without a particular need for domain-specific reasoning.