mlsanityData to 13 Oct 2026

Formal Specifications from Natural Language

arXiv 2206.01962 ↗First posted 4 Jun 2022cs.SE cs.LG cs.PLcited by 33

Not on the map. Why?

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.

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

Builds on

31 of 96 references.

References · 31

  1. 2017Attention Is All You Needcited by 60,106
  2. 2020Language Models are Few-Shot Learnerscited by 32,320
  3. 2020An Image is Worth 16x16 Words: Transformers for Image Recognition at Scalecited by 30,043
  4. 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,223
  5. 2019Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformercited by 14,549
  6. 2021Evaluating Large Language Models Trained on Codecited by 8,205
  7. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,317
  8. 2017A Broad-Coverage Challenge Corpus for Sentence Understanding through Inferencecited by 2,676
  9. 2022Competition-Level Code Generation with AlphaCodecited by 1,445
  10. 2020Generative Language Modeling for Automated Theorem Provingcited by 386
  11. 2019Analysing Mathematical Reasoning Abilities of Neural Modelscited by 333
  12. 2019Deep Learning for Symbolic Mathematicscited by 267
19 more
  1. 2020Unsupervised Translation of Programming Languagescited by 262
  2. 2022Autoformalization with Large Language Modelscited by 259
  3. 2018Learning a SAT Solver from Single-Bit Supervisioncited by 198
  4. 2018A Survey on Semantic Parsingcited by 62
  5. 2019Guiding High-Performance SAT Solvers with Unsat-Core Predictionscited by 62
  6. 2018First Experiments with Neural Translation of Informal to Formal Mathematicscited by 53
  7. 2020Teaching Temporal Logics to Neural Networkscited by 51
  8. 2019Enhancing the Transformer with Explicit Relational Encoding for Math Problem Solvingcited by 35
  9. 2016Neural Generation of Regular Expressions from Natural Language with Minimal Domain Knowledgecited by 24
  10. 2021CoDesc: A Large Code-Description Parallel Datasetcited by 23
  11. 2020Learning a natural-language to LTL executable semantic parser for grounded roboticscited by 22
  12. 2021DeepSTL -- From English Requirements to Signal Temporal Logiccited by 22
  13. 2021Neural Circuit Synthesis from Specification Patternscited by 17
  14. 2020Exploring Neural Models for Parsing Natural Language into First-Order Logiccited by 16
  15. 2017Learning Structured Natural Language Representations for Semantic Parsingcited by 15
  16. 2017Robust Incremental Neural Semantic Graph Parsingcited by 13
  17. 2016Semantic Parsing with Semi-Supervised Sequential Autoencoderscited by 11
  18. 2019Sketch-Driven Regular Expression Generation from Natural Language and Examplescited by 10
  19. 2018BoSy: An Experimentation Framework for Bounded Synthesiscited by 8

Built on by

Cited by year (2026 to 13 Oct)

Citing papers per year: 2022: 2; 2023: 10; 2024: 5; 2025: 9; 2026: 7.

33 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 420
  2. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 163
  3. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  4. 2024Faithful Logical Reasoning via Symbolic Chain-of-Thoughtcited by 100
  5. 2023Clover: Closed-Loop Verifiable Code Generationcited by 64
  6. 2023Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translationcited by 59
  7. 2023nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Modelscited by 57
  8. 2023Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specificationcited by 38
  9. 2022Towards a Mathematics Formalisation Assistant using Large Language Modelscited by 22
  10. 2022Learning to Follow Instructions in Text-Based Gamescited by 12
  11. 2023Fine-Tuning Language Models Using Formal Methods Feedbackcited by 12
  12. 2023Iterative Circuit Repair Against Formal Specificationscited by 9
21 more
  1. 2024TR2MTL: LLM based framework for Metric Temporal Logic Formalization of Traffic Rulescited by 9
  2. 2025HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinementcited by 6
  3. 2025Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suitecited by 4
  4. 2025SR-LLM: Rethinking the Structured Representation in Large Language Modelcited by 3
  5. 2025Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Visioncited by 3
  6. 2024Learning Temporal Logic Predicates from Data with Statistical Guaranteescited by 2
  7. 2024Towards Specification-Driven LLM-Based Generation of Embedded Automotive Softwarecited by 2
  8. 2025From Hypothesis to Premises: LLM-based Backward Logical Reasoning with Selective Symbolic Translationcited by 2
  9. 2026Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Inductioncited by 2
  10. 2023Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approachcited by 1
  11. 2024Integrating Explanations in Learning LTL Specifications from Demonstrationscited by 1
  12. 2025Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformerscited by 1
  13. 2026Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generationcited by 1
  14. 2026Semiotic logical hexagon theory for LLM logical reasoningcited by 1
  15. 2025MCP2OSC: Parametric Control by Natural Languagecited by 0
  16. 2025CP-Model-Zoo: A Natural Language Query System for Constraint Programming Modelscited by 0
  17. 2025GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translationcited by 0
  18. 2026LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoningcited by 0
  19. 2026Coherency through formalisations of Structured Natural Language, A case study on FRETishcited by 0
  20. 2026Faithful Autoformalization of Natural Language Assertionscited by 0
  21. 2026Natural Language to First-Order Logic LLM-based Autoformalizationcited by 0