NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
NeuroNL2LTL is a neurosymbolic framework designed to translate natural language into Linear Temporal Logic (LTL). This system combines learned translation with formal verification to enhance reliability in safety-critical applications. It achieves significant semantic equivalence while ensuring outputs are verified for correctness.
- ▪NeuroNL2LTL unifies learned translation with formal verification to improve the translation of natural language to LTL.
- ▪The framework uses an intermediate representation that preserves the structure of LTL, allowing for effective verification.
- ▪It has been tested on over 200,000 requirements across various domains, achieving 28% semantic equivalence and 86% verified satisfiability.
Opening excerpt (first ~120 words) tap to expand
Computer Science > Artificial Intelligence arXiv:2605.22874 (cs) [Submitted on 20 May 2026] Title:NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic Authors:Paapa Kwesi Quansah, Ernest Bonnah View a PDF of the paper titled NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic, by Paapa Kwesi Quansah and 1 other authors View PDF HTML (experimental) 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.
…
Excerpt limited to ~120 words for fair-use compliance. The full article is at arXiv cs.AI.
Discussion
0 commentsMore from arXiv cs.AI
