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

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 grounding of atomic propositions (APs) phase and a translation phase. However, existing methods struggle with accurate grounding, 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 grounding 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 improves the end-to-end translation accuracy by 5.49% and out-of-domain translation accuracy by 14.06% on average.

Temporal logic is a mathematical language used to express or describe the behavior of a system over time. It isn't terribly easy for human beings to write complex temporal logic expressions, so we would benefit from technology that helps humans translate what they are saying in English (or whatever their own native language happens to be) into temporal logic. While some have used expensive large language models, such as Chat-GPT, we adopt a cheaper and more structured approach using a combination of two much smaller language models. We use BERT to simplify the input, that is a natural language expression, into what we call "lifted" natural language. This is just the same sentence, but with some groups of words replaces by small variable names. By using the lifted natural language, we can produce much more accurate temporal logic translations. Additionally, we are using a sequence-to-sequence model to perform translation, rather than a next-token-prediction or "generative" model. This means we can enforce rules about the entire output sequence, very efficiently. We hope that our contribution advances the field of natural language formalization.