PaperlayerView exact revision on arXiv

Source-linked AI summary

NeuroSTAR: Automata-guided Neuro-symbolic Specification Formalization

Joy Saha, Trey Woodlief, Sebastian Elbaum, Matthew B. Dwyer

arXiv:2609.03161v1cs.FL

TL;DR

NL-to-LTLf systems must capture intended meaning from natural-language requirements, but LLM-based formalizations can miss semantic constraints. NEUROSTAR combines multiple generators with automata-guided trace comparison and iterative refinement. It achieves best or joint-best accuracy on three of four filtered benchmark datasets and outperforms all baselines on both strict datasets.

  • Problem

    LLM-based formalizations can be syntactically correct yet fail to capture semantic constraints in natural-language requirements.

    Source: §I · p. 1

  • Method

    NEUROSTAR generates multiple LTLf candidates and uses automata-theoretic disagreements among their traces to guide iterative refinement.

    Source: §I · p. 1, §VIII · p. 10

  • Results

    NEUROSTAR achieves best or joint-best accuracy on three of four filtered datasets and outperforms all baselines on both strict datasets, reaching 96.4% on CONFONLst and 100% on SYNTHNLst.

    Source: §VIII · p. 10

  • Takeaways & Limitations

    The benchmark evaluation supports automata-guided refinement as an approach that establishes state-of-the-art performance in NL-to-LTLf formalization.

    Source: §VIII · p. 10

    Reported results may vary with design parameters and generator or judge models, and existing benchmarks may not capture the complexity of realistic specifications.

    Source: §VII · p. 10

Abstract

from arXiv · show

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.

I. INTRODUCTION

NEUROSTAR addresses the difficulty LLMs have capturing semantic constraints in natural-language specifications by using automata-guided refinement of multiple generated candidates. The paper also audits benchmark datasets and evaluates the framework on prior benchmarks and Virginia driving laws.

I. INTRODUCTION

  • LLMs can produce syntactically correct formalizations but are less effective at capturing semantic constraints, while temporal logic semantics are amenable to symbolic encoding and algorithmic manipulation.Source: §I · p. 1
  • NEUROSTAR converts candidate temporal-logic specifications into automata, finds traces where candidates disagree, and iteratively asks LLMs to minimize those disagreements.The framework combines multiple generators to refine a final specification.Source: §I · p. 1
  • The evaluation replicates ADARULE and identifies dataset inconsistencies, then examines whether the benchmarks capture interpretive challenges found in real-world requirements.The paper presents a benchmark audit, a comparison with real-world specifications, and a reference-free study of Virginia driving laws.Source: §I · pp. 1–2
  • NEUROSTAR establishes a new state of the art on prior benchmarks and produces driving-law formalizations satisfying a necessary correctness condition for 89 of 106 reviewed laws.The reviewed laws include obligations, exceptions, and interactions among multiple road users.Source: §I · p. 1

A. Temporal Logics

LTL and LTLf share syntax but differ in trace semantics, and NEUROSTAR targets LTLf for finite-mission cyber-physical systems. The paper situates its approach among prior NL-to-temporal-logic methods and frames a benchmark study around dataset quality and real-world interpretive challenges.

A. Temporal Logics

  • LTL formulas are interpreted over infinite traces and compile to Büchi automata, whereas LTLf formulas use finite traces and compile to deterministic finite automata.The logics share syntax, but their differing semantics can also yield different expressibility.Source: A. Temporal Logics · p. 2
  • LTLf is the target because finite-length missions make it practically useful for cyber-physical-system specifications.Source: A. Temporal Logics · p. 2

B. Natural Language to Temporal Logic Translation

  • NL-to-temporal-logic work progressed from pattern classification and paired-data transformers to LLM methods, but existing approaches face data limitations or lack multiple perspectives and automata-based semantic reasoning.NEUROSTAR is motivated as a reference-free, multi-generator framework with automata-theoretic reasoning.Source: B. Natural Language to Temporal Logic… · p. 2

