mlsanityData to 7 Oct 2026

NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic

arXiv 2605.22874 ↗First posted 20 May 2026cs.AI cs.LOcited by 0

Not on the map. Why?

Abstract (arXiv)

Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification's reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28% semantic equivalence with reference specifications while ensuring 86% of outputs are verified satisfiable. The system also generates contextually grounded explanations from LTL, enabling domain experts to validate specifications without specialized training. This work demonstrates that formal verification can function as both training objective and runtime filter for neural specification systems, allowing us to build neural-based tools whose reliability derives from logical guarantees rather than statistical confidence.

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 22 of its 43 references that are in the map. First posted on arXiv 20 May 2026.

Builds on

22 of 43 references.

References · 22

  1. 2022Training language models to follow instructions with human feedbackcited by 15,712
  2. 2017Deep reinforcement learning from human preferencescited by 3,846
  3. 2023Let's Verify Step by Stepcited by 3,598
  4. 2022Constitutional AI: Harmlessness from AI Feedbackcited by 2,950
  5. 2019Neural Probabilistic Logic Programming in DeepProbLogcited by 389
  6. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  7. 2022CodeRL: Mastering Code Generation through Pretrained Models and Deep Reinforcement Learningcited by 342
  8. 2017A Semantic Loss Function for Deep Learning with Symbolic Knowledgecited by 267
  9. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  10. 2018SequenceR: Sequence-to-Sequence Learning for End-to-End Program Repaircited by 144
  11. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  12. 2023Scallop: A Language for Neurosymbolic Programmingcited by 63
10 more
  1. 2023nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Modelscited by 57
  2. 2023NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Modelscited by 57
  3. 2023Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environmentscited by 52
  4. 2021Neural Program Repair with Execution-based Backpropagationcited by 50
  5. 2015Shield Synthesis: Runtime Enforcement for Reactive Systemscited by 41
  6. 2018Learning Linear Temporal Propertiescited by 41
  7. 2021Modular Deep Reinforcement Learning for Continuous Motion Planning with Temporal Logiccited by 38
  8. 2023Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specificationcited by 38
  9. 2020Learning a natural-language to LTL executable semantic parser for grounded roboticscited by 22
  10. 2020Learning Interpretable Models in the Property Specification Languagecited by 11

Built on by

Not cited yet.