GinSign：将自然语言接地到系统签名以进行时序逻辑翻译
GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation
AI总结：
GinSign通过将自然语言接地到系统签名，提升时序逻辑翻译的准确性和下游模型检查能力，实现95.5%的逻辑等价分数。
摘要：
自然语言（NL）到时序逻辑（TL）的翻译使工程师能够无需手动编写正式规范即可指定、验证和强制执行系统行为，这是构建可信自主系统的关键能力。尽管现有的NL到TL翻译框架已展现出令人鼓舞的初步结果，但这些系统要么显式假设可以访问准确的原子接地，要么在接地翻译准确性方面表现低下。在本文中，我们提出了一种名为GinSign的框架，用于将自然语言接地到系统签名以进行时序逻辑翻译。该框架引入了一个接地模型，该模型学习将NL片段映射到给定系统签名的抽象任务：给定一个提升的NL规范和一个系统签名S，分类器必须将每个提升的原子命题分配到签名定义的原子集合P中的元素。我们将接地任务分层分解——首先预测谓词标签，然后选择合适类型的常量参数。将此任务从自由生成问题分解为结构化分类问题，使得可以使用较小的掩码语言模型，从而消除了对昂贵LLM的依赖。在多个领域中的实验表明，省略接地的框架往往会产生语法正确的提升LTL，但其语义与接地的目标表达式不等价，而我们的框架支持下游模型检查，并实现了95.5%的接地逻辑等价分数，比SOTA提高了1.4倍。
英文摘要：
Natural language (NL) to temporal logic (TL) translation enables engineers to specify, verify, and enforce system behaviors without manually crafting formal specifications-an essential capability for building trustworthy autonomous systems. While existing NL-to-TL translation frameworks have demonstrated encouraging initial results, these systems either explicitly assume access to accurate atom grounding or suffer from low grounded translation accuracy. In this paper, we propose a framework for Grounding Natural Language Into System Signatures for Temporal Logic translation called GinSign. The framework introduces a grounding model that learns the abstract task of mapping NL spans onto a given system signature: given a lifted NL specification and a system signature $\mathcal{S}$, the classifier must assign each lifted atomic proposition to an element of the set of signature-defined atoms $\mathcal{P}$. We decompose the grounding task hierarchically -- first predicting predicate labels, then selecting the appropriately typed constant arguments. Decomposing this task from a free-form generation problem into a structured classification problem permits the use of smaller masked language models and eliminates the reliance on expensive LLMs. Experiments across multiple domains show that frameworks which omit grounding tend to produce syntactically correct lifted LTL that is semantically nonequivalent to grounded target expressions, whereas our framework supports downstream model checking and achieves grounded logical-equivalence scores of $95.5\%$, a $1.4\times$ improvement over SOTA.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
