⚡ electrical engineering

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

本文介绍了\textsc{ReasonSTL}，这是一个通过过程奖励学习对本地开源语言模型进行适配的工具增强框架，能够准确且私密地将自然语言需求转化为信号时序逻辑（STL）公式，为手动规范制定和商业 API 提供了一种具有成本效益的替代方案。

原作者： Bowen Ye, Zhijian Li, Junyue Huang, Junkai Ma, Xiang Yin

发布于 2026-05-12

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Bowen Ye, Zhijian Li, Junyue Huang, Junkai Ma, Xiang Yin

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象你是一名工程师，正在设计一辆自动驾驶汽车或一个机械臂。你有一个关于它应如何行为的绝妙构想，但你只能用plain English（普通英语）来描述它，例如：“如果汽车离墙太近，它必须在两秒内停下。”

问题在于，计算机的“大脑”不懂英语。它只懂一种严格、数学化的语言，称为信号时序逻辑（Signal Temporal Logic, STL）。这种语言就像一份超精确的食谱，能精确到毫秒和毫米，告诉机器具体该做什么。

问题所在：
迄今为止，将你的英语句子转化为这种严格的数学食谱曾是一场噩梦。

人工翻译：你需要一位人类专家来翻译。这既缓慢、昂贵，又难以扩展。
询问人工智能（“黑箱”）：你可以请一个强大的商业人工智能（例如基于巨型云端的聊天机器人）来代劳。但这存在风险。你可能会不小心将公司的机密安全规则发送给第三方服务器。此外，每次提问都需要支付高昂费用。
旧有人工智能尝试：以往本地的 AI 模型就像那些只背熟了字母表却不会做数学题的学生。它们会猜测食谱，但只要一个数字出错（例如将“两秒”说成“2.5 秒”），整个结果就会失败。

解决方案：REASONSTL
作者们创建了一个名为REASONSTL的新系统。你可以把它想象成雇佣了一位注重隐私的本地学徒，他遵循一套非常具体的工作流程。这位学徒不只是猜测答案，而是遵循严格的三步流程：

翻译者（推理）：学徒阅读你的英语句子并将其拆解。“好的，‘太近’意味着距离，‘两秒’需要转换为毫秒。”
计算器（工具使用）：学徒不猜测数学计算，而是拿出计算器（一种“工具”）。它拥有用于单位转换（英尺到米）、时间计算和数学运算的特定工具。它必须使用这些工具来确保数字准确。
架构师（构建）：一旦数字经过验证，学徒便使用严格的蓝图（JSON 树结构）构建最终的数学食谱（STL 公式），以确保没有遗漏括号或混淆符号。

他们如何教导这位学徒
他们并没有只在最后告诉学徒“做得好”或“做得差”。他们采用了一种名为**过程奖励学习（Process-Rewarded Learning）**的特殊训练方法。

想象一位老师正在观察学徒工作。如果学徒正确使用了计算器，但随后把房子盖倒了，老师会说：“数学做得好，但建筑盖错了。”
如果学徒试图在不使用计算器的情况下猜测数学结果，老师会立即制止他们。
这确保了学徒学会逐步思考并使用正确的工具，而不仅仅是死记硬背答案。

新测试：STL-BENCH
为了检验这位学徒是否真的出色，团队构建了一个更严苛的新测试，名为STL-BENCH。

它就像一场期末考试，包含现实世界的场景（如航空航天或机器人技术），而不仅仅是虚构的句子。
它是双语的（英语和中文）。
它专门测试学徒能否处理那些“枯燥但关键”的任务：单位转换、数学计算以及理解复杂的时间限制。

结果
团队将他们拥有 40 亿参数的模型（一个“小型”但聪明的本地模型）与巨型商业 AI 模型及其他方法进行了测试。

隐私与成本：由于它在他们自己的计算机上本地运行，因此可以免费重复运行，并保持所有数据隐私。
性能：令人惊讶的是，这位本地学徒在准确性上超越了巨型商业“黑箱”AI 模型。它在算对数学和构建正确结构方面表现更佳。
人工核查：当人类查看结果时，发现本地模型与昂贵的商业模型一样出色。

总而言之
REASONSTL 是一种教导本地 AI 模型将人类安全规则转化为严格计算机代码的新方法。通过迫使 AI 使用计算器和工具来“展示其解题过程”，并通过训练使其在每一步都保持谨慎，他们创造了一个隐私安全、成本低廉且意外精准的系统，使其成为向大型云公司发送敏感数据的安全替代方案。

技术摘要：REASONSTL

问题陈述

信号时序逻辑（STL）是一种形式化语言，对于在信息物理系统（CPS）和自主系统中指定实值信号上的时空需求至关重要。虽然 STL 支持严格的验证与合成，但从业者通常使用自然语言（NL）来表达需求。将这些自然语言描述转换为可执行的 STL 公式是一个关键瓶颈。

现有方法面临显著局限：

