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

TL;DR

This paper introduces GraFT, a novel framework that improves natural language to temporal logic translation by restricting output tokens, leading to higher accuracy and better out-of-domain performance.

Contribution

GraFT reduces the complexity of NL to TL translation by constraining output tokens, enhancing learning efficiency and translation accuracy over state-of-the-art methods.

Findings

Achieves 5.49% higher end-to-end accuracy

Improves out-of-domain translation accuracy by 14.06%

Demonstrates theoretical justification for solution space reduction

Abstract

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.