PaperlayerView exact revision on arXiv

Source-linked AI summary

Feedback Makes Perfect: A Closed-Loop Framework for NL-to-STL Translation

Bowen Ye, Xiang Yin

arXiv:2609.33287v1cs.AIcs.ROcs.SYeess.SY

TL;DR

Natural-language requirements can be ambiguous or omit the author’s intent, making one-shot NL-to-STL translation ill-defined. The paper introduces a closed-loop process in which users check natural-language renderings of generated formulas and correct them. It reports improved closed-loop accuracy, with gains varying by model capability.

  • Problem

    One-shot NL-to-STL translation is ill-defined because requirements can be ambiguous or fail to express the author’s intent.

    Source: §1 · p. 2

  • Method

    The framework renders each generated STL formula into natural language for user checking and uses natural-language corrections to revise the specification.

    Source: §1 · p. 2, §4.1 · p. 5

  • Results

    Closed-loop refinement raises strong models to 98.0–99.2% accuracy, while Qwen2.5-3B-Instruct improves from 17.6% to 48.0%.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The results support semantic feedback as an alignment layer between human intent and machine-executable formal artifacts.

    Source: §6 · p. 9

    User acceptance depends on faithful back-translation and does not formally prove that a specification is equivalent to the intended requirement.

    Source: §4.2 · p. 6

Abstract

from arXiv · show

Signal Temporal Logic (STL) enables rigorous verification and control of cyber-physical systems, but writing correct specifications requires expertise that most requirement holders lack. Large language models can translate natural-language (NL) requirements into STL, yet stronger translators alone approach an accuracy ceiling. We argue that this ceiling stems from how the task is posed: one-shot, open-loop translation is somewhat ill-defined. Natural language is ambiguous, and, more fundamentally, what a person writes may not always be what they intend, so the target specification is not fully contained in the input text. We therefore reformulate NL-to-STL translation as a closed-loop feedback process. Each generated formula is translated back into natural language for the user to check, and natural-language corrections drive revision until the user accepts the specification. Users never read or write formal syntax. This framework rests on an asymmetry familiar from feedback control theory. The forward path, from ambiguous language to formal logic, is hard and error-prone. The feedback path, from structured STL back to language, can be made highly precise, and a precise feedback path lets an imprecise forward path achieve precise closed-loop behavior. Experiments on 500 expert-authored requirements and seven LLMs support this view. Back-translated explanations agree with expert judgments in 99.5\% of cases. Closed-loop refinement raises strong models from about 89\% open-loop accuracy to 98.0--99.2\%, and yields gains of over 30 percentage points for weaker models (e.g., 17.6\%$\rightarrow$48.0\%). Ablations show these gains come from the semantic content of the feedback rather than from repeated attempts. An expert audit and a 280-session user study further confirm the reliability of the loop. We also identify a capability threshold above which feedback no longer helps.

1 INTRODUCTION

The paper argues that one-shot NL-to-STL translation cannot reliably recover intent that is ambiguous or absent from the written requirement. It proposes a natural-language feedback loop that lets users check and correct generated specifications, reporting improved accuracy while identifying a model-capability boundary.

1 INTRODUCTION

  • One-shot translation is ill-defined because language is ambiguous and written requirements may omit or misstate the author’s intent.The target specification may therefore contain information that cannot be recovered from the input text alone.Source: §1 · p. 2
  • The framework repeatedly generates an STL formula, renders its meaning in natural language, and revises it using the user’s natural-language corrections.Users interact only in natural language, while STL remains in the machine layer.Source: §1 · p. 2
  • 98.0–99.2% closed-loop accuracy is reported for strong models, while Qwen2.5-3B-Instruct rises from 17.6% to 48.0%.Back-translated explanations agree with expert judgments in 99.5% of cases; Qwen2.5-0.5B-Instruct improves only from 6.8% to 7.8%.Source: §1 · p. 2
  • A precise STL-to-language feedback path can compensate for an error-prone language-to-STL path, but feedback cannot rescue a translator too weak to act on corrections.The experiments cover 500 expert-authored requirements, seven LLMs, feedback ablations, an expert audit, and a 280-session user study.Source: §1 · p. 2

2 RELATED WORK

Prior work improves temporal-logic translation, clarifies requirements, or refines and verifies LLM outputs. This paper positions its contribution as checking generated specifications against user intent after generation and before downstream formal reasoning.

