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

📄 arXiv: 2406.05709v1 📥 PDF

作者: Kumar Manas, Stefan Zwicklbauer, Adrian Paschke

分类: cs.RO, cs.FL, cs.LG

发布日期: 2024-06-09

备注: Accepted for publication in Proceedings of the IEEE Intelligent Vehicles Symposium (IV), Jeju Island - Korea, 2-5 June 2024

DOI: 10.1109/IV55156.2024.10588650

💡 一句话要点

TR2MTL：基于LLM的交通规则度量时序逻辑形式化框架

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 交通规则形式化 度量时序逻辑 大型语言模型 思维链学习 自动驾驶 人机协同 自然语言处理

📋 核心要点

  1. 现有交通规则形式化方法依赖人工翻译，需要领域知识和逻辑学专业技能，成本高且效率低。
  2. TR2MTL框架利用大型语言模型和思维链上下文学习，实现交通规则到度量时序逻辑的自动翻译。
  3. 实验结果表明，TR2MTL在交通规则形式化任务上表现出高精度和泛化能力，且领域无关。

📝 摘要（中文）

交通规则形式化对于验证自动驾驶车辆（AVs）的合规性和安全性至关重要。然而，将自然语言交通规则手动翻译为形式化规范需要领域知识和逻辑专业知识，这限制了其应用。本文介绍了一种名为TR2MTL的框架，该框架利用大型语言模型（LLMs）自动将交通规则（TR）翻译成度量时序逻辑（MTL）。它被设想为一个用于AV规则形式化的人在环系统。该框架采用思维链上下文学习方法，指导LLM逐步翻译并生成有效且语法正确的MTL公式。它可以扩展到各种形式的时序逻辑和规则。我们在一个具有挑战性的交通规则数据集上评估了该框架，该数据集是我们从各种来源创建的，并将其与使用不同上下文学习方法的LLM进行了比较。结果表明，TR2MTL是领域无关的，即使在小型数据集上也能实现高精度和泛化能力。此外，该方法能够有效地预测非结构化交通规则中具有不同程度的逻辑和语义结构的公式。

🔬 方法详解

问题定义：论文旨在解决将自然语言描述的交通规则自动转化为形式化度量时序逻辑（MTL）表达式的问题。现有方法主要依赖人工完成这一转化过程，需要专家具备交通规则的领域知识以及形式化逻辑的专业技能，成本高昂且效率低下。此外，人工转化容易引入主观偏差，难以保证转化结果的一致性和准确性。

核心思路：论文的核心思路是利用大型语言模型（LLMs）强大的自然语言理解和生成能力，通过思维链（Chain-of-Thought）上下文学习的方法，引导LLM逐步完成从自然语言交通规则到MTL表达式的转化。这种方法旨在模拟人类专家进行形式化推理的过程，将复杂的转化任务分解为一系列更小的、易于处理的步骤，从而提高转化结果的准确性和可解释性。

技术框架：TR2MTL框架采用人机协同的设计理念，将LLM作为自动翻译的核心引擎，并允许人工干预和修正。框架主要包含以下几个阶段：1) 输入自然语言交通规则；2) LLM基于思维链上下文学习，逐步推导出MTL表达式；3) 人工审核和修正LLM生成的MTL表达式；4) 输出最终的、形式化的交通规则表示。框架可以灵活扩展，支持不同类型的时序逻辑和规则。

关键创新：TR2MTL的关键创新在于将思维链上下文学习方法应用于交通规则的形式化任务。通过提供一系列精心设计的示例，引导LLM逐步推理，从而显著提高了转化结果的准确性和可信度。此外，该框架具有领域无关性，可以应用于其他领域的规则形式化任务。

关键设计：论文中，思维链上下文学习的示例设计至关重要。这些示例需要覆盖各种类型的交通规则和对应的MTL表达式，并清晰地展示推理过程中的关键步骤。具体而言，示例需要包含：1) 自然语言交通规则；2) 对规则的语义分析；3) 将语义分析转化为MTL表达式的步骤；4) 最终的MTL表达式。此外，论文还可能涉及一些超参数的调整，例如LLM的选择、上下文示例的数量等，这些参数的选择会影响最终的转化效果。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

TR2MTL框架在自建的交通规则数据集上进行了评估，实验结果表明，该框架能够有效地将自然语言交通规则转化为MTL表达式，即使在小数据集上也能实现较高的准确率和泛化能力。与直接使用LLM进行翻译的方法相比，TR2MTL通过思维链上下文学习，显著提高了转化结果的准确性和可解释性。具体性能数据未知，但摘要强调了其优于其他上下文学习方法。

🎯 应用场景

TR2MTL框架可应用于自动驾驶车辆的安全性验证、交通规则合规性检查、智能交通系统设计等领域。通过自动将自然语言交通规则转化为形式化规范，可以提高自动驾驶系统的可靠性和安全性，降低开发和维护成本。未来，该框架可以扩展到其他领域的规则形式化，例如金融监管、法律条文等，具有广阔的应用前景。

📄 摘要（原文）

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.