GinSign：将自然语言 grounding 到系统签名，用于时序逻辑翻译

自然语言（NL）到时序逻辑（TL）翻译使工程师能够在无需手动编写形式化规范的情况下指定、验证和执行系统行为——这一能力对于构建可靠的自主系统至关重要。虽然现有NL-to-TL翻译框架已取得鼎舞初始成果，但这些系统要么显式假设访问准确的原子 grounding，要么在grounded翻译准确性方面存在不足。本文提出了一种面向时序逻辑翻译的框架，称为GinSign（Grounding Natural Language Into System Signatures for Temporal Logic）。该框架引入一种grounding模型，通过学习将NL片段映射到给定系统签名的抽象任务：给定提升后的NL规范和系统签名$\mathcal{S}$，分类器必须将每个提升原子命题分配给由签名定义的原子集合$\mathcal{P}$中的一个元素。我们在层次结构上分解了grounding任务——首先预测谓词标签，然后选择相应类型的常数参数。将该任务从自由形式生成问题分解为结构化分类问题，使得可以使用更小的掩码语言模型，无需依赖高成本的大语言模型。跨多个领域的实验表明，缺少grounding的框架倾向于产生语法正确的提升LTL，但在语义上与grounded目标表达式不等价；而我们框架支持下游模型检查，并实现了grounded逻辑等价性得分达到95.5%，显著优于SOTA的1.4倍。