语法是容易的，语义是困难的：评估LLM在LTL翻译中的表现
Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation
AI总结：
本文评估了多个LLM将自然语言句子转换为LTL公式的能力，发现其在语法层面表现较好，但在语义层面存在挑战，且更详细的提示和重新表述为代码补全问题能提升性能。
摘要：
命题线性时序逻辑（LTL）是一种用于规范软件、网络和系统中 desirable 要求和安全隐私政策的流行形式化方法。然而，由于其复杂的语义，将这些要求和政策表达为 LTL 仍具挑战性。由于许多安全隐私分析工具需要 LTL 公式作为输入，这种难度使许多开发者和分析师难以触及。大型语言模型（LLM）可以通过将自然语言片段翻译成 LTL 公式来扩大这些工具的可访问性。本文通过评估几个代表性 LLM 将断言性英语句子转换为 LTL 公式的效果，验证了这一前提。使用人类生成和合成的真实数据，我们从语法和语义维度评估了有效性。结果揭示了三个发现：（1）与以往发现一致，LLM 在 LTL 的语法方面表现优于语义方面；（2）它们通常受益于更详细的提示；（3）将任务重新表述为 Python 代码补全问题显著提升了整体性能。我们还讨论了在该任务上进行公平评估的挑战，并以未来工作的建议作为结论。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
