SCP-NL2TL：面向自然语言到时序逻辑规范的选择性保形预测与语义验证

# SCP-NL2TL：面向自然语言到时序逻辑规约的语义验证选择性共形预测  
来源：https://arxiv.org/html/2608.05439

Yixuan Wang1, Licheng Luo1, Yu Fu1, Kaidi Xu2, Yue Dong1, Mingyu Cai1  
1University of California, Riverside, Riverside, CA, USA  
2City University of Hong Kong, Hong Kong SAR, China

[email protected], [email protected], [email protected]  
kaidixu at cityu.edu.hk, [email protected], [email protected]

###### 摘要

将自然语言指令翻译为机器可解释的形式化规约，使机器人和自主系统能够进行规划、推理并对其行为进行形式化验证。然而，现有翻译模型通常会对每个输入都生成一个规约，即使结果不可靠或未能捕捉用户意图，从而在安全关键应用中带来风险。受选择性共形预测的启发，我们提出了一种选择性翻译框架，不仅生成形式化规约，而且决定它们何时可以被信任。可靠性通过两个互补的黑盒信号进行评分：规约反译为自然语言时的保真度，以及在精确语义等价下重复翻译的离散度。这两个信号在不同的错误上失效，并且联合起来比单独使用任一信号能更清晰地区分不正确的翻译。共形风险控制将该分数校准为接受或弃权（abstain）的决策，对错误规约被接受执行的比例给出无分布假设的界；同时，一个基于指令嵌入的共形异常检测器在任何翻译尝试之前过滤掉分布外输入。所提出的框架对各种形式化规约语言具有通用性。在信号时序逻辑（STL）、线性时序逻辑（LTL）和几何时空逻辑（SpaTiaL）上的实验表明，该方法提高了翻译可靠性，在评估的跨层偏移下具有鲁棒性，并实现了有效的不确定性感知弃权。这项工作通过使AI系统能够识别生成的规约何时可能不可靠，为可信的自然语言接口奠定了基础。项目材料可在 sites.google.com/ucr.edu/scpnl2tl (https://sites.google.com/ucr.edu/scpnl2tl?usp=sharing) 获取。

*关键词*：自然语言到时序逻辑翻译，共形风险控制，选择性预测

## 1 引言

将自然语言指令翻译为机器可解释的形式化规约，使机器人和自主系统能够规划、推理并对其行为进行形式化验证[57 (https://arxiv.org/html/2608.05439#bib.bib41),41 (https://arxiv.org/html/2608.05439#bib.bib42),6 (https://arxiv.org/html/2608.05439#bib.bib43),58 (https://arxiv.org/html/2608.05439#bib.bib44)]。线性时序逻辑（LTL）、信号时序逻辑（STL）和几何时空逻辑（SpaTiaL）等形式化语言提供了时间和空间需求的表示[37 (https://arxiv.org/html/2608.05439#bib.bib21),32 (https://arxiv.org/html/2608.05439#bib.bib33),36 (https://arxiv.org/html/2608.05439#bib.bib35)]，但编写这些规约需要形式化方法的专业知识。近年来，自然语言到时序逻辑（NL2TL）系统利用语义解析、序列模型以及最近带有结构化中间表示的预训练语言模型，使这一过程更加便捷[20 (https://arxiv.org/html/2608.05439#bib.bib4),7 (https://arxiv.org/html/2608.05439#bib.bib5),31 (https://arxiv.org/html/2608.05439#bib.bib6)]。尽管这些方法显著提高了翻译准确性和结构有效性，它们总是不加区分地为每个输入生成规约。

在安全关键应用中，总是生成规约是不可取的。一个公式可能语法正确但语义错误，例如分配了错误的谓词、参数、时间运算符、区间、逻辑作用域或空间关系，从而导致下游规划器或验证器执行不符合用户意图的行为。因此，实用的NL2TL系统不仅应决定生成什么规约，还应决定该规约是否足够可靠以被执行。标准评估指标无法提供这种判断，因为精确匹配准确率描述的是平均基准性能，而非单次翻译的可信度[43 (https://arxiv.org/html/2608.05439#bib.bib45),8 (https://arxiv.org/html/2608.05439#bib.bib46),60 (https://arxiv.org/html/2608.05439#bib.bib47),42 (https://arxiv.org/html/2608.05439#bib.bib48)]。

共形预测（CP）为这种判断提供了统计工具。从任意启发式分数和一组校准示例出发，它以用户指定的概率生成覆盖真实标签的预测集，仅要求校准数据与测试数据可交换[48 (https://arxiv.org/html/2608.05439#bib.bib25)]。然而，该保证是针对集合给出的，而规划器执行的是一个公式，而不是权衡多个候选[17 (https://arxiv.org/html/2608.05439#bib.bib49),23 (https://arxiv.org/html/2608.05439#bib.bib50)]；一组候选规约无法直接交给规划器使用。

近期工作已将这一机制从“覆盖答案”转向“拒绝给出答案”。共形风险控制将覆盖目标推广到任意有界单调损失[1 (https://arxiv.org/html/2608.05439#bib.bib24)]，而选择性共形过程在第一个决策之前增加了第二个决策，测试校准数据是否支持给定的测试点，并在不支持时拒绝给出响应[55 (https://arxiv.org/html/2608.05439#bib.bib39)]