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

• URL: http://arxiv.org/abs/2605.22874v1
• Date: Wed, 20 May 2026 03:31:51 GMT
• Title: NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
• Abstract summary: We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification.<n>On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28% semantic equivalence with reference specifications.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications [28.546702829415207]
  Translating natural language instructions into machine-interpretable formal specifications enables robots and autonomous systems to plan, reason, and formally verify their behavior.<n>Existing translation models typically generate a specification for every input, even when the result is unreliable or fails to capture the user's intent.<n>Inspired by selective conformal prediction, we propose a selective translation framework that not only generates formal specifications but also determines when they can be trusted.
  arXiv  Detail & Related papers  (2026-08-05T22:17:09Z)
• CASS-RTL: Correctness-Aware Subspace Steering for RTL Generation with LLMs [0.0]
  This work proposes CASS-RTL, a first-of-its-kind framework for discovering and leveraging LLMs' correctness-aware components.<n>We observe 10%-20% improvement in pass@1/5/10 accuracy on VerilogEval and 5% improvement on CVDP.
  arXiv  Detail & Related papers  (2026-06-04T04:02:51Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning [5.961092142323502]
  textscReasonSTL is a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation.<n>textscReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction.<n>Experiments show that a 4B model trained with textscReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations.
  arXiv  Detail & Related papers  (2026-05-07T16:07:30Z)
• LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning [2.365021420497964]
  Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL)<n>In this work, we focus on enabling resource-efficient open-weight models to generate correct temporal logic (LTL) specifications from informal requirements.<n>We presentGuard, a modular toolchain that combines constrained generation with formal consistency checking to generate conflict-free specifications from informal input.
  arXiv  Detail & Related papers  (2026-03-05T22:34:45Z)
• VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
  Referring Expression (REC) aims to localize the image region corresponding to a natural-language query.<n>Recent neuro-symbolic REC approaches leverage large language models (LLMs) and vision-language models (VLMs) to perform compositional reasoning.<n>We introduce VIRO, a neuro-symbolic framework that embeds lightweight operator-level verifiers within reasoning steps.
  arXiv  Detail & Related papers  (2026-01-19T07:21:19Z)
• Training LLMs with LogicReward for Faithful and Rigorous Reasoning [75.30425553246177]
  We propose LogicReward, a reward system that guides model training by enforcing step-level logical correctness with a theorem prover.<n>An 8B model trained on data constructed with LogicReward surpasses GPT-4o and o4-mini by 11.6% and 2% on natural language inference and logical reasoning tasks.
  arXiv  Detail & Related papers  (2025-12-20T03:43:02Z)
• Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs [10.958536923155101]
  Req2LTL is a modular framework that bridges NL and Linear Temporal Logic.<n>It achieves 88.4% semantic accuracy and 100% syntactic correctness on real-world aerospace requirements.
  arXiv  Detail & Related papers  (2025-12-19T08:25:54Z)
• ProSLM : A Prolog Synergized Language Model for explainable Domain Specific Knowledge Based Question Answering [0.0]
  Neurosymbolic approaches can add robustness to opaque neural systems by incorporating explainable symbolic representations. We propose systemname, a novel neurosymbolic framework, to improve robustness and reliability of large language models. Our work opens a new area of neurosymbolic generative AI text validation and user personalization.
  arXiv  Detail & Related papers  (2024-09-17T22:34:33Z)
• Neuro-Symbolic Inductive Logic Programming with Logical Neural Networks [65.23508422635862]
  We propose learning rules with the recently proposed logical neural networks (LNN) Compared to others, LNNs offer strong connection to classical Boolean logic. Our experiments on standard benchmarking tasks confirm that LNN rules are highly interpretable.
  arXiv  Detail & Related papers  (2021-12-06T19:38:30Z)
• FF-NSL: Feed-Forward Neural-Symbolic Learner [70.978007919101]
  This paper introduces a neural-symbolic learning framework, called Feed-Forward Neural-Symbolic Learner (FF-NSL) FF-NSL integrates state-of-the-art ILP systems based on the Answer Set semantics, with neural networks, in order to learn interpretable hypotheses from labelled unstructured data.
  arXiv  Detail & Related papers  (2021-06-24T15:38:34Z)
• NSL: Hybrid Interpretable Learning From Noisy Raw Data [66.15862011405882]
  This paper introduces a hybrid neural-symbolic learning framework, called NSL, that learns interpretable rules from labelled unstructured data. NSL combines pre-trained neural networks for feature extraction with FastLAS, a state-of-the-art ILP system for rule learning under the answer set semantics. We demonstrate that NSL is able to learn robust rules from MNIST data and achieve comparable or superior accuracy when compared to neural network and random forest baselines.
  arXiv  Detail & Related papers  (2020-12-09T13:02:44Z)
• Logical Natural Language Generation from Open-Domain Tables [107.04385677577862]
  We propose a new task where a model is tasked with generating natural language statements that can be emphlogically entailed by the facts. To facilitate the study of the proposed logical NLG problem, we use the existing TabFact dataset citechen 2019tabfact featured with a wide range of logical/symbolic inferences. The new task poses challenges to the existing monotonic generation frameworks due to the mismatch between sequence order and logical order.
  arXiv  Detail & Related papers  (2020-04-22T06:03:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.