# Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation

arXiv: https://arxiv.org/abs/2604.07321 · HTML: https://mlsanity.com/paper/2604.07321/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 66 references that are in the map.
- First posted on arXiv 8 Apr 2026.

## Builds on (most cited first, 14 of 14)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [CodeT5: Identifier-aware Unified Pre-trained Encoder-Decoder Models for Code Understanding and Generation](https://mlsanity.com/paper/2109.00859/) (2021)
- [StarCoder: may the source be with you!](https://mlsanity.com/paper/2305.06161/) (2023)
- [Can Large Language Models Reason and Plan?](https://mlsanity.com/paper/2403.04121/) (2024)
- [Flexible and Efficient Grammar-Constrained Decoding](https://mlsanity.com/paper/2502.05111/) (2025)
- [Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control](https://mlsanity.com/paper/2406.07400/) (2024)
- [Linear-time Temporal Logic guided Greybox Fuzzing](https://mlsanity.com/paper/2109.02312/) (2021)
- [Quickstrom: Property Based Acceptance Testing with LTL Specifications](https://mlsanity.com/paper/2203.11532/) (2022)
- [Model Checking Access Control Policies: A Case Study using Google Cloud IAM](https://mlsanity.com/paper/2303.16688/) (2023)
- [CloudFix: Automated Policy Repair for Cloud Access Control Policies Using Large Language Models](https://mlsanity.com/paper/2512.09957/) (2025)
- [Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits](https://mlsanity.com/paper/1508.02448/) (2015)
- [PHOENIX: Device-Centric Cellular Network Protocol Monitoring using Runtime Verification](https://mlsanity.com/paper/2101.00328/) (2021)
- [MAVERICK: An App-independent and Platform-agnostic Approach to Enforce Policies in IoT Systems at Runtime](https://mlsanity.com/paper/2302.01452/) (2023)

## Abstract (arXiv)

Propositional Linear Temporal Logic (LTL) is a popular formalism for specifying desirable requirements and security and privacy policies for software, networks, and systems. Yet expressing such requirements and policies in LTL remains challenging because of its intricate semantics. Since many security and privacy analysis tools require LTL formulas as input, this difficulty places them out of reach for many developers and analysts. Large Language Models (LLMs) could broaden access to such tools by translating natural language fragments into LTL formulas. This paper evaluates that premise by assessing how effectively several representative LLMs translate assertive English sentences into LTL formulas. Using both human-generated and synthetic ground-truth data, we evaluate effectiveness along syntactic and semantic dimensions. The results reveal three findings: (1) in line with prior findings, LLMs perform better on syntactic aspects of LTL than on semantic ones; (2) they generally benefit from more detailed prompts; and (3) reformulating the task as a Python code-completion problem substantially improves overall performance. We also discuss challenges in conducting a fair evaluation on this task and conclude with recommendations for future work.