Natural-Language-to-Temporal-Logic Translation

  • Prior NL-to-temporal-logic work strengthens translation, while this paper studies alignment with intent across successive requirement revisions.The authors distinguish translator accuracy from intent alignment.Source: §2 · p. 3

Interactive Requirement Clarification and Specification Refinement

  • Interactive clarification methods resolve underspecification before translation, but cannot catch a well-defined requirement translated into an incorrect formula.The paper instead validates the semantics of a complete generated specification without requiring users to reason about temporal-logic fragments.Source: §2 · p. 3

Reliability Assessment and Feedback-based Refinement of LLM Outputs

  • Existing feedback and verification methods target output quality or confidence, whereas formal specification synthesis requires checking whether the artifact preserves intended meaning.The paper frames semantic agreement with human intent as the relevant correctness criterion.Source: §2 · p. 3

Interactive Requirement Clarification and Specification Refinement

  • The framework adds semantic validation after specification generation, connecting human intent, generated specifications, and subsequent formal analysis.It complements rather than replaces existing translation or verification techniques.Source: §2 · pp. 3–4

3 PRELIMINARIES

The preliminaries define STL over real-valued signals and frame translation as preserving intended meaning across intent, language, and formal representation. They distinguish semantic alignment from syntactic matching and note that requirements may omit information needed for a unique specification.

3.1 SIGNAL TEMPORAL LOGIC

  • STL formulas combine real-valued predicates, Boolean connectives, and temporal operators over explicit intervals.The paper considers future-time STL with bounded or explicitly specified intervals and represents formulas as structured syntax trees.Source: §3.1 · p. 4
  • The satisfaction relation checks whether a signal satisfies a formula; globally, eventually, and until operators specify temporal conditions over intervals.STL also assigns quantitative robustness values indicating the degree of satisfaction or violation.Source: §3.1 · p. 4

3.2 NL-TO-STL TRANSLATION

  • NL-to-STL translation maps a natural-language requirement to a formula whose semantics should represent the underlying intent.The formulation distinguishes latent intent, its linguistic description, and the resulting formal representation.Source: §3.2 · p. 4
  • Correctness depends on semantic alignment rather than exact formula matching, while requirements may omit thresholds, temporal bounds, or triggering conditions.Completing such requirements may require assumptions, so a formula can reflect translator-introduced assumptions rather than information in the original text.Source: §3.2 · pp. 4–5

4 CLOSED-LOOP SEMANTIC ACCEPTANCE FRAMEWORK

The framework repeatedly turns a user’s utterance into a candidate STL formula, renders the formula’s semantics in natural language, and lets the user accept or revise it. Revisions can clarify incomplete requirements or correct translation errors, but user acceptance is not a formal proof of equivalence.

4.1 ITERATIVE CONTEXT UPDATE AND SEMANTIC OBSERVATION

  • Each round incorporates the user’s utterance and prior artifacts into an updated context, generates a candidate STL formula, and renders it back into natural language.The same update rule processes the initial requirement and later revisions.Source: §4.1 · p. 5
  • NL feedback restates the candidate formula’s semantics, including its predicates, quantitative parameters, temporal intervals, and logical relationships.Thresholds and time bounds are derived from the formula, so users can check the candidate without inspecting STL syntax.Source: §4.1 · p. 5

4.2 USER VERIFICATION AND REQUIREMENT REFINEMENT

  • Users accept a candidate or revise it with a new utterance that can clarify missing details, correct a revealed misinterpretation, or add a constraint.Acceptance relies on the user’s assessment of the NL feedback; it does not formally prove equivalence to the intended requirement.Source: §4.2 · pp. 5–6

4.3 CLOSED-LOOP ACCEPTANCE PROTOCOL

  • The protocol repeats context update, translation, back-translation, and user verification until acceptance or exhaustion of the round budget.A projector example is corrected from eventual closure to continuous closure and accepted after two rounds.Source: §4.3 · p. 6
  • With a compositional requirement, ten rounds corrected the stationarity clause but left pickup, delivery, and speed constraints missing, so the protocol returned unresolved.The trace shows that feedback exposed the missing conjuncts, but repeated targeted revisions did not recover the full temporal composition.Source: §4.3 · p. 7

5 EXPERIMENTS

The experiments compare one-shot translation with iterative semantic refinement across seven LLMs and assess accuracy, feedback effects, and acceptance reliability. Refinement improves accuracy, with gains depending on model capability and semantic feedback, while human evaluations test the reliability of acceptance decisions.

