ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification

TL;DR

ClarifySTL is an interactive framework that improves the transformation of natural language requirements into STL specifications by actively clarifying vagueness and ambiguity with user feedback.

Contribution

It introduces an interactive LLM-agent system that detects and resolves vagueness and ambiguity in requirements before STL transformation, enhancing accuracy and user collaboration.

Findings

ClarifySTL outperforms baseline methods on benchmarks DeepSTL and STL-DivEn.

The framework effectively detects vagueness and ambiguity in requirements.

Experimental results demonstrate improved accuracy in STL transformation.

Abstract

Signal Temporal Logic (STL) is a formal language for specifying real-time behaviors of cyber-physical systems (CPS). Automatically transforming natural language requirements into STL specifications has received growing attention. Recent efforts leveraging large language models (LLMs) have demonstrated impressive performance, but some natural language requirements in practice contain vague or ambiguous information, which remains challenging for LLMs to handle. To address these challenges, we propose ClarifySTL, an interactive LLM-agent framework that enhances STL transformation through requirements clarification. ClarifySTL first detects vague expressions that indicate underspecified information in a requirement. If any vagueness is detected, it generates targeted clarification queries to guide users in supplementing the requirement until all necessary details are provided. Subsequently, if ClarifySTL detects ambiguities, it formulates focused ambiguity clarification queries and updates the requirements based on user feedback until all ambiguities are resolved. Finally, the requirements with vagueness and ambiguity clarified are transformed into STL specifications using LLMs. This interactive framework ensures that the resulting STL formulas faithfully capture user intent while reducing the burden on the user. We evaluate ClarifySTL on the representative benchmarks DeepSTL and STL-DivEn, as well as our newly introduced AmbiEval benchmark, which is specifically designed to assess the performance of the agents in handling vagueness and ambiguity, including both detection and query generation. The experimental results show that ClarifySTL is effective.