TR2MTL: LLM based framework for Metric Temporal Logic Formalization of Traffic Rules
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Autonomous VehiclesIn-Context LearningTranslationvalidSimilar Papers 제목 키워드 기반
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
A rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as writing formal specifications is an error-p…
Using Ontologies for the Formalization and Recognition of Criticality for Automated Driving
Knowledge representation and reasoning has a long history of examining how knowledge can be formalized, interpreted, and semantically analyzed by machines. In the area of automated vehicles, recent advances suggest the a…
GuardAD: Safeguarding Autonomous Driving MLLMs via Markovian Safety Logic
Multimodal large language models (MLLMs) are increasingly integrated into autonomous driving (AD) systems; however, they remain vulnerable to diverse safety threats, particularly in accident-prone scenarios. Recent safeg…
Autonomous DrivingDeontic Temporal Logic for Formal Verification of AI Ethics
Ensuring ethical behavior in Artificial Intelligence (AI) systems amidst their increasing ubiquity and influence is a major concern the world over. The use of formal methods in AI ethics is a possible crucial approach fo…
EthicsFairnessUrban Traffic Flow Forecast Based on FastGCRNN
Traffic forecasting is an important prerequisite for the application of intelligent transportation systems in urban traffic networks. The existing works adopted RNN and CNN/GCN, among which GCRN is the state of art work,…
Decoder