Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge

TL;DR

This paper introduces a large, diverse NL-STL dataset and a novel knowledge-guided framework for transforming natural language into Signal Temporal Logic, improving accuracy and diversity over existing methods.

Contribution

The paper presents STL-DivEn, a large diverse NL-STL dataset, and KGST, a knowledge-guided transformation framework leveraging external knowledge and a generate-then-refine process.

Findings

STL-DivEn dataset is more diverse than existing datasets.

KGST outperforms baseline models in transformation accuracy.

Both metric and human evaluations confirm the effectiveness of KGST.

Abstract

Temporal Logic (TL), especially Signal Temporal Logic (STL), enables precise formal specification, making it widely used in cyber-physical systems such as autonomous driving and robotics. Automatically transforming NL into STL is an attractive approach to overcome the limitations of manual transformation, which is time-consuming and error-prone. However, due to the lack of datasets, automatic transformation currently faces significant challenges and has not been fully explored. In this paper, we propose an NL-STL dataset named STL-Diversity-Enhanced (STL-DivEn), which comprises 16,000 samples enriched with diverse patterns. To develop the dataset, we first manually create a small-scale seed set of NL-STL pairs. Next, representative examples are identified through clustering and used to guide large language models (LLMs) in generating additional NL-STL pairs. Finally, diversity and accuracy are ensured through rigorous rule-based filters and human validation. Furthermore, we introduce the Knowledge-Guided STL Transformation (KGST) framework, a novel approach for transforming natural language into STL, involving a generate-then-refine process based on external knowledge. Statistical analysis shows that the STL-DivEn dataset exhibits more diversity than the existing NL-STL dataset. Moreover, both metric-based and human evaluations indicate that our KGST approach outperforms baseline models in transformation accuracy on STL-DivEn and DeepSTL datasets.