Empirical evaluation of state-of-the-art natural-language (NL) to temporal-logic (TL) translation systems reveals near-perfect performance on existing benchmarks. However, current studies measure only the accuracy of the translation of NL logic into formal TL, ignoring a system's capacity to ground atomic propositions into new scenarios or environments. This is a critical feature, necessary for the verification of resulting formulas in a concrete state space. Consequently, most NL-to-TL translation frameworks propose their own bespoke dataset in which the correct grounding is known a-priori, inflating performance metrics and neglecting the need for extensible, domain-general systems. In this paper, we introduce the Verifiable Linear Temporal Logic Benchmark ( VLTL-Bench), a unifying benchmark that measures verification and verifiability of automated NL-to-LTL translation. The dataset consists of four unique state spaces and thousands of diverse natural language specifications and corresponding formal specifications in temporal logic. Moreover, the benchmark contains sample traces to validate the temporal logic expressions. While the benchmark directly supports end-to-end evaluation, we observe that many frameworks decompose the process into i) lifting, ii) grounding, iii) translation, and iv) verification. The benchmark provides ground truths after each of these steps to enable researches to improve and evaluate different substeps of the overall problem. To encourage methodologically sound advances in verifiable NL-to-LTL translation approaches, we release VLTL-Bench here: https://www.kaggle.com/datasets/dubascudes/vltl bench.

翻译：对当前最先进的自然语言（NL）到时序逻辑（TL）翻译系统的实证评估显示，其在现有基准测试中表现接近完美。然而，现有研究仅衡量自然语言逻辑翻译为形式化时序逻辑的准确性，忽视了系统将原子命题映射到新场景或环境的能力。这一能力对于在具体状态空间中验证生成公式至关重要。因此，大多数NL-to-TL翻译框架提出其定制数据集，其中正确映射已知先验，导致性能指标虚高，并忽略了可扩展、领域通用系统的需求。本文提出可验证线性时序逻辑基准（VLTL-Bench），这是一个统一基准，用于评估自动化NL-to-LTL翻译的可验证性与验证能力。该数据集包含四个独特的状态空间、数千个多样化的自然语言规约及其对应的时序逻辑形式规约。此外，基准还提供用于验证时序逻辑表达式的样本轨迹。虽然基准直接支持端到端评估，但我们观察到许多框架将流程分解为：i）提升，ii）映射，iii）翻译，以及iv）验证。基准提供每个步骤后的真实值，使研究人员能够改进和评估整体问题的不同子步骤。为促进可验证NL-to-LTL翻译方法在方法论上的稳健发展，我们在以下地址发布VLTL-Bench：https://www.kaggle.com/datasets/dubascudes/vltl bench。