tBen: Benchmarking and Testing the Rule-Based Temporal Logic Reasoning Ability of Large Language Models with DatalogMTL

Authors: Dingmin Wang, Bocheng Zou, Zhen Han, zhiqiang xu
Primary area: datasets and benchmarks
Keywords: Temporal Logic Reasoning, Large Language Models, DatalogMTL

Abstract:
Large language models (LLMs) are increasingly adopted for a variety of tasks, including multi-hop question answering, knowledge probing, and symbolic commonsense reasoning. While LLMs have advanced the state-of-the-art in these areas, their ability to explicitly solve rule-based temporal logic reasoning problems—a complex cognitive process involving the understanding, representation, and manipulation of temporal information such as events, their durations, and relationships—remains unexplored. To enhance understanding of LLM performance in this common task widely explored in the traditional symbolic AI field, we have developed a new set of synthetic benchmarks for rule-based temporal logic reasoning tBen. Our tBen benchmarks are built within the context of DatalogMTL, a powerful knowledge representation language for reasoning about the properties of systems that evolve over time, in which we provide flexible configurations for customizing temporal rules and task complexity.

We evaluated the close-sourced GPT-4o and the open-sourced Llama-3 using three common prompting settings—$\textit{zero-shot}$, $\textit{few-shot}$, and $\textit{zero-shot-CoT}$—on our synthetic benchmarks. Our key findings are as follows: (i) Without generating the reasoning process (chain-of-thought), even  advanced LLMs like GPT-4o exhibited nearly random performance on these rule-based temporal logic reasoning tasks. However, with chain-of-thought prompting, LLMs demonstrated preliminary temporal logical reasoning abilities; (ii) Both GPT-4o and Llama-3 were unable to solve temporal logical reasoning problems involving recursion, indicating a lack of advanced complex reasoning capabilities in understanding symbolic representations involving time; (iii) There is significant room for improvement in leveraging large language models to address problems widely explored in the traditional logic-based AI domain. Prompts and datasets are available in the appendix, and a datasheet for tBen is also provided.

Decision: reject
Reviewer scores: 5, 5, 3, 3

Reviews and discussion:
<thread>
creation date:
1729059236523

thread_type:
official_review

<thread_object>
creator: reviewer_dt7e

<content>
summary:
This paper proposes TBen, a benchmark for evaluating the ability of LLMs to perform rule-based temporal logic reasoning.
TBen uses DatalogMTL to describe problems, a language capable of describing temporal logic data.
TBen defines six levels of rule complexity, allowing customization of reasoning data formats based on logical complexity and temporal rules.
The authors conduct experiments with standard prompting techniques and chain-of-thought prompting techniques on GPT-4o and LLaMA3 models to explore the models' performance on temporal logic reasoning.
The results show that the models only achieve results similar to random guessing when generating intermediate steps. 
Additionally, this paper finds that current models are unable to solve temporal reasoning problems involving recursive forms, indicating the challenges faced by current models in solving complex temporal logic reasoning.

strengths:
1. This paper proposes tBen for evaluating the ability of large language models to perform rule-based temporal logic reasoning. Furthermore, the data construction approach in the paper allows for the adjustment of the types of time and the complexity of logic to generate benchmarks at different difficulty levels.
2. Evaluations are conducted based on the proposed benchmark with state-of-the-art LLMs. They analyze the shortcoming and challenges faced by current LLMs.
3. The authors also conduct some analysis on some topics, such as rule v.s. NL and ablations.

weaknesses:
1. The TBen benchmark is entirely rule-generated and can yield deterministic results using solvers, which limits the breadth of its application. This benchmark is only suitable for evaluating models' performance in rule-based temporal logic reasoning and cannot be extended to certain real-world scenarios. The dataset's usage scenarios are significantly restricted, which is a shortcoming in its content. In other words, this benchmark is more tailored to serve the analysis testbed for this paper rather than subsequent follow-up research.
2. If this paper is regarded as an evaluation paper, then the analysis work and related in-depth discussions conducted in this paper are insufficient. The paper only conducted experiments on two models and the analysis was relatively superficial, lacking in-depth analysis.

questions:
1. This benchmark is fully symbolic, so whether there will be deviations in the process of converting it into natural language form (verbalization), leading to a gap between language models' handling of symbolic reasoning and natural language reasoning.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730649860760

