跳转至

SCP-NL2TL：结合语义验证与选择性保形预测的自然语言转时序逻辑规范框架

文章背景与核心概要

将自然语言指令转化为机器可解释的形式化规范，对于实现自主系统和机器人的行为规划、推理及形式化验证至关重要。然而，标准的翻译模型往往在结果不可靠或误解用户意图时仍盲目生成规范，这在安全关键领域会带来严重风险。

本文引入了 SCP-NL2TL 这一选择性翻译框架，利用选择性保形预测（selective conformal prediction）和语义验证来评估生成的规范何时可以被可靠信赖。该框架通过采用互补的黑盒信号（反向翻译保真度和翻译离散度）、保形风险控制（conformal risk control）以及分布外指令异常检测器，成功将错误执行降至最低。在 信号时序逻辑（STL）、线性时序逻辑（LTL） 和 几何时空逻辑（SpaTiaL） 上的广泛实验表明，该方法显著提升了翻译的可靠性与鲁棒性。

Translating natural language instructions into machine-interpretable formal specifications is vital for enabling autonomous systems and robots to plan, reason, and formally verify their behavior. However, standard translation models often generate specifications even when they are unreliable or misinterpret user intent—posing severe risks in safety-critical domains.

This paper introduces SCP-NL2TL, a selective translation framework utilizing selective conformal prediction and semantic verification to assess when generated formal specifications can be reliably trusted. By employing complementary black-box signals (back-translation fidelity and translation dispersion), conformal risk control, and an out-of-distribution instruction anomaly detector, the framework successfully minimizes incorrect executions. Extensive experiments across Signal Temporal Logic (STL), Linear Temporal Logic (LTL), and geometric Spatio-Temporal Logic (SpaTiaL) demonstrate marked improvements in translation reliability and robustness.

📌 元数据 (Metadata)

👥 作者 (Authors)

  • Yixuan Wang
  • Licheng Luo
  • Yu Fu
  • Kaidi Xu
  • Yue Dong
  • Mingyu Cai
  • Yixuan Wang
  • Licheng Luo
  • Yu Fu
  • Kaidi Xu
  • Yue Dong
  • Mingyu Cai

📄 摘要 (Abstract)

将自然语言指令翻译成机器可解释的形式化规范，使机器人和自主系统能够规划、推理并对其行为进行形式化验证。然而，现有的翻译模型通常会为每个输入生成规范，即使结果不可靠或未能捕捉用户意图，从而在安全关键应用中造成风险。

受选择性保形预测的启发，我们提出了一种选择性翻译框架，它不仅能生成形式化规范，还能判断其何时值得信赖。可靠性通过两个互补的黑盒信号进行评分：将规范反向翻译为自然语言的保真度，以及在精确语义等价下重复翻译的离散度。这两种信号针对不同的错误失效，结合起来比单独使用更能精准地分离出错误的翻译。

保形风险控制将该评分校准为接受或拒绝规范的决策，并对接受错误规范执行的比率设定了分布无关的边界；同时，基于指令嵌入的保形异常检测器在尝试任何翻译之前就能筛除分布外输入。该框架具有跨形式化规范语言的通用性，在信号时序逻辑（STL）、线性时序逻辑（LTL）和几何时空逻辑（SpaTiaL）上的实验证明了其在评估的跨层偏移下提升了翻译可靠性、鲁棒性以及实现有效的具备不确定性感知（uncertainty-aware）的拒绝机制。这项工作通过使AI系统能够识别生成的规范何时可能不可靠，为值得信赖的自然语言接口奠定了基础。

Translating natural language instructions into machine-interpretable formal specifications enables robots and autonomous systems to plan, reason, and formally verify their behavior. However, existing translation models typically generate a specification for every input, even when the result is unreliable or fails to capture the user's intent, creating risks in safety-critical applications.

Inspired by selective conformal prediction, we propose a selective translation framework that not only generates formal specifications but also determines when they can be trusted. Reliability is scored by two complementary black-box signals, the fidelity of the specification back-translated into natural language and the dispersion of repeated translations under exact semantic equivalence, which fail on different errors and jointly separate incorrect translations more sharply than either alone.

Conformal risk control calibrates this score into a decision that accepts a specification or abstains, with a distribution-free bound on the rate at which incorrect specifications are accepted for execution, and a conformal anomaly detector on instruction embeddings screens out-of-distribution inputs before any translation is attempted. The proposed framework is general across formal specification languages, with experiments on Signal Temporal Logic (STL), Linear Temporal Logic (LTL), and geometric Spatio-Temporal Logic (SpaTiaL) demonstrating improved translation reliability, robustness under the evaluated cross-tier shifts, and effective uncertainty-aware abstention. This work establishes a foundation for trustworthy natural language interfaces by enabling AI systems to recognize when generated specifications may not be reliable.

🔗 全文与资源 (Full-Text & Resources)