III. BENCHMARK STUDY

  • The benchmark study examines ambiguity, incorrect ground-truth formulas, LTL-to-LTLf effects, and whether existing datasets capture real-world interpretation challenges.The audit considers CONFONL, SYNTHNL, LANGNL, and SPECNL, whose weaknesses could affect construct and external validity.Source: §III · pp. 2–3

A. RQ1: Benchmark Ambiguity

The benchmark analysis identifies dataset ambiguities and finds that existing benchmarks underrepresent the interpretive challenges of real-world specifications. It filters or edits problematic examples and contrasts candidate-formula diversity on CONFONLf and Virginia driving law.

A. RQ1: Benchmark Ambiguity

  • CONFONLf and SYNTHNLf labels favor non-strict timing interpretations, so the authors remove divergent strict/non-strict cases rather than impose their own interpretation.This removed 60 pairs (31.08%) across the two datasets.Source: A. RQ1: Benchmark Ambiguity · p. 3

B. RQ2: Benchmark Simplicity

  • 84.7% of CONFONLf inputs yielded syntactically identical candidates and 86.7% semantically identical candidates, versus 23.1% and 25.0% for VALAW.Mean syntactic and semantic distances were 0.057 and 0.043 for CONFONLf, versus 0.257 and 0.472 for VALAW.Source: Figure 1 · p. 3, B. RQ2: Benchmark Simplicity · p. 4

A. RQ1: Benchmark Ambiguity

  • Anaphoric ambiguity can leave a reference such as “there” unclear; the authors minimally rewrote seven CONFONLst specifications to make the referent explicit.The example’s LTL label indicates that “there” refers to AP1.Source: A. RQ1: Benchmark Ambiguity · p. 3
  • Filtering removed up to 48.43% of entries for contamination, trivial formulae, temporal ambiguity, and LTLf incompatibility; an additional 4.27% of remaining entries were edited for anaphoric ambiguity.The evaluation also removes 18 pairs (5.7%) for LTLf incompatibility, incorrect labels, or trivial formulae, and 76 duplicated LANGNL test pairs (76%).Source: A. RQ1: Benchmark Ambiguity · p. 3

B. RQ2: Benchmark Simplicity

  • Existing benchmarks underrepresent real-world interpretive difficulty: CONFONLf entries average 30× fewer words, with syntactic and semantic distances approximately 4.5× and 11× smaller than VALAW.The authors interpret VALAW’s broader semantic-distance distribution as evidence of genuinely different behavioral interpretations, not merely alternate syntax.Source: B. RQ2: Benchmark Simplicity · p. 4

IV. THE NEUROSTAR APPROACH

NEUROSTAR combines multiple LLM-generated LTLf candidates with automata-based semantic comparisons to guide training-free iterative refinement. Concrete trace disagreements provide feedback for refining candidates against the natural-language requirement.

IV. THE NEUROSTAR APPROACH

  • NEUROSTAR aims to formalize natural-language requirements as LTLf formulas that are syntactically valid, AP-consistent, and semantically faithful.Its neuro-symbolic integration makes candidate behavioral differences explicit through automata operations and uses trace-level differences to guide iterative refinement.Source: §IV · p. 4

A. Key Insights

  • Multiple generators provide diverse candidate formulas, whose differences can contribute complementary semantic insight during refinement.Different candidates may capture different aspects of a requirement, including temporal ordering and edge cases.Source: A. Key Insights · p. 4

B. Approach Overview

  • The framework generates and validates candidate formulas, derives DFA-based differential traces, then turns judgments about behaviors to add or remove into feedback for the next iteration.The loop ends at convergence or when the maximum iteration count is reached.Source: B. Approach Overview · pp. 4–5

C. Candidate LTLf Generation and Validation

Candidate generation uses an atomic-proposition library and validation checks before semantic comparison. The automata-based differencing module turns candidate disagreements into finite witness traces, with trace selection adapted to the domain and budget.

