@inproceedings{english-etal-2026-ginsign,
title = "{G}in{S}ign: Grounding Natural Language Into System Signatures for Temporal Logic Translation",
author = "English, William H and
Walker, Chase and
Simon, Dominic and
Ewetz, Rickard",
editor = "Lee, Hung-Yi and
Dev, Sunipa and
Li, Jessy and
Elliott, Desmond",
booktitle = "Findings of the {A}ssociation for {C}omputational {L}inguistics: {EMNLP} 2026",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.findings-emnlp.1406/",
pages = "29970--29988",
ISBN = "979-8-89176-462-0",
abstract = "Natural language (NL) to temporal logic (TL) translation lets engineers specify and verify system behaviors without hand-crafting formal specifications. Existing frameworks lift NL into syntactically valid TL but leave atomic propositions abstract{---}not \textit{grounded} to the concrete predicates and typed objects a system exposes (e.g., binding ``find the bookbag'' to \texttt{search(backpack)}). Ungrounded formulas cannot be checked over traces, yet current systems either omit grounding or ground inaccurately. We propose , a modular stage for \underline{G}rounding Natural Language \underline{In}to System \underline{Sign}atures that attaches to any NL-to-TL lifter. We cast grounding as signature-conditioned classification: enumerating the signature as an input prefix lets one encoder-only model assign each abstract AP a predicate and its typed arguments, generalize to unseen signature elements, and transfer across domains without retraining, while never hallucinating out-of-signature atoms. Because predictions are selections from the enumerated signature, the out-of-signature rate is 0{\%} \textit{by construction}, against up to 95{\%} for prompted LLMs given the same signature in-context. attains at least 99{\%} joint grounding accuracy across seven domains (worst case 99.39 {\ensuremath{\pm}} 0.04 over five seeds); paired with a lifter, it produces executable specifications that track the oracle-grounding upper bound, improving grounded logical equivalence by 75{\%} over the strongest prompted-LLM and embedding-similarity grounder."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="english-etal-2026-ginsign">
<titleInfo>
<title>GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation</title>
</titleInfo>
<name type="personal">
<namePart type="given">William</namePart>
<namePart type="given">H</namePart>
<namePart type="family">English</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Chase</namePart>
<namePart type="family">Walker</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Dominic</namePart>
<namePart type="family">Simon</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Rickard</namePart>
<namePart type="family">Ewetz</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-10</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Findings of the Association for Computational Linguistics: EMNLP 2026</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hung-Yi</namePart>
<namePart type="family">Lee</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sunipa</namePart>
<namePart type="family">Dev</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jessy</namePart>
<namePart type="family">Li</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Desmond</namePart>
<namePart type="family">Elliott</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Budapest, Hungary</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-462-0</identifier>
</relatedItem>
<abstract>Natural language (NL) to temporal logic (TL) translation lets engineers specify and verify system behaviors without hand-crafting formal specifications. Existing frameworks lift NL into syntactically valid TL but leave atomic propositions abstract—not grounded to the concrete predicates and typed objects a system exposes (e.g., binding “find the bookbag” to search(backpack)). Ungrounded formulas cannot be checked over traces, yet current systems either omit grounding or ground inaccurately. We propose , a modular stage for \underlineGrounding Natural Language \underlineInto System \underlineSignatures that attaches to any NL-to-TL lifter. We cast grounding as signature-conditioned classification: enumerating the signature as an input prefix lets one encoder-only model assign each abstract AP a predicate and its typed arguments, generalize to unseen signature elements, and transfer across domains without retraining, while never hallucinating out-of-signature atoms. Because predictions are selections from the enumerated signature, the out-of-signature rate is 0% by construction, against up to 95% for prompted LLMs given the same signature in-context. attains at least 99% joint grounding accuracy across seven domains (worst case 99.39 \ensuremath\pm 0.04 over five seeds); paired with a lifter, it produces executable specifications that track the oracle-grounding upper bound, improving grounded logical equivalence by 75% over the strongest prompted-LLM and embedding-similarity grounder.</abstract>
<identifier type="citekey">english-etal-2026-ginsign</identifier>
<location>
<url>https://aclanthology.org/2026.findings-emnlp.1406/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>29970</start>
<end>29988</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation
%A English, William H.
%A Walker, Chase
%A Simon, Dominic
%A Ewetz, Rickard
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Findings of the Association for Computational Linguistics: EMNLP 2026
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-462-0
%F english-etal-2026-ginsign
%X Natural language (NL) to temporal logic (TL) translation lets engineers specify and verify system behaviors without hand-crafting formal specifications. Existing frameworks lift NL into syntactically valid TL but leave atomic propositions abstract—not grounded to the concrete predicates and typed objects a system exposes (e.g., binding “find the bookbag” to search(backpack)). Ungrounded formulas cannot be checked over traces, yet current systems either omit grounding or ground inaccurately. We propose , a modular stage for \underlineGrounding Natural Language \underlineInto System \underlineSignatures that attaches to any NL-to-TL lifter. We cast grounding as signature-conditioned classification: enumerating the signature as an input prefix lets one encoder-only model assign each abstract AP a predicate and its typed arguments, generalize to unseen signature elements, and transfer across domains without retraining, while never hallucinating out-of-signature atoms. Because predictions are selections from the enumerated signature, the out-of-signature rate is 0% by construction, against up to 95% for prompted LLMs given the same signature in-context. attains at least 99% joint grounding accuracy across seven domains (worst case 99.39 \ensuremath\pm 0.04 over five seeds); paired with a lifter, it produces executable specifications that track the oracle-grounding upper bound, improving grounded logical equivalence by 75% over the strongest prompted-LLM and embedding-similarity grounder.
%U https://aclanthology.org/2026.findings-emnlp.1406/
%P 29970-29988
Markdown (Informal)
[GinSign: Grounding Natural Language Into System Signatures for Temporal Logic Translation](https://aclanthology.org/2026.findings-emnlp.1406/) (English et al., Findings 2026)
ACL