摘要

本文由Weizhi Tang和Vaishak Belle共同撰写，题为“LTLBench: Towards Benchmarks for Evaluating Temporal Logic Reasoning in Large Language Models”，旨在探讨大型语言模型（LLMs）在时间逻辑推理（TR）能力方面的表现。论文提出了一种新颖的方法，通过利用随机有向图生成、线性时间逻辑（LTL）公式和NuSMV模型检查器来设计和开发一个用于构建评估LLMs TR能力的基准数据集的流程。基于此流程，作者构建了一个名为LTLBench的基准数据集，包含2,000个TR挑战，并对六种LLMs进行了评估。此外，论文还探讨了增加事件数量和公式操作符对TR问题复杂性和LLMs性能的影响。研究结果表明，尽管LLMs在处理TR挑战方面显示出一定的潜力，但它们在复杂的TR问题上仍面临挑战。论文期望这项工作能为LLMs的TR能力提供深入见解，并为未来的TR评估提供有价值的工具。

原理

LTLBench的核心工作原理基于随机有向图生成、LTL公式和NuSMV模型检查器的结合。首先，通过随机生成有向图来构建TR问题的上下文，其中每个节点代表一个事件，边表示事件之间的直接关系。接着，利用LTL公式生成算法，根据图中的事件生成相应的LTL公式，这些公式用于描述事件之间的逻辑关系。然后，将生成的图和LTL公式转换为NuSMV代码，通过NuSMV模型检查器执行这些代码，以确定TR问题的真实标签。最后，将事件信息和LTL公式转换为自然语言形式的TR问题，用于评估LLMs的TR能力。这种方法不仅确保了数据集的多样性和复杂性，还通过NuSMV模型检查器提供了准确的问题标签，从而能够全面评估LLMs在TR任务上的表现。

流程

LTLBench的工作流程包括四个主要阶段：随机有向图生成、LTL公式生成、NuSMV代码生成和自然语言生成。首先，在随机有向图生成阶段，根据给定的事件数量n（n > 1）生成一个有向图，确保事件之间存在过渡关系。其次，在LTL公式生成阶段，基于图中的事件，使用LTL公式生成算法生成包含给定操作符数量m（m > 0）的LTL公式。接着，在NuSMV代码生成阶段，将图中的事件信息和LTL公式转换为NuSMV代码，并通过NuSMV模型检查器执行代码以获取TR问题的真实标签。最后，在自然语言生成阶段，将事件信息和LTL公式转换为自然语言形式的TR问题，用于LLMs的评估。整个流程通过随机生成和转换，确保了数据集的多样性和复杂性，从而能够全面评估LLMs在TR任务上的表现。

应用

LTLBench的应用前景广泛，主要体现在以下几个方面：首先，它可以作为评估和比较不同LLMs在时间逻辑推理能力上的基准工具。其次，通过调整事件数量和操作符的复杂度，LTLBench可以用于研究LLMs在处理不同复杂度TR问题时的性能变化。此外，该基准数据集还可以用于指导LLMs的进一步开发和优化，特别是在需要处理复杂时间逻辑推理任务的领域，如智能问答系统、自动化规划和决策支持系统等。长远来看，LTLBench有望推动LLMs在更广泛的人工智能应用中的实际部署和应用，特别是在需要高度可靠和精确时间逻辑推理能力的场景中。