arXiv:2512.16814cs.CLcs.AI2025-12ICML被引 12

用语法约束提升自然语言转时序逻辑的准确率

Grammar-Forced Translation of Natural Language to Temporal Logic using LLMs

  • 通过限制每步输出词表,降低翻译复杂度
  • 在多个基准上提升端到端准确率5.49%、跨领域准确率14.06%
  • 适合需要高可靠形式化交互的机器人系统研发

将自然语言(NL)转化为时序逻辑(TL)是人与机器人及自主系统沟通的关键。现有方法通常分两步:原子命题(APs)提取和翻译。但当前方法在准确提取、共指消解以及小样本学习方面表现不佳。本文提出一种名为语法强制翻译(GraFT)的框架,基于观察:以往方法让语言模型从全词汇表中迭代预测,导致复杂度高。GraFT通过在每一步仅允许极少数有效输出词,大幅压缩解空间,利用问题特性的独特性实现降维。我们还提供了理论依据,说明解空间缩小可促进更高效学习。在CW、GLTL和Navi三个基准上评估,相较于先进方法,GraFT平均提升端到端翻译准确率5.49%,跨域翻译准确率14.06%。

原文摘要 · Abstract (English)

Translating natural language (NL) into a formal language such as temporal logic (TL) is integral for human communication with robots and autonomous systems. State-of-the-art approaches decompose the task into a lifting of atomic propositions (APs) phase and a translation phase. However, existing methods struggle with accurate lifting, the existence of co-references, and learning from limited data. In this paper, we propose a framework for NL to TL translation called Grammar Forced Translation (GraFT). The framework is based on the observation that previous work solves both the lifting and translation steps by letting a language model iteratively predict tokens from its full vocabulary. In contrast, GraFT reduces the complexity of both tasks by restricting the set of valid output tokens from the full vocabulary to only a handful in each step. The solution space reduction is obtained by exploiting the unique properties of each problem. We also provide a theoretical justification for why the solution space reduction leads to more efficient learning. We evaluate the effectiveness of GraFT using the CW, GLTL, and Navi benchmarks. Compared with state-of-the-art translation approaches, it can be observed that GraFT the end-to-end translation accuracy by 5.49% and out-of-domain translation accuracy by 14.06% on average.

自然语言转逻辑时序逻辑大模型应用形式化验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。