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

信号时序逻辑（STL）常用于自主系统验证，但用户多以自然语言表达需求，导致翻译困难。现有方法依赖专家或高成本 API，存在隐私风险。本文提出 ReasonSTL，一种工具增强框架，适配本地开源模型进行自然语言到 STL 的生成。该框架将翻译分解为显式推理、确定性工具调用和结构化公式构建，并引入过程奖励训练监督工具使用轨迹及最终公式。实验表明，经训练的 4B 模型在自动指标与人工评估中均达最先进水平，提供了透明、低成本且保护隐私的形式化规范起草方案。