thread_type:
official_review

<thread_object>
creator: reviewer_dbvf

<content>
summary:
The paper introduces TBEN, a new synthetic benchmark designed to evaluate the rule-based temporal logic reasoning abilities of large language models (LLMs). TBEN focuses on DatalogMTL, an automated reasoning language that extends Datalog with temporal logic, enabling reasoning about time. The benchmark consists of tasks spanning six levels of complexity, from simple single-atom rules to more complex recursive rules.

The authors evaluate two LLMs (GPT-4 and Llama-3) using three prompting strategies: zero-shot, few-shot, and zero-shot chain-of-thought (CoT). They find that without reasoning (i.e., CoT), even advanced models perform poorly. They also observe that both models struggle with recursive reasoning, highlighting limitations in handling advanced temporal logic problems.

strengths:
- **Importance of temporal reasoning** Reasoning about time is a key aspect of intelligence, which seems to be still understudied in the area of large language models. The paper shows (to an extent) how LLMs struggle in this task.

- **Well thought task generation** The authors present a well-thought method for generating synthetic tasks with controlled/varying levels of complexity. Such systematic approach is valuable.

weaknesses:
- **Logical Reasoning or Language Familiarity?**: It is unclear whether the poor performance of LLMs is due to their inability to reason about temporal concepts or their unfamiliarity with the formal syntax and semantics of DatalogMTL. The benchmark may conflate temporal reasoning abilities with decoding a niche formal language: the evaluated models may not have been adequately exposed to formal temporal logic during training (actually even in natural language, LLMs tend to perform worse on languages with lesser training data). Not referenced in the text, Appendix E touches a bit this aspect, but is not sufficient (besides being not well written yet). 


- **Impact on the Broader Community**: The practical implications and impact of the findings on the ICLR community and AI research at large are limited (beyond showing another domain where LLMs struggle). This for me the most crucial weakness. To be suitable for ICLR, the paper should have may be tested the temporal reasoning in truly natural language contexts (not just templated translations of a formal language like Figure 4.) and provided deep insights on why they work or fail at these tasks etc. In its current form, the paper is a better fit for a specialized benchmark workshop.

- **Binary question format**: The tasks result in simple true/false answers. So while this eases the task of the evaluation, such binary questions may not capture the full complexity of temporal reasoning and could limit the depth of insights gained from the evaluation.

- **Clarity and Referencing Issues**: The manuscript frequently references the "Appendix" without specifying sections or page numbers, making it challenging for readers to locate supplementary information.

questions:
In which way exposing the formal temporal reasoning weaknessess in LLMs is essential for the broader goal of improving reasoning abilities of LLMs? How does it differ from exposing weaknesses in any other specific domain like coding in a particular  programming language? 

How do we know if we're testing the models abilities to reason about time?  or if we're limited by the models' lack of fluency in this niche formal language to which the models were not as much exposed as the rest? 

Why not put all the focus on the natural language temporal reasoning abilities of the models? since natural language is what they were exposed to most? 

As a follow-up, the current templated way of generating natural language questions is good, but "unnatural", how about using LLMs to generate the natural language text instead? and transforming the entire exercise into an actual natural language based reasoning about time? 

Finally, it would be interesting to extend the evaluation to the "large reasoning models" like the open AI's o1 family.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730714812271

thread_type:
official_review

<thread_object>
creator: reviewer_fuzn

<content>
summary:
The paper constructs a benchmark for evaluating the rule-based temporal reasoning capabilities of large language models, using a knowledge representation language called DatalogMTL. It introduces the DatalogMTL language, outlines the dataset construction process, and provides details on the final evaluation tasks. Besides, It tests models such as GPT-4o and Llama-3 on this dataset.

strengths:
1. Unlike previous works that focus more on natural language-based logical reasoning abilities, this paper evaluates the rule-based temporal logic reasoning abilities of large language models.  
2. This paper provides a detailed introduction to the representation language DatalogMTL and the entire benchmark construction process, which will help readers gain a better understanding of the evaluation benchmark.

