NeuroSTAR：自动机引导的神经符号规约形式化

中文摘要 AI 辅助

将自然语言（NL）描述自动转换为有限迹上的线性时序逻辑（LTLf）是对系统动态行为进行自动形式化验证的前提。近期，多种基于大语言模型（LLM）的方法在该任务上展现出潜力，但它们难以处理自然语言描述的细微差别，导致LLM仅能部分捕捉预期含义。为解决这一局限，我们提出NeuroSTAR（自动机引导的神经符号规约形式化），这是一个NL转LTLf的框架，基于两项见解构建：其一，它利用多个生成器获取多样化的LTLf候选；其二，它基于确定有限自动机（DFA）迹开展自动机理论语义比较，以识别指导公式优化的行为分歧。我们对NeuroSTAR进行评估，结果显示，在无歧义基准测试中，相较于先前的最先进方法（SoTA），它将NL转LTLf的翻译性能提升了8至18个百分点。我们还进一步研究了其在驾驶法规文本上的适用性，这是自主车辆规约所需的复杂、现实且无参考的关键领域。该研究表明，NeuroSTAR能在83.9%的驾驶法规段落中捕捉必要的时序语义，证明了自动机引导的无参考优化在形式化中的有效性。

英文摘要

Automated translation of natural language (NL) descriptions into Linear Temporal Logic over finite traces (LTLf) is a prerequisite for automated formal verification of a system's dynamic behavior. Several LLM-based methods have recently shown potential for this task. However, they struggle with the nuance of natural language descriptions, which can lead LLMs to only partially capture the intended meaning. To address this limitation, we propose NeuroSTAR (Automata-guided Neuro-symbolic Specification Formalization), an NL-to-LTLf framework that builds on two insights. First, it leverages multiple generators to obtain diverse LTLf candidates. Second, it uses an automata-theoretic semantic comparison based on DFA traces to identify behavioral disagreements that guide formula refinement. We evaluate NeuroSTAR and show that it improves NL-to-LTLf translation performance by 8-18 percentage points relative to the prior state-of-the-art (SoTA) on unambiguous benchmarks. We further study its applicability to a body of driving law text, a complex, realistic, and reference-free domain critical for autonomous-vehicle specification. This study shows that NeuroSTAR can capture the necessary temporal semantics in 83.9% of the driving law sections, which demonstrates the effectiveness of automata-guided reference-free refinement in formalization.

发表机构

• University of Virginia（弗吉尼亚大学）
• William & Mary（威廉玛丽学院）

机构由 AI 辅助整理，请以论文原文为准。