C. Candidate LTLf Generation and Validation

  • Each generator receives the natural-language description, AP library, and iteration feedback; the library grounds informal descriptions in the fixed formal vocabulary available to the formulas.The module outputs syntactically valid, AP-consistent candidates and can use an LLM to construct an AP library when one is unavailable.Source: C. Candidate LTLf Generation and… · p. 5
  • Candidates must pass syntax and AP-membership checks before comparison; failed formulas receive error messages and a fixed number of repair retries.This step removes malformed formulas and AP hallucinations before semantic comparison.Source: C. Candidate LTLf Generation and… · p. 5

D. Automata-Based Differencing

  • The differencing module converts each candidate to a DFA and constructs automata whose traces expose behaviors unique to that candidate or accepted by alternatives but missed by it.Finite accepting paths become concrete witness traces for feedback.Source: D. Automata-Based Differencing · p. 5
  • Trace-generation strategy depends on the trace budget and domain; witnesses may target edge, state, or path coverage, truth-value diversity, or varied atomic-proposition combinations.The goal is to capture as much relevant difference-automaton behavior as possible within the budget.Source: D. Automata-Based Differencing · pp. 5–6

E. Judging and Feedback

NEUROSTAR uses LLM judges to assess concrete trace behaviors against the natural-language specification and turn disagreements into formula-refinement feedback. A convergence checker returns a stable medoid when candidates agree sufficiently, while non-converged candidates receive another refinement round.

E. Judging and Feedback

  • LLM judges assess whether accepted and missing traces match the natural-language specification, using separate panels to decide which behaviors to keep or add.The keep panel uses majority voting; the add panel checks whether missing behaviors align with the specification.Source: E. Judging and Feedback · p. 6
  • Judge decisions yield traces to remove or insert, which define stability scores for each candidate formula.High stability scores indicate that a candidate needs few local modifications.Source: E. Judging and Feedback · p. 6
  • The checker filters candidates by stability, proceeds to another iteration if fewer than three qualify, and otherwise tests whether the medoid is within threshold θ of another stable candidate.It selects the medoid using pairwise bounded-trace Jaccard distances; a converged medoid is returned as the final formula.Source: E. Judging and Feedback · p. 6
  • Semantically equivalent outputs are treated as converged, even though all generators could produce the same wrong formula together.The authors retain this choice because their empirical evaluation found that models were much more likely to be correct together than wrong together.Source: E. Judging and Feedback · pp. 6–7
  • When candidates have not converged, judges’ trace-level decisions and the anonymized full candidate set are sent to each generator as refinement feedback.The full set is included because distinguishing traces alone may not determine a suitable global repair; each round uses a new context window.Source: E. Judging and Feedback · p. 7

V. TECHNIQUE EVALUATION

This section frames the evaluation question as whether NEUROSTAR improves NL-to-LTLf translation relative to existing baseline techniques on established benchmarks.

V. TECHNIQUE EVALUATION

  • The evaluation asks whether NEUROSTAR improves NL-to-LTLf translation performance compared with existing baseline techniques.RQ3 specifically asks how NEUROSTAR performs against baselines on existing benchmarks.Source: §V · p. 7

A. Evaluation Design

The evaluation uses multiple generators and judges, automata-derived witness traces, and filtered and strict versions of four datasets. Trace selection is designed to maximize coverage while keeping the judge prompts small.

A. Evaluation Design

  • NEUROSTAR uses four generators spanning Gemini 3.5 Flash and Kimi K2.5 at two temperatures, with Kimi K2.5 also serving as both judge panels.Generators receive five ADARULE training examples; varying model family and temperature is intended to produce diverse candidates.Source: A. Evaluation Design · p. 7
  • For each candidate, NEUROSTAR derives witness traces from difference DFAs and selects at most five traces to maximize edge coverage over traces of length at most five.The selection is globally optimal over the enumerated trace set, using a mixed-integer linear program; the limits were chosen empirically to balance behavioral coverage and prompt size.Source: A. Evaluation Design · p. 7
  • RQ3 is evaluated on filtered and strict versions of the four datasets described in the evaluation design.Source: A. Evaluation Design · p. 7

