NeuroSTAR: Automata-guided Neuro-symbolic Specification Formalization

Abstract

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.