Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper evaluates the ability of LLMs to translate natural language into LTL formulas, a crucial task for specifying requirements in security and privacy analysis. The study finds that LLMs struggle with the semantic aspects of LTL, even though they perform relatively well on syntax. However, performance improves with more detailed prompts and when the task is framed as Python code completion.
LLMs can handle the syntax of translating natural language to LTL, but still fail on the more important semantics, highlighting a key gap in their ability to formalize complex requirements.
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.