Seedlabs
Source research

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

Kumar Manas, Stefan Zwicklbauer, Adrian Paschke · 2024 · 31 citationsRead the paper

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.

What the full text shows

Working prototype
  • TR2MTL translation accuracy varies by LLM backbone. — 57.91% (GPT-4), 51.43% (GPT-3.5-turbo), 42.59% (StarCoder) (Evaluated on a drone planning dataset)
  • BART-FT-RAW outperformed the prompting-based TR2MTL models. — 69.36% accuracy (Evaluated on a drone planning dataset)
  • TR2MTL performance degrades when the logical structure of the target formula differs from the prompt examples. (e.g., prompts with G(A ∨ B) ∨ C lead to poor performance on G(A ∨ B) ∧ C)
  • TR2MTL fails to generate formulas with multiple predicate arguments if prompts only contain single-argument predicates. (Limited data for prompting)
Setup
Evaluation conducted using a custom dataset of traffic rules derived from the Vienna Convention on Road Traffic (VCoRT) and German Road Traffic Regulation (StVO), and a drone planning dataset.
How
The framework uses a chain-of-thought (CoT) in-context learning approach with two-shot prompting to guide LLMs in translating natural language traffic rules into Metric Temporal Logic (MTL). It employs an MTL template and a parser to filter and generate the final formal specifications.
Limitations
Performance is highly dependent on the diversity and logical structure of the few-shot prompts. · Requires a human-in-the-loop for verification and editing due to the safety-critical nature of the domain. · Mapping high-level predicates to specific simulator formats (e.g., CommonRoad) is currently manual.

Summarized by Gemma 4 from the open-access full text · 10 Oct 2026. Read it