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

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

自动驾驶车辆需要遵守交通规则，但将自然语言交通规则手动转化为形式化规范需要领域知识和逻辑专业知识，限制了其适应性。因此，本文提出了一种使用大型语言模型自动将交通规则翻译为度量时态逻辑的框架TR2MTL，旨在成为人机交互的AV规则形式化系统。

TR2MTL框架使用链式思维上下文学习方法，指导大型语言模型逐步翻译交通规则并生成有效和语法正确的MTL公式。该框架是领域无关的，即使数据集很小也能实现高精度和泛化能力。此外，该方法有效地预测了在非结构化交通规则中具有不同逻辑和语义结构的公式。

本文提出了TR2MTL框架，使用大型语言模型自动将交通规则翻译为度量时态逻辑的形式化规范。该框架使用链式思维上下文学习方法，能够有效地预测具有不同逻辑和语义结构的公式。实验结果表明，该框架是领域无关的，即使数据集很小也能实现高精度和泛化能力。

最近的相关研究包括使用机器学习方法自动推断交通规则的研究，以及使用形式化方法验证AV遵守交通规则的研究。例如，论文“Automated Synthesis of Traffic Rules for Autonomous Vehicles”和“Formal Verification of Autonomous Vehicle Platooning Protocols with Dynamic Time Warping Logic”。