# GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation

arXiv: https://arxiv.org/abs/2512.16770 · HTML: https://mlsanity.com/paper/2512.16770/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 39 references that are in the map.
- First posted on arXiv 18 Dec 2025.

## Builds on (most cited first, 15 of 15)

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer](https://mlsanity.com/paper/1910.10683/) (2019)
- [Referring Expression Comprehension: A Survey of Methods and Datasets](https://mlsanity.com/paper/2007.09554/) (2020)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models](https://mlsanity.com/paper/2305.07766/) (2023)
- [Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments](https://mlsanity.com/paper/2302.11649/) (2023)
- [Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification](https://mlsanity.com/paper/2303.08006/) (2023)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Learning a natural-language to LTL executable semantic parser for grounded robotics](https://mlsanity.com/paper/2008.03277/) (2020)
- [Mining Parametric Temporal Logic Properties in Model Based Design for Cyber-Physical Systems](https://mlsanity.com/paper/1512.07956/) (2015)
- [PROC2PDDL: Open-Domain Planning Representations from Texts](https://mlsanity.com/paper/2403.00092/) (2024)
- [Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges](https://mlsanity.com/paper/2402.13075/) (2024)
- [Generalizing to New Domains by Mapping Natural Language to Lifted LTL](https://mlsanity.com/paper/2110.05603/) (2021)
- [On Systematically Building a Controlled Natural Language for Functional Requirements](https://mlsanity.com/paper/2005.01355/) (2020)
- [Verifiable Natural Language to Linear Temporal Logic Translation: A Benchmark Dataset and Evaluation Suite](https://mlsanity.com/paper/2507.00877/) (2025)

## Abstract (arXiv)

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 S, the classifier must assign each lifted atomic proposition to an element of the set of signature-defined atoms 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× improvement over SOTA.