ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning

• URL: http://arxiv.org/abs/2605.06483v2
• Date: Fri, 08 May 2026 10:38:45 GMT
• Title: ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning
• Abstract summary: textscReasonSTL is a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation.<n>textscReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction.<n>Experiments show that a 4B model trained with textscReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations.
• Score: 5.961092142323502
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Signal Temporal Logic (STL) is an expressive formal language for specifying spatio-temporal requirements over real-valued, real-time signals. It has been widely used for the verification and synthesis of autonomous systems and cyber-physical systems. In practice, however, users often express their requirements in natural language rather than in structured STL formulas, making natural-language-to-STL translation a critical yet challenging task. Manual specification requires temporal-logic expertise and cannot scale, while prompting commercial LLM APIs incurs substantial token costs and may expose sensitive system requirements to third-party services, raising privacy concerns for industrial deployment. To address these challenges, we present \textsc{ReasonSTL}, a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation. \textsc{ReasonSTL} decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction. We further introduce process-rewarded training to supervise both tool-use trajectories and final formulas, together with \textsc{STL-Bench}, a bilingual, computation-aware benchmark grounded in real-world signals. Experiments show that a 4B model trained with \textsc{ReasonSTL} achieves state-of-the-art performance in both automatic metrics and human evaluations, demonstrating that \textsc{ReasonSTL} provides a transparent, low-cost, and privacy-preserving alternative for formal specification drafting.

Related papers

• When LLMs Develop Languages: Symbolic Communication for Efficient Multi-Agent Reasoning [85.36421257648294]
  Chain-of-Thought (CoT) improves large language models (LLMs) on difficult reasoning tasks.<n>We propose Communicative Language Symbolism Routing (R)<n>R treats each Language Symbolism Framework as a reusable symbolic protocol with compact symbols, usage rules, and a message-passing contract.<n>R reduces latency-oriented generated token completion by $3sim 6times$ compared to standard CoT.
  arXiv  Detail & Related papers  (2026-06-28T12:02:42Z)
• ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification [41.040507019193775]
  Signal Temporal Logic (STL) is a formal language for specifying real-time behaviors of cyber-physical systems.<n>Recent efforts leveraging large language models (LLMs) have demonstrated impressive performance, but some natural language requirements contain vague or ambiguous information.<n>We propose ClarifySTL, an interactive LLM-agent framework that enhances STL transformation through requirements clarification.
  arXiv  Detail & Related papers  (2026-05-02T02:55:06Z)
• LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning [2.365021420497964]
  Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL)<n>In this work, we focus on enabling resource-efficient open-weight models to generate correct temporal logic (LTL) specifications from informal requirements.<n>We presentGuard, a modular toolchain that combines constrained generation with formal consistency checking to generate conflict-free specifications from informal input.
  arXiv  Detail & Related papers  (2026-03-05T22:34:45Z)
• Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs [10.958536923155101]
  Req2LTL is a modular framework that bridges NL and Linear Temporal Logic.<n>It achieves 88.4% semantic accuracy and 100% syntactic correctness on real-world aerospace requirements.
  arXiv  Detail & Related papers  (2025-12-19T08:25:54Z)
• Fine-Tuned Language Models for Domain-Specific Summarization and Tagging [3.543800643014229]
  This paper presents a pipeline integrating fine-tuned large language models (LLMs) with named entity recognition (NER) for efficient domain-specific text summarization and tagging.<n>The authors address the challenge posed by rapidly evolving sub-cultural languages and slang, which complicate automated information extraction and law enforcement monitoring.
  arXiv  Detail & Related papers  (2025-10-29T12:33:48Z)
• Data Dependency-Aware Code Generation from Enhanced UML Sequence Diagrams [54.528185120850274]
  We propose a novel step-by-step code generation framework named API2Dep.<n>First, we introduce an enhanced Unified Modeling Language (UML) API diagram tailored for service-oriented architectures.<n>Second, recognizing the critical role of data flow, we introduce a dedicated data dependency inference task.
  arXiv  Detail & Related papers  (2025-08-05T12:28:23Z)
• The Synergy of LLMs & RL Unlocks Offline Learning of Generalizable Language-Conditioned Policies with Low-fidelity Data [50.544186914115045]
  TEDUO is a novel training pipeline for offline language-conditioned policy learning in symbolic environments.<n>Our approach harnesses large language models (LLMs) in a dual capacity: first, as automatization tools augmenting offline datasets with richer annotations, and second, as generalizable instruction-following agents.
  arXiv  Detail & Related papers  (2024-12-09T18:43:56Z)
• Large Language Models are Interpretable Learners [53.56735770834617]
  In this paper, we show a combination of Large Language Models (LLMs) and symbolic programs can bridge the gap between expressiveness and interpretability. The pretrained LLM with natural language prompts provides a massive set of interpretable modules that can transform raw input into natural language concepts. As the knowledge learned by LSP is a combination of natural language descriptions and symbolic rules, it is easily transferable to humans (interpretable) and other LLMs.
  arXiv  Detail & Related papers  (2024-06-25T02:18:15Z)
• Injecting linguistic knowledge into BERT for Dialogue State Tracking [60.42231674887294]
  This paper proposes a method that extracts linguistic knowledge via an unsupervised framework. We then utilize this knowledge to augment BERT's performance and interpretability in Dialogue State Tracking (DST) tasks. We benchmark this framework on various DST tasks and observe a notable improvement in accuracy.
  arXiv  Detail & Related papers  (2023-11-27T08:38:42Z)
• Simultaneous Machine Translation with Large Language Models [51.470478122113356]
  We investigate the possibility of applying Large Language Models to SimulMT tasks. We conducted experiments using the textttLlama2-7b-chat model on nine different languages from the MUST-C dataset. The results show that LLM outperforms dedicated MT models in terms of BLEU and LAAL metrics.
  arXiv  Detail & Related papers  (2023-09-13T04:06:47Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  We present nl2spec, a framework for applying Large Language Models (LLMs) derive formal specifications from unstructured natural language. We introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization.
  arXiv  Detail & Related papers  (2023-03-08T20:08:53Z)
• Context-Tuning: Learning Contextualized Prompts for Natural Language Generation [52.835877179365525]
  We propose a novel continuous prompting approach, called Context-Tuning, to fine-tuning PLMs for natural language generation. Firstly, the prompts are derived based on the input text, so that they can elicit useful knowledge from PLMs for generation. Secondly, to further enhance the relevance of the generated text to the inputs, we utilize continuous inverse prompting to refine the process of natural language generation.
  arXiv  Detail & Related papers  (2022-01-21T12:35:28Z)
• From English to Signal Temporal Logic [7.6398837478968025]
  We propose DeepSTL, a tool and technique for the translation of informal requirements, given as free English sentences, into Signal Temporal Logic (STL), a formal specification language for cyber-physical systems. A major challenge to devise such a translator is the lack of publicly available informal requirements and formal specifications. In the second step, we use a state-of-the-art transformer-based neural translation technique, to train an accurate attentional translator of English to STL.
  arXiv  Detail & Related papers  (2021-09-21T16:13:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.