weaknesses:
1. This paper should provide a more detailed discussion on the significance of this dataset. For the LLMs community, what are the core challenges that this dataset presents compared to other benchmarks assessing the logic reasoning abilities of large language models? Since it ultimately translates into prompts for the models, what is the unique significance of temporality in this context? Does it introduce challenges that are completely different from previous tasks in logic, mathematics, and code reasoning? On another note, how can performing well on this benchmark assist in downstream tasks? Additionally, for the traditional rule-based reasoning community, why should LLMs be applied to this rule-based temporal task, and what are the advantages and disadvantages of LLMs compared to traditional rule-based reasoning methods?
2. The current design of the prompts seems inadequate. For example, in line 746, it does not explain to the model what the "@" symbol means, so it is unreasonable to expect the model to produce correct results. Additionally, in Figure 2, how does the model understand the meanings of these combinations of expressions? The existing prompts do not seem to clearly explain this to the model.

questions:
Please refer to the weaknesses section above.
</content>
</thread_object>

</thread>
<thread>
creation date:
1731032583017

thread_type:
official_review

<thread_object>
creator: reviewer_vhgk

<content>
summary:
The paper presents a synthetic benchmark to evaluate temporal logic reasoning capabilities of large language models (LLMs). The benchmark uses the DatalogMTL language, to represent problems involving rule-based temporal logic. The evaluation on GPT-4o and LLama3 show that LLMs perform poorly on this benchmark highlighting a gap in LLM capabilities when compared to traditional symbolic approaches.

strengths:
The authors look at metric temporal reasoning problems (specifically fact entailment ones) and provide a varied set of problems to evaluate LLMs. They evaluate both an open-source and a closed model and provide ablation studies to get better understanding of the LLMs’ capabilities in such temporal reasoning tasks.

weaknesses:
My primary concern with the proposed benchmark is that it relies on Yes or No questions, which I believe are inadequate for effectively measuring the logical reasoning abilities of an LLM. For a more informative evaluation of whether LLMs are capable of metric temporal reasoning, the benchmark should employ more descriptive questions. 

There have been several works that examine LLM performance on traditional reasoning problems, such as satisfiability, PDDL planning, and scheduling [1,2,3], and these studies consistently show that LLMs perform poorly on such tasks. Additionally, other works have highlighted the inability of Chain of Thought to generalize within such reasoning problems [4,5]. However, these works have not been compared or contrasted to in the paper in order to better position the benchmark in terms of its contribution.

[1] Ye, Xi, Qiaochu Chen, Isil Dillig, and Greg Durrett. "Satlm: Satisfiability-aided language models using declarative prompting." Advances in Neural Information Processing Systems 36 (2024).

[2] Valmeekam, Karthik, Matthew Marquez, Alberto Olmo, Sarath Sreedharan, and Subbarao Kambhampati. "Planbench: An extensible benchmark for evaluating large language models on planning and reasoning about change." Advances in Neural Information Processing Systems 36 (2024).

[3] Silver, Tom, Varun Hariprasad, Reece S. Shuttleworth, Nishanth Kumar, Tomás Lozano-Pérez, and Leslie Pack Kaelbling. "PDDL planning with pretrained large language models." In NeurIPS 2022 foundation models for decision making workshop. 2022.

[4] Dziri, Nouha, Ximing Lu, Melanie Sclar, Xiang Lorraine Li, Liwei Jiang, Bill Yuchen Lin, Sean Welleck et al. "Faith and fate: Limits of transformers on compositionality." Advances in Neural Information Processing Systems 36 (2024).

[5] Stechly, Kaya, Karthik Valmeekam, and Subbarao Kambhampati. "Chain of thoughtlessness: An analysis of cot in planning." arXiv preprint arXiv:2405.04776 (2024).

questions:
Are there details on the accuracy of the COTs generated by the LLMs?
</content>
</thread_object>

</thread>


Metareview:
metareview:
The paper presents a synthetic benchmark to evaluate temporal logic reasoning capabilities of LLMs. Whether LLMs indeed possess the ability to reason and to what to extent is an important question in the community and is gaining more and more attention. Reviewers all appreciate the importance of this direction. However, many benchmarks are proposed in the recent years. All the reviewers in some degree raise the concern about what is the unique value of this benchmark compared to other rule-based logic benchmarks. Besides testing some LLMs, reviewers hope, and I agree, that we would like to gain some further insights from those experiments. What weakness of LLMs does this benchmark expose, and how addressing this weakness can improve LLM's reasoning in general. More discussion on more experiments that provide insights of why LLMs fail on reasoning would definitely make this paper stronger. Hence, I recommend a rejection.