5.1 EXPERIMENTAL SETUP

  • The benchmark contains 500 expert-authored requirements across four domains, and evaluation compares one-shot translation with up to 10 rounds of semantic refinement.The benchmark includes 335 well-specified requirements, 122 translation-error cases, and 43 underspecified requirements; closed-loop evaluation uses an LLM judge except in designated human-in-the-loop experiments.Source: §5.1 · p. 7, §5.2 · p. 7

5.2 SEMANTIC FEEDBACK IMPROVES SPECIFICATION FIDELITY

  • For the four higher-performing models, closed-loop accuracy reaches 98.0–99.2%, with mean feedback below 0.5 events per sample.Across all evaluated models, closed-loop accuracy exceeds open-loop accuracy by 1.0–30.8 percentage points; Table 1 reports the comparison.Source: §5.2 · p. 8, Table 1 · p. 8

5.3 UNDERSTANDING THE ROLE OF SEMANTIC FEEDBACK

  • With refinement procedures unchanged and only feedback specificity differing, informative feedback raises accuracy by 9.6–26.5 percentage points over generic retry instructions; Qwen2.5-0.5B-Instruct rises only 6.8% to 7.8%.Aggregate translation rounds per accepted specification were approximately 1.2 for the highest-performing models and 119.7 for Qwen2.5-0.5B-Instruct.Source: §5.3 · pp. 8–9

5.4 RELIABILITY OF THE SEMANTIC ACCEPTANCE LOOP

  • Back-translation agrees with expert labels in 398/400 cases (99.5%), and expert review finds 99.2% precision among specifications accepted by the complete framework.Experts confirm 629 of 634 accepted specifications as semantically correct; Table 2 reports the reliability evaluation.Source: §5.4 · p. 9, Table 2 · p. 9
  • In 280 real-user sessions, participants accept 202 specifications (72.1%) within the 10-round budget after providing 730 subsequent feedback inputs.Among the three larger models, user acceptance ranges from 92.5–97.5%, with 0.35–1.20 additional NL inputs per sample; Table 2 includes the user evaluation.Source: §5.4 · p. 9, Table 2 · p. 9

6 CONCLUSION

The conclusion frames NL-to-STL translation as a semantic-alignment problem rather than merely one-shot generation. The proposed feedback loop lets people validate and refine specifications in natural language before downstream formal reasoning.

6 CONCLUSION

  • The framework reframes NL-to-STL translation around semantic alignment between human intent and formal specifications.The paper argues that a written requirement may not faithfully represent its author's intent, and that one-shot translation is therefore ill-posed.Source: §6 · p. 9
  • Natural-language interaction lets generated specifications be validated and refined before downstream formal reasoning.The paper distinguishes correctness with respect to a specification from whether that specification reflects its author's intent.Source: §6 · p. 9
  • The results support semantic feedback as an alignment layer for machine-executable formal artifacts, with benefits shaped by feedback quality and model capability.Source: §6 · p. 9

A BENCHMARK CONSTRUCTION

The benchmark pairs expert-authored NL requirements with STL specifications and annotations that distinguish incomplete inputs from mistranslations. Its expert review and controlled cases support diagnosis of both feedback paths, rather than maximizing corpus size.

A BENCHMARK CONSTRUCTION

  • The benchmark covers ADAS, Drone, smart-home, and AGV requirements, with five domain experts writing them and two independently covering AGV.The distribution was fixed before sampling; the larger AGV share reflects its two annotators, while the other domains remain within 5.2 percentage points of one another.Source: A BENCHMARK CONSTRUCTION · p. 12
  • The retained set contains 3,556 requirements: 1,455 simple, 1,640 medium, and 461 hard cases.Of these, 1,100 are annotated as formula errors or underspecified requirements, including 402 minimal contrastive pairs.Source: A BENCHMARK CONSTRUCTION · p. 12
  • The benchmark combines formula-level errors, missing input information, localized explanations, corrected targets, and controlled minimal pairs in one diagnostic corpus.Its expert-written and cross-reviewed annotations support evaluation of both feedback paths, while limiting scale relative to larger translation corpora.Source: A BENCHMARK CONSTRUCTION · p. 12
  • Experts separately judged input sufficiency and checked the STL, keeping underspecification distinct from translation error.Cross-review raised 123 substantive objections; adjudication revised and retained 120 cases and removed three without agreement.Source: A BENCHMARK CONSTRUCTION · p. 12
  • The 81-case Nested subset tests temporal anchoring, operator scope, event–state distinctions, nested implication, and dependencies across temporal windows.These cases target structural alignment beyond lexical overlap.Source: A BENCHMARK CONSTRUCTION · p. 12
  • The main evaluation uses the same random sample of 500 cases for every translator and condition: 335 well-specified, 122 translation-error, and 43 underspecified cases.Thus, one third requires output correction or input clarification.Source: A BENCHMARK CONSTRUCTION · p. 12

