ReasonSTL: 도구 기반 강화 학습을 통한 자연어와 시그널 템포럴 로직 간의 연결

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

시그널 템포럴 로직(STL)은 실시간 신호에 대한 시공간적 요구 사항을 명시하기 위한 강력한 형식 언어이며, 자율 시스템 및 사이버-물리 시스템의 검증 및 합성에 널리 사용됩니다. 그러나 실제로는 사용자들이 구조화된 STL 수식이 아닌 자연어로 요구 사항을 표현하는 경우가 많으므로, 자연어-STL 번역은 매우 중요하면서도 어려운 과제입니다. 수동 명시는 시간 논리에 대한 전문 지식이 필요하며 확장성이 떨어지고, 상업용 LLM API를 사용하는 경우 상당한 토큰 비용이 발생하고 민감한 시스템 요구 사항이 타사 서비스에 노출되어 산업 환경에서의 개인 정보 보호 문제가 발생할 수 있습니다. 이러한 문제점을 해결하기 위해, 우리는 로컬 오픈 소스 언어 모델을 활용하여 자연어에서 STL을 생성하는 도구 기반 프레임워크인 ReasonSTL을 제안합니다. ReasonSTL은 번역 과정을 명시적인 추론, 결정적인 도구 호출 및 구조화된 수식 구성으로 분해합니다. 또한, 도구 사용 경로와 최종 수식을 모두 감독하기 위해 프로세스 기반 보상 학습을 도입했으며, 실제 신호에 기반한 양방향, 계산 성능을 고려한 벤치마크인 STL-Bench를 함께 제공합니다. 실험 결과, ReasonSTL로 학습된 40억 개의 파라미터 모델은 자동 평가 지표 및 인간 평가 모두에서 최고 성능을 달성했으며, 이는 ReasonSTL이 형식 명세 초안 작성에 대한 투명하고 저렴하며 개인 정보 보호 기능을 갖춘 대안을 제공함을 보여줍니다.

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.