Dilemma of LLM Translation for Temporal Logic: Syntax Easy to Master, Semantics Still a Challenge

This article systematically evaluates the ability of large language models (LLMs) to translate natural language into Linear Temporal Logic (LTL). It finds that LLMs perform well at the syntax level but have significant deficiencies in semantic understanding. The study proposes that reconstructing the task as a Python code completion task can significantly improve performance, providing a reference for lowering the threshold of formal methods.

LTL is an important formal specification language in fields such as software engineering and cybersecurity, capable of precisely describing the temporal behavior of systems. However, its steep learning curve and the error-prone nature of translating natural language to LTL have become bottlenecks for the popularization of formal methods. The emergence of LLMs brings hope for solving this problem—if accurate translation can be achieved, it can lower the threshold for using such tools.

The research team designed a six-layer evaluation framework. Strategies to solve the ontology problem (propositional variable mapping) include prompt engineering, syntax-constrained decoding, and semantic equivalence checking (verified using NuSMV). Three types of LLMs were tested: proprietary general-purpose LLMs (e.g., GPT-4), fine-tuned specialized LLMs, and open-source foundation models.

1. Syntax performance is better than semantics: The best model has high syntax accuracy but low semantic equivalence accuracy; 2. Detailed prompts significantly improve performance: From basic to enhanced prompts, performance increases by 20-30%; 3. Breakthrough via Python code completion reconstruction: Convert the task into completing a Python function that outputs LTL, leveraging the LLM's code capabilities to improve performance.

1. Misuse of temporal operators: Confusing G (globally), F (finally), etc.; 2. Bias in propositional variable selection: Over-simplifying logical structures (e.g., using a single variable instead of logical AND); 3. Difficulty with past-tense operators: Future tense performs better than past tense (e.g., S, Y), possibly due to scarce training data.

Testing 56 security requirements (authentication, sessions, etc.) revealed challenges: complex domains, importance of propositional grounding, and scope errors of temporal operators. However, performance can be significantly improved through prompt engineering and task reconstruction.

Tool developers: Adopt human-machine collaboration (LLM generation + expert correction), interactive clarification, and multi-model integration; Researchers: Build specialized training data, integrate neural-symbolic approaches, and explore task reconstruction strategies.

Limitations: Limited dataset size, only evaluating English-to-LTL translation, static one-time translation; Future directions: Larger datasets, multi-language and extended LTL (MTL/STL), dynamic interactive translation scenarios.