ReasonSTL：经工具增强过程奖励学习桥接自然语言与信号时序逻辑

信号时态逻辑 (STL) 是一种表达形式语言，用于指定实值实时信号的时空要求。它已广泛用于自主系统和信息物理系统的验证和综合。然而，在实践中，用户经常使用自然语言而不是结构化的 STL 公式来表达他们的需求，这使得自然语言到 STL 的翻译成为一项关键但具有挑战性的任务。手动规范需要时间逻辑专业知识并且无法扩展，同时促使商业 LLM API 产生大量的token成本，并且可能会将敏感的系统要求暴露给第三方服务，从而引发工业部署的隐私问题。为了应对这些挑战，我们提出了 \textsc{ReasonSTL}，这是一个工具增强框架，它采用本地开源语言模型来生成自然语言到 STL。 \textsc{ReasonSTL} 将翻译过程分解为显式推理、确定性工具调用和结构化公式构造。我们进一步引入过程奖励训练来监督工具使用轨迹和最终公式，以及 \textsc{STL-Bench}，这是一种基于现实世界信号的双语、计算感知基准。实验表明，使用 \textsc{ReasonSTL} 训练的 4B 模型在自动指标和人工评估方面均实现了最先进的性能，这表明 \textsc{ReasonSTL} 为正式规范起草提供了透明、低成本且保护隐私的替代方案。