TR2MTL: LLM based framework for Metric Temporal Logic Formalization of Traffic Rules

TL;DR

The paper tackles the challenge of translating vague, unstructured natural-language traffic rules into precise formal specifications. It introduces TR2MTL, a human-in-the-loop framework that uses chain-of-thought prompting and controlled MTL templates to translate traffic rules into Metric Temporal Logic, with an MTL parser ensuring syntactic and semantic correctness. Evaluated on a newly constructed dataset of 50 traffic rules from StVO and VCoRT, TR2MTL demonstrates strong performance with CoT prompting, cross-domain generalization to marine and drone domains, and practical trajectory-monitoring applications. The work enables rapid, interpretable rule formalization for autonomous vehicles, highlighting both the potential and the need for further grounding of formulas to real sensor data and broader temporal-logical formalisms.

Abstract

Traffic rules formalization is crucial for verifying the compliance and safety of autonomous vehicles (AVs). However, manual translation of natural language traffic rules as formal specification requires domain knowledge and logic expertise, which limits its adaptation. This paper introduces TR2MTL, a framework that employs large language models (LLMs) to automatically translate traffic rules (TR) into metric temporal logic (MTL). It is envisioned as a human-in-loop system for AV rule formalization. It utilizes a chain-of-thought in-context learning approach to guide the LLM in step-by-step translation and generating valid and grammatically correct MTL formulas. It can be extended to various forms of temporal logic and rules. We evaluated the framework on a challenging dataset of traffic rules we created from various sources and compared it against LLMs using different in-context learning methods. Results show that TR2MTL is domain-agnostic, achieving high accuracy and generalization capability even with a small dataset. Moreover, the method effectively predicts formulas with varying degrees of logical and semantic structure in unstructured traffic rules.

Figures (4)

• Figure 1: TR2MTL architecture for translating traffic rules into MTL. We use a pre-trained LLM to translate traffic rules into MTL formulas. We pass the traffic rules to the LLM and parse its output with an MTL parser to get the final translation. We guide the LLM with MTL templates and prompts (examples of traffic rules and their MTL translations). Prompts (see Fig. \ref{['fig:noncotprompt']}, \ref{['fig:cotprompt']}) are designed to fit the traffic rule formalization task.
• Figure 2: Prompt without reasoning and step-by-step thinking for in-context learning. Two-shot learning prompts or two traffic rules examples are shown. MTL output is directly provided without additional hints. Only Natural language text is provided during the test phase, and the model should generate the MTL formula. Annotations are for illustration (not part of the actual prompts).
• Figure 3: Prompt with reasoning and step-by-step thinking for in-context learning. Prompts used in our experiments, each having two input-thought process-output triplets or two-shot learning (a total of 2 such diverse example pairs were used). The step-by-step thought process breaks the rules into subrules and generates formulas. Later, they are combined to form the complete MTL rules. Prompts are made of such examples, but only textual rules are provided during testing, and the model generates step thinking and the final MTL formula similar to the two prompts example. We omit the details of the thought process for the second prompt, but it can be written similarly to the first prompt.
• Figure 4: Distribution of mistakes made by the framework.