B SYSTEM IMPLEMENTATION AND COMPONENT VALIDATION

The system iteratively translates requirements into STL, renders each candidate’s semantics in natural language, and uses acceptance or localized feedback to guide revision. Its back-translation acceptance interface is highly accurate, though comparison with direct judges uses separate evaluation sets.

B SYSTEM IMPLEMENTATION AND COMPONENT VALIDATION

  • The loop generates an STL candidate, renders its semantics in natural language, and returns a decision plus a localized discrepancy that can guide the next round.It ends at acceptance, budget exhaustion, or system failure, with a budget of 10 rounds.Source: B SYSTEM IMPLEMENTATION AND COMPONENT… · p. 13
  • For underspecified inputs, the system requests the smallest needed clarification; for translation errors, it identifies the semantic discrepancy without revealing the reference STL.The reference formula is withheld from the translators, acceptance mechanism, and simulated user, and used only for external assessment.Source: B SYSTEM IMPLEMENTATION AND COMPONENT… · pp. 13–14
  • Back-translation reads only the candidate formula and preserves predicates, thresholds, Boolean dependencies, temporal intervals, implication structure, and temporal scope.Restricting its input prevents the rendering from silently repairing the candidate.Source: B SYSTEM IMPLEMENTATION AND COMPONENT… · p. 13
  • The acceptance interface matches expert accept/reject judgments in 398/400 cases, or 99.5%.It correctly identifies 248 of 249 matches and 150 of 151 mismatches; a mechanical rule layer resolves 92 cases without an API call.Source: B SYSTEM IMPLEMENTATION AND COMPONENT… · p. 15
  • The interface’s two calibration errors are one false rejection after unit normalization and one false acceptance involving unresolved conjunction-disjunction scope.Both errors fall in AGV, where accuracy is 97.5%; the panel makes no errors on ADAS, Drone, Smart Home, or Nested calibration cases.Source: B SYSTEM IMPLEMENTATION AND COMPONENT… · p. 15
  • The back-translation interface obtains 81/81 recall on positive Nested cases, versus 33.3% and 77.3% for two direct judges.The protocols use separate evaluation sets and panel aggregation, so the observed gap cannot be attributed to structured rendering alone.Source: B SYSTEM IMPLEMENTATION AND COMPONENT… · p. 15

C DOMAIN-WISE RESULTS AND NESTED ANALYSIS

Closed-loop refinement yields non-monotonic gains across models, with the largest gains for 3B and 7B translators and high accuracy for stronger models. Results also show that feedback quality and temporal structure matter to performance.

C DOMAIN-WISE RESULTS AND NESTED ANALYSIS

  • 30.4 and 30.8 percentage points are the largest measured gains, for the 3B and 7B models; four higher-performing models reach 98.0–99.2% closed-loop accuracy.Those four models use 0.19–0.41 feedback messages per case, while the 0.5B model improves by 1.0 percentage point despite frequent feedback.Source: C DOMAIN-WISE RESULTS AND NESTED… · p. 15, Table 8 · p. 16
  • All four larger models receive operational acceptance on every ADAS and AGV case; Nested cases are the only unresolved category shared by all four.Their remaining non-Nested unresolved sessions occur in Drone and Smart Home.Source: C DOMAIN-WISE RESULTS AND NESTED… · pp. 15–16
  • On the 81-instance Nested subset, accuracy falls 0.4–6.6 percentage points from corresponding 500-case results; the best result is 80 of 81 cases.Residual failures mainly involve temporal anchoring, operator scope, event–state confusion, and dependencies across nested windows.Source: Table 7 · p. 15, C DOMAIN-WISE RESULTS AND NESTED… · p. 16
  • A generic retry instruction yields lower accuracy than localized feedback in all four conditions, with differences of 26.5 and 26.0 points for the 3B and 7B models and 10.0 and 9.6 for two larger models.This ablation uses a dedicated subset, so its values are not interchangeable with the 500-case main results.Source: C DOMAIN-WISE RESULTS AND NESTED… · p. 16, Table 9 · p. 16
  • For Qwen2.5-7B, injected acceptance noise raises apparent convergence to 92.0% as semantic accuracy falls from 76.0% to 62.5%.The loss is larger for the 3B and 7B translators (7.0 and 13.5 points) than for the two stronger models (2.0 and 2.1 points).Source: C DOMAIN-WISE RESULTS AND NESTED… · p. 16

