评测大模型将自然语言转为时序逻辑公式的效果，发现语义理解是短板。
Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation
- 用提示词优化和代码补全任务提升翻译效果
- 模型在语法正确性上表现好，但语义准确率低
- 适合安全分析、系统验证等需要形式化表达的领域
命题线性时序逻辑（LTL）是描述软件、网络与系统中期望需求及安全隐私策略的常用形式化方法。然而，由于其复杂的语义，用LTL表达这些要求仍具挑战性，限制了非专业人员使用依赖LTL输入的安全与隐私分析工具。大语言模型（LLMs）有望通过将自然语言片段转化为LTL公式来降低使用门槛。本文评估了多个代表性LLM在将陈述性英文句子转换为LTL公式方面的表现，采用人工生成与合成的真实标签数据，在句法与语义两个维度进行评估。结果表明：（1）与以往研究一致，LLMs在句法层面优于语义层面；（2）更详细的提示词能显著提升性能；（3）将任务重构为Python代码补全问题可大幅提升整体表现。我们还讨论了该任务公平评估的挑战，并提出未来研究建议。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。