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.

翻译：命题线性时序逻辑（LTL）是一种用于描述软件、网络及系统中预期需求、安全与隐私策略的流行形式化规范。然而，由于其复杂的语义，用LTL表达此类需求与策略仍具挑战性。由于众多安全与隐私分析工具要求以LTL公式作为输入，这一难点使得许多开发者和分析人员难以使用这些工具。大型语言模型（LLMs）可通过将自然语言片段翻译为LTL公式，拓宽对这些工具的可及性。本文通过评估若干代表性LLMs将断言性英语句子转化为LTL公式的有效性，对该前提进行了检验。基于人工生成和合成真实数据，我们从语法与语义两个维度评估了翻译效果。结果揭示了三个发现：（1）与先前研究一致，LLMs在LTL的语法方面表现优于语义方面；（2）更详细的提示通常能提升其性能；（3）将任务重构为Python代码补全问题可显著改善整体表现。我们还讨论了在此任务中开展公平评估的挑战，并总结了对未来工作的建议。