B. Baselines

NEUROSTAR compares candidate formula behavior rather than relying only on natural-language patterns, and it performs best or jointly best on most reported benchmark variants. Results also include an exception on synthetic pattern data and an explicit check for valid atomic propositions.

B. Baselines

  • ADARULE retrieves guidelines, LfF retrieves examples, and n-shot prompting uses ordinary few-shot generation; unlike these baselines, NEUROSTAR compares formula behavior.The n-shot baseline uses the same models, temperatures, and number of examples as NEUROSTAR’s generators.Source: B. Baselines · p. 7

C. RQ3 Results

  • NEUROSTAR is best or joint-best on three filtered datasets (CONFONLf 87.8%, SPECNLf 92.9%, LANGNLf 94.1%) and both strict datasets (CONFONLst 96.4%, SYNTHNLst 100%).On CONFONLf, it exceeds n-shot prompting by 1.6 percentage points and ADARULE by 10.2 percentage points.Source: C. RQ3 Results · p. 7
  • ADARULE records the highest SYNTHNLf accuracy at 78.9%, 3.1 percentage points above NEUROSTAR.The paper attributes this result to ADARULE’s ability to memorize SYNTHNL’s eight predefined specification patterns, which transfers poorly to realistic robot-task data.Source: C. RQ3 Results · p. 8
  • ADARULE and LfF sometimes fail to extract correct atomic-proposition names, while NEUROSTAR and n-shot prompting take the proposition library as input.NEUROSTAR also checks proposition validity because an incorrect proposition invalidates the generated formula.Source: C. RQ3 Results · p. 8

VI. PROOF-OF-CONCEPT STUDY

The proof-of-concept study evaluates NEUROSTAR on Virginia driving-code sections without reference formulae, using human assessment of violating traces as a cost-conscious correctness signal. Its design addresses the corpus’s complexity and cross-references while recognizing that this metric does not assess the full set of accepted and rejected traces.

VI. PROOF-OF-CONCEPT STUDY

  • The study focuses on 108 Virginia driving-code sections without ground-truth LTLf formulae, from a corpus written by domain experts and covering a diverse, complex problem domain.Earlier work had identified 114 sections as applicable to autonomous driving and manually specified six; this study examines the remaining 108.Source: A. Evaluation Design · p. 8

A. Evaluation Design

  • The study assesses convergence across iterations by comparing generated formulae with final formulae using semantic differences between automata.Fig. 3 depicts cumulative semantic convergence across iterations.Source: Figure 3 · p. 8
  • Because the laws contain cross-references and longer specifications, the evaluation supplies referenced sections as context and uses six existing LTLf formulae as few-shot examples.The setup uses lC = 10 and b = 10; without reference formulae, comparison with training-dependent approaches such as ADARULE is impossible on this dataset.Source: A. Evaluation Design · p. 8

B. Evaluation Metric

  • The metric was designed as a cost-conscious correctness signal because comparing the structure of long natural-language specifications with LTLf formulae was challenging and time-consuming.The driving-code specifications averaged 273 words, motivating an assessment based on traces.Source: B. Evaluation Metric · p. 8
  • Two authors assess whether a shortest violating trace also violates the law’s intent, with a third rater resolving disagreements by majority decision.Raters are instructed to judge conservatively and call a trace a violation only when sure.Source: B. Evaluation Metric · pp. 8–9
  • Valid-witness assessment does not establish whether the full set of accepted and rejected formula traces matches the natural-language description.The authors describe the metric as an initial assessment and note that additional accepting and rejecting traces could provide further confidence.Source: B. Evaluation Metric · p. 9

C. RQ4 Results

NEUROSTAR captures the necessary temporal semantics in 83.9% of the evaluated VALAW sections, while its iterative outputs converge semantically for 107 laws by iteration eight. The qualitative analysis highlights temporal operators, legal exceptions, vehicle classes, operational conditions, and independent obligations, alongside limitations from missing atomic propositions.