D HUMAN EVALUATION AND INTERACTION CASES

The expert audit found 99.2% acceptance precision among automatically accepted outputs, while participants accepted 72.1% of 280 model–requirement sessions. Interaction traces show both successful repairs and unresolved errors, including failures in translation and back-translation.

D HUMAN EVALUATION AND INTERACTION CASES

  • 99.2% acceptance precision was confirmed across 629 of 634 automatically accepted outputs, with five false acceptances.The Wilson 95% confidence interval was [98.2%, 99.7%].Source: D HUMAN EVALUATION AND INTERACTION CASES · pp. 16–17, Table 11 · p. 17
  • 72.1% of 280 human model–requirement sessions ended in participant acceptance, after 730 feedback messages informed subsequent attempts.Participants supplied 1,010 natural-language inputs in total, including 280 initial requirements.Source: D HUMAN EVALUATION AND INTERACTION CASES · p. 17, Table 12 · p. 17
  • The 72.1% participant acceptance rate measures reaching an acceptable specification within the interaction budget, unlike 99.2% precision among automatically accepted outputs.Across 40 shared requirements, four larger models accepted 154 of 160 sessions with 102 feedback messages; the 0.5B model accepted 3 of 40 and required 297.Source: D HUMAN EVALUATION AND INTERACTION CASES · p. 17
  • The shared-requirement comparison supports broad trends but does not establish a fine-grained ranking among larger models.The representative traces complement two earlier traces and report operational acceptance decisions; independent correctness is assessed separately by the expert audit.Source: D HUMAN EVALUATION AND INTERACTION CASES · p. 18
  • Traces show feedback correcting connective, temporal-anchoring, trigger–response, reach-and-maintain, and multi-clause errors, sometimes requiring several rounds.Examples include changing a brake conjunction to a disjunction after six revisions and sequencing altitude attainment with maintenance using Until.Source: D HUMAN EVALUATION AND INTERACTION CASES · pp. 18–21
  • Some errors persisted through ten rounds: a 0.5B translator retained an incorrect unbounded interval despite repeated corrections.Other traces report temporal-anchoring plateaus and an absent implication after repeated targeted corrections.Source: D HUMAN EVALUATION AND INTERACTION CASES · pp. 18–20
  • A semantically correct formula remained unresolved when back-translation rendered greater-than as “not equal to,” while audit cases also exposed unit and Boolean-scope mismatches.The audit conditions on automatic acceptance, so it estimates acceptance precision rather than agreement on an arbitrary sample.Source: D HUMAN EVALUATION AND INTERACTION CASES · pp. 17, 21

E LIMITATIONS

The results characterize seven evaluated translators under a ten-round budget, not a model-independent capability threshold. Deployment also depends on grounding predicates in sensing, representations, thresholds, identity, and environmental variation.

E LIMITATIONS

  • The seven evaluated translators and ten-round budget do not establish a model-independent capability threshold.Refinement gains depend on the translator’s observed ability to incorporate feedback; the 0.5B model gains only 1.0 percentage point, and full-formula regeneration can alter previously correct subformulas.Source: E LIMITATIONS · p. 21
  • Predicate deployment requires grounding choices for sensing, representation, thresholds, object identity, and environmental variation.External validity is also limited to STL, four cyber-physical-system domains, and 280 human-interaction sessions.Source: E LIMITATIONS · p. 21

F FUTURE DIRECTIONS AND EXTENSIONS

The authors propose studying whether semantic observation and discrepancy-driven refinement extend to other executable formal languages, but do not evaluate that hypothesis. They also identify combining semantic acceptance with verification, monitoring, and synthesis as future work.

F FUTURE DIRECTIONS AND EXTENSIONS

  • Extending semantic observation and discrepancy-driven refinement beyond STL is a hypothesis, not an evaluated result.Proposed targets include linear temporal logics, planning specifications, program contracts, and workflow descriptions, each requiring language-specific observation and calibrated acceptance criteria.Source: F FUTURE DIRECTIONS AND EXTENSIONS · p. 22
  • Combining semantic acceptance with formal verification, runtime monitoring, and controller synthesis remains future work.The proposed additional feedback signals include counterexamples, execution traces, and behavioral trajectories.Source: F FUTURE DIRECTIONS AND EXTENSIONS · p. 22
Loading 2609.33287v1…