人工规范：需要专家知识，劳动密集，且无法扩展。
商业大语言模型（LLM）API：虽然具备能力，但会产生高昂的令牌成本，并将敏感的系统需求传输给第三方，引发隐私担忧。
先前的自动化方法：
- DeepSTL 依赖从头训练的神经机器翻译，限制了泛化能力。
- KGST 使用涉及专有 API 的混合流程，存在隐私和成本问题。
- RESTL 在本地运行，但直接生成公式而缺乏中间推理，损害了可解释性和正确性。
技术挑战：自然语言到 STL 的转换不仅需要语法有效性，还需要语义 grounding、计算感知推理（例如单位转换、算术运算）以及对时间区间和特定领域信号的精确处理。阈值或运算符中的微小错误可能导致语义错误。

方法论：REASONSTL

作者提出了 REASONSTL，这是一个专为计算感知型自然语言到 STL 生成设计的本地化、工具增强型框架。其核心理念是将转换过程分解为显式推理、确定性工具调用和结构化公式构建，而不是依赖单步序列预测。

1. 工具增强型生成

模型不生成原始文本，而是生成一个结构化的展开过程，包含推理片段、工具调用和工具输出，最终形成结构化的 STL JSON 树。

工具集：该框架利用一套紧凑的、类型化的确定性工具：
- parse_duration：规范化时间表达式（例如，"30 minutes" $\to$ 1800）。
- convert_unit：转换物理单位（例如，ft $\to$ m）。
- eval_math_expr：计算阈值的算术表达式。
- calc_time_diff：根据时间戳计算时间差。
解耦：该设计将语言解释和结构推理与精确数值计算分离，使过程可检查和可验证。

2. 结果有界的过程奖励优化

REASONSTL 引入了一种新颖的训练策略，同时监督中间工具使用轨迹和最终公式构建。

过程奖励：中间阶段（工具调用、推理）根据局部正确性（参数有效性、可执行性、一致性）分配奖励。
结果有界：关键在于，中间奖励受最终 STL 公式正确性的上限约束。如果最终公式不正确，中间步骤可获得的最大奖励将降低。这防止模型强化那些看似合理但语义无效、最终导致错误结果的推理轨迹。
前缀掩码：如果中间步骤失败，后续依赖阶段将被屏蔽以阻止反向更新，确保模型学会尽早停止或纠正错误。
优化：该框架使用组相对策略目标（类似于 PPO 但不进行似然比截断），基于这些有界奖励来优化模型。

3. STL-BENCH：一个新基准

为了评估计算感知型自然语言到 STL 的生成，作者引入了 STL-BENCH，这是一个基于真实世界 CPS 信号的双语（英语/中文）基准。

特性：涵盖 6 个工程领域、33 个场景和 41 个基于领域的信号变量。
复杂度：73% 的样本需要中间计算（工具使用）。它包含针对工具使用轨迹、时间归一化和单位转换的显式标注。
结构：STL 公式表示为 JSON 树，以支持模式验证和递归结构匹配，超越了简单的字符串匹配。
验证：该数据集通过模板锚定生成、基于规则的验证和分层人工审计构建，以确保高质量标签。

主要贡献

本地工具增强型框架：REASONSTL 是一个本地化、开源的框架，通过多步推理和确定性工具调用将自然语言转换为 STL，显式处理时间归一化、单位转换和算术求值。
结果有界的过程监督：一种训练策略，联合监督中间工具使用轨迹和最终公式构建，通过将中间奖励与最终正确性绑定，降低了强化无效推理路径的风险。
计算感知型基准（STL-BENCH）：一个双语基准，包含基于领域的信号、物理单位、算术约束和显式的工具使用标注，支持对计算感知型生成的严格评估。

实验结果

实验在已建立的 DeepSTL 基准和新的 STL-BENCH 上进行。

DeepSTL 上的表现：使用 REASONSTL-DIRECT（一种直接生成变体）训练的 4B 参数模型（Qwen3-4B）实现了 81.43% 的公式准确率和 82.57% 的格式准确率。这比最强的黑盒 API 基线（Claude-Opus-4.7）高出 15 个百分点以上，并比之前的最先进方法（RESTL）提高了约 21 个百分点。
STL-BENCH 上的表现：
- 完整的 REASONSTL 模型（包含推理和工具）在英语上实现了 51.0% 的公式准确率，在中文上实现了 47.0%，优于基础模型和精心提示的 API 基线（例如 GPT-5.4, Kimi-K2.6）。
- 人工验证：在每种语言 100 个样本的子集上，REASONSTL 的表现达到或超过了专有模型，英语准确率为 53%，中文为 51%。
- 泛化能力：在人工编写、无模板的测试集上，REASONSTL 实现了最高的公式准确率（54%），略优于强大的 API 基线，同时保持了比某些商业模型更高的推理吞吐量。
消融研究：结果证实，虽然监督微调（SFT）有助于格式初始化，但带有过程奖励和工具增强推理的强化学习（RL）是性能提升的主要驱动力。

意义与主张

该论文声称，REASONSTL 提供了一种透明、低成本且保护隐私的形式化规范起草替代方案。通过保持整个流程本地化和开源，它解决了商业大语言模型 API 相关的隐私和成本障碍。

作者强调，该框架将任务分解为确定性计算和结构化推理的能力，使得生成过程可检查且易于验证，这是安全关键型 CPS 应用的关键特征。虽然该系统达到了最先进性能，但作者谦逊地指出，它目前最适合作为人机回环的起草助手，而非专家规范设计的完全自主替代品，特别是在安全关键背景下，残留的语义错误必须由领域专家审查。