C. RQ4 Results

  • By iteration 8, all 107 converged laws reached semantic equivalence with their final formulae.One of the 107 converged laws was trivially true.Source: C. RQ4 Results · p. 9
  • 89 of 106 violating witnesses were judged valid (83.9%) by a majority of reviewers, excluding one trivially true formula among the 107 converged laws.A valid witness was judged to constitute a violation of the corresponding natural-language specification.Source: C. RQ4 Results · p. 9
  • The § 46.2-829 example uses F for urgency and weak-until for remaining stopped until passage without assuming passage occurs; officer direction conditions the obligation.The figure illustrates a generated formula, with the law’s original description replaced by a summary for readability.Source: C. RQ4 Results · p. 9, Figure 4 · p. 10
  • NEUROSTAR models “unless” and “except” clauses as negated antecedent literals, and uses U for obligations to maintain a state until a condition occurs.Such clauses occur in 22.6% and 30.2% of sections, respectively; reach-and-maintain patterns occur in 11.3%.Source: C. RQ4 Results · p. 9
  • The generated formulae preserve distinctions among vehicle classes and fine-grained roadway conditions, and represent interactions among multiple road users.Examples include emergency vehicles, roadway position, and vehicle-pedestrian interactions.Source: C. RQ4 Results · p. 9
  • NEUROSTAR isolates an operative legal rule from surrounding administrative context and combines independent requirements as globally scoped conjuncts.Examples include a school-zone speed restriction and separate scooter, EPAMD, age, and interstate-highway obligations.Source: C. RQ4 Results · p. 9
  • A gap between needed propositions and the AP library can collapse distinct legal scenarios, thresholds, or place-specific scopes into less detailed formulae.The paper identifies this AP vocabulary gap as the dominant limitation and notes that it can constrain downstream scenario-specific test generation [57].Source: C. RQ4 Results · pp. 9–10
  • 83.9% of the evaluated VALAW sections had their necessary temporal semantics captured by NEUROSTAR.The study reports this as its RQ4 answer despite observed limitations in the AP library.Source: C. RQ4 Results · p. 10

VII. THREATS TO VALIDITY

NEUROSTAR performs strongly on filtered and strict benchmarks and captures necessary temporal semantics in most VALAW laws. The authors also identify implementation, trace-bound, model-choice, and AP-vocabulary limits.

VII. THREATS TO VALIDITY

  • Implementation bugs, parameter choices, dataset-cleaning errors, and VALAW judgment bias threaten validity despite testing, manual review, pilot tuning, and conflict adjudication.Four researchers, including three temporal-logic experts, reviewed cleaned datasets; uncertain witness judgments were assigned V_WV = 0 and conflicts were resolved by a third reviewer.Source: §VII · p. 10
  • Bounded-trace Jaccard comparison risks false convergence with too few traces, while model choice and benchmark simplicity limit result generalizability.The authors select a trace bound where distance stabilizes and evaluate on VALAW to address benchmark-complexity concerns.Source: §VII · p. 10

VIII. CONCLUSION

  • NEUROSTAR combines multiple generators with automata-theoretic reasoning over semantic differences among candidates to guide convergence on a final formula.Source: §VIII · p. 10
  • 89 of 106 Virginia laws had necessary temporal semantics captured, alongside best or joint-best accuracy on three of four filtered datasets and both strict datasets.NEUROSTAR reached 96.4% on CONFONLst and 100% on SYNTHNLst; the analysis removed 48.43% of benchmark data and found the datasets less challenging than real-world requirements.Source: §VIII · p. 10
  • Qualitative analysis finds that NEUROSTAR models each driving law’s operative core together with its temporal, conditional, and agent-specific structure.Source: §VIII · p. 11
  • The AP vocabulary gap is the dominant limitation in driving-law formalization, and improving AP-library construction is proposed as future work.Source: §VIII · p. 11
Loading 2609.03161v1…