Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation

Authors: Chengwen Qi, Ren Ma, Bowen Li, He Du, Binyuan Hui, Jinwang Wu, Yuanjun Laili, Conghui He
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
Keywords: logical reasoning, symbolic provers, llms evaluation

Abstract:
First-order logic (FOL) reasoning, which involves sequential deduction, is pivotal for intelligent systems and serves as a valuable task for evaluating reasoning capabilities, particularly in chain-of-thought (CoT) contexts. Existing benchmarks often rely on extensive human annotation or handcrafted templates, making it difficult to achieve the necessary complexity, scalability, and diversity for robust evaluation. To address these limitations, we propose a novel framework called ProverGen that synergizes the generative strengths of Large Language Models (LLMs) with the rigor and precision of symbolic provers, enabling the creation of a scalable, diverse, and high-quality FOL reasoning dataset, ProverQA. ProverQA is also distinguished by its inclusion of accessible and logically coherent intermediate reasoning steps for each problem. Our evaluation shows that state-of-the-art LLMs struggle to solve ProverQA problems, even with CoT prompting, highlighting the dataset's challenging nature. We also finetune Llama3.1-8B-Instruct on a separate training set generated by our framework.
The finetuned model demonstrates consistent improvements on both in-distribution and out-of-distribution test sets, suggesting the value of our proposed data generation framework. Code available at: \url{https://github.com/opendatalab/ProverGen}

Decision: accept (poster)
Reviewer scores: 8, 6, 8, 3

Reviews and discussion:
<thread>
creation date:
1729986609614

thread_type:
official_review

<thread_object>
creator: reviewer_oqpi

<content>
summary:
This paper introduces ProverGen, a synthetically generated benchmark for deductive reasoning evaluation, which consists of 1.5K examples. ProverGen resembles prior work such as ProntoQA, where it generates a ground-truth reasoning path and then converts it into a deductive reasoning problem. On top of this, the authors use LLM to translate the rules and facts into NL statements based on a LLM generated background facts, making the problem more natural.

strengths:
see below

weaknesses:
## Novelty

As mentioned above, the creation of this dataset largely resembles that of ProntoQA. The main difference is the LLM translated facts and rules that make the statements semantically more natural and diverse. However, it is not sufficiently demonstrated how this aspect contributes to the novelty of this benchmark. It is unclear what limitations or insights of LLMs are revealed by this dataset that others could not. This, together with the quality and significance issues to be discussed below, significantly undermine the novelty of this work.


## Quality

There are several issues with the creation of the dataset.

Some FOL reasoning cases are potentially not covered by this benchmark:
- Judging from the pipeline and examples, the "goal" fact is an instantiated literal with unary predicate such as *Elegant(Sawyer)*, and *Swift(jack)*, but it does not cover cases with binary predicates or those with higher-order of arity, such as *FriendOf(Amy, Bob)*. It also does not cover cases of composite facts, such as *FriendOf(Amy, Bob) \land Person(Bob)*

Lack of dataset quality check:
- There lacks a check on whether the translated NL statement actually align with the ground-truth FOL rule
- Furthermore, the translated universal rule is only checked by an LLM on whether it aligns with commonsense. This could be noisy as the LLM can hallucinate.
- Without a quantitative measure on the quality of the translation, it is difficult to assess the dataset quality. At least one should provide the accuracy of the translation on a small held-out set that has manual annotations.

Finetuning results interpretation:
- As mentioned in the appendix, model finetuned on FOLIO is trained with only 1K examples, while the other two has 50K. I'm not sure if one can reliably draw any conclusion by comparing it with the other two as the training data difference is too big.

## Clarity

This paper is generally easy to follow.

## Significance

Another major concern of mine is the significance of this benchmark.
- This dataset contains only 1.5K examples with synthetically generated reasoning chains and NL translation that has no direct verification. While the authors generated a training set for experiments in section 5, it was not presented as part of the contribution and there also lacks direct verification on its quality and alignment. That said, this dataset really can only be used to evaluate an LLM on a specific reasoning task, i.e., deductive reasoning.
- Nevertheless, an evaluation dataset could also be a concrete contribution, but in order to be significant, it needs to reveal something new that was neglected and overlooked in other benchmarks, or bring new or significant harder challenges to the table. Unfortunately, this is not sufficiently demonstrated in the paper. Throughout the comparison in Table 1, ProverGen is on par with other benchmarks with only the hard set being somewhat more challenging. But where is the insight? Does the model fail because of an important property that is exclusively tested in ProverGen is missing? What can people learn from ProverGen about the LLM's reasoning capability that benchmarks fail to reveal?

That said, the authors need to address this issue before this work can be considered significant.

questions:
see above
</content>
</thread_object>

</thread>
<thread>
creation date:
1730264981987

thread_type:
official_review

<thread_object>
creator: reviewer_64s6

<content>
summary:
The paper proposes an automatic framework for generating high-quality datasets that adhere to First-order Logic principles, while also being scalable and diverse. The pipeline consists of three stages: Background Story Generation, Logic Skeleton Generation, and Statement Translation. Additionally, the framework introduces distracting premises into the dataset to enhance the comprehensiveness of the benchmark. Experiments show that state-of-the-art LLMs struggle with these logical reasoning tasks, and fine-tuning LLMs on this dataset leads to greater improvement compared to previous logical reasoning benchmarks. An ablation study is conducted to demonstrate the necessity of including distracting factors.

strengths:
I also work on logical reasoning, and I personally really like this paper. It addresses some key limitations of the previous benchmarks.

(1)	For the first time, this paper proposes an automatic pipeline that fully encompasses First-order Logic (FOL) relationships while being scalable and faithful. Additionally, it offers more natural and diverse language compared to previous benchmarks, as well as symbolic language, and includes a complete reasoning chain.

(2)	Experiments demonstrate that this benchmark poses a significant challenge to state-of-the-art LLMs.

(3)	Fine-tuning using this new dataset results in greater improvements compared to previous logical reasoning datasets, highlighting the advantages of the dataset.

(4)	It reduces the issues of disconnection and contradiction present in previous benchmarks, making the evaluation more reliable.

weaknesses:
I don't see any major weaknesses in this paper, but it could benefit from improvements in the following areas:

(1)	Some details require further clarification. When generating the logic skeleton, how are the facts and rules selected? Are they extracted from the generated background story? Providing more details on how the FOL relationships are incorporated at this step would help the reader better understand the process.

(2)	You mentioned that the bottom-up approach in previous work may result in disconnected and contradictory premises. This is a crucial point, as I have also encountered such cases while working on symbolic reasoning datasets. Is it possible to verify this claim with some data? For example, you could show the proportion of disconnected and contradictory cases in datasets like ProofWriter. I understand that, intuitively, the top-down method should generate fully connected logic. So alternatively, you could provide a qualitative analysis of why prior methodology tends to have this problem and how your method effectively addresses it.  Besides, regarding the issue of self-contradictory premises, since you include distracting premises, how do you ensure that these distractions do not lead to contradictory conclusions? While you mention that the distractions do not directly affect the core premises needed for the final conclusion, could they potentially introduce indirect contradictions?

(3)	It might be helpful to emphasize the importance of reducing disconnected and contradictory cases in your contribution, as they hinder the reliability of the evaluation.

(4)	Given the probabilistic nature of LLMs, the benchmark could be further improved by implementing a quality control process, particularly in the stages of generating the logic skeleton and translating FOL into natural language.

questions:
(1)	How are the facts and rules selected when generating the logic skeleton, and how do you incorporate the full set of FOL relationships at this stage?

(2)	Does the LLM introduce any errors when translating FOL statements into natural language, as well as during the Logic Skeleton Generation?

(3)	Is there any invalid case generated and is there a quality control process in place to filter out invalid cases?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730608933740

thread_type:
official_review

<thread_object>
creator: reviewer_bnmr

<content>
summary:
The authors propose a first-order logic reasoning data generation pipeline and introduce a reasoning benchmark/dataset called ProverGen. This pipeline combines symbolic provers with LLMs to generate scalable, diverse, and high-quality data. Mainstream LLMs are evaluated on this benchmark. Additionally, the authors trained a Llama3.1-8B model on a training set produced by the pipeline, and results show that ProverGen enhances both in-distribution and out-of-distribution logic reasoning abilities.

strengths:
1. The paper is well-written with clear presentation. The authors effectively explain how ProverGen differs from existing FOL reasoning benchmarks.

2. The main contribution is a novel top-down generation framework that creates logically coherent and diverse FOL problems, includes varying difficulty levels and two types of distractions, poses meaningful challenges, as SOTA models achieve only 50% accuracy on hard problems.

3. The experiements are clear and relatively sound. The authors evaluates multiple SOTA LLMs with both standard and chain-of-thought prompting, demonstrates improvement through model finetuning, shows generalization to out-of-distribution FOL tasks.

4. Provides reproducible results and promises to release code and dataset.

weaknesses:
1. The scope is relatively limited. Focuses exclusively on first-order logic reasoning, which may not fully represent real-world reasoning scenarios. Lacks evaluation on general reasoning benchmarks (e.g., MMLU, GSM8K, BIG-bench) to assess broader impact of training.

2. While in-distribution performance shows significant improvement after finetuning (>30% increase), out-of-distribution gains are marginal (5-8%). The modest OOD improvement suggests that training on ProverGen may not substantially enhance general reasoning capabilities. Questions remain about whether the skills learned from this benchmark can transfer to broader reasoning tasks.

3. Lacks detailed analysis of domain distribution in the generated dataset. The diversity of the generated data is not fully revealed.

questions:
1. Please discuss the points mentioned in the weakness section.

2. In the case study section, are there any statistics showing how many cases improved with the help of training?

3. Would changing the generation model from Llama3.1-70B-Instruct to a more advanced model make any difference?

4. Is this generation pipeline only helpful for building benchmarks, or can the synthetic dataset be used for future training?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730704225248

thread_type:
official_review

<thread_object>
creator: reviewer_nagl

<content>
summary:
The authors present a new method to generate first-order reasoning QA data to evaluate the reasoning abilities of LLMs. For each example, they utilize a synthetic generative process to produce the skeleton of the proof tree. They use an LLM to generate the subject and predicates of the example, where a seed subject and topic are sampled from public datasets of names and WordNet, respectively. The use of the LLM facilitates the generation of logical facts and rules that are consistent with the real-world and ensures the generated natural language sentences are linguistically diverse and realistic, in contrast with other synthetic data generation pipelines which use templates. Their generated dataset, called ProverGen, is demonstrated to be effective in measuring the reasoning abilities of LLMs.

Interestingly, the authors also show that fine-tuning models on ProverGen improves their OOD reasoning capabilities on datasets such as FOLIO and PrOntoQA.

strengths:
- The authors present a pipeline approach for generating QA data to test the reasoning abilities of LLMs.
- The natural language of the text in the examples generated by ProverGen are linguistically diverse and realistic, thanks to the use of an LLM in converting logical form into natural language.
- The authors ensure the proof tree of each example is correct by utilizing a symbolic prover (Prover9).

weaknesses:
- Some of the comparisons to previous work are not completely accurate (see questions below).
- The coverage of the output examples is not well described (i.e., the set of possible output proof skeletons, the set of deduction rules used for generation, etc).
- Since the described rules are specifically designed to be consistent with the LLM's background knowledge, the model can exploit background knowledge as a heuristic when solving examples from ProverGen.

questions:
I provide more detailed questions and comments below. The paper is well-written with only a small number of grammatical errors.

Table 1: While it is true that the provided data CSVs for PrOntoQA doesn't contain logical form annotations for each example, they do provide code to parse any sentence in the dataset into FOL logical forms (since each example was generated by converting logical forms into natural language sentences).

Line 86: "ProverGen’s difficulty setting demonstrates a fine-grained complexity"
  I understand the intended meaning of this phrase thanks to the part of the sentence that follows this phrase, but this phrase itself is somewhat difficult to understand on its own.

It would also be good to mention the disadvantage of data contamination for manually-annotated datasets. In addition, a discussion of how the proposed dataset relates to the problem of data contamination would be welcome.

Footnote 3: PrOntoQA avoids using real-world concepts to ensure the generated sentences do not contradict with real-world knowledge (i.e. the "fictional ontology" setting). They also provide true and false ontologies to specifically LLM behavior on examples that contain facts/rules that are consistent (or inconsistent) with the real-world.

Section 3.2.2: What are the set of possible deduction rules from which proof steps are sampled? Are deduction rules involving universal and existential quantifiers generated? I assume since the authors claim ProverGen has coverage over all connectives and quantifiers in FOL, that there is at least one possible deduction rule for each connective and quantifier. More broadly, what are the completeness properties of this proof skeleton generation procedure? What are the kinds of proofs that can and cannot be generated?

Line 303: "we opt to the specific rule" -> "we opt for the specific rule"

Have the authors experimented with more than 2 few-shot examples in the prompt? If so, were there any significant differences in behavior?
</content>
</thread_object>

</thread>
<thread>
creation date:
1732209454638

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Updated Manuscript and Response to all reviewers:

comment:
We thank all the reviewers for their valuable feedback and thoughtful comments on our paper. We have uploaded a revised PDF of the paper. All revisions have been clearly marked using red font and formatted as [Revision: xxx] to facilitate easy identification.
</content>
</thread_object>

</thread>
<thread>
creation date:
1732972789950

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Rebuttal summary

comment:
We sincerely appreciate all the reviewers for their thorough evaluations. The constructive suggestions have greatly enhanced the quality of our work, and their positive feedback is especially inspiring for us.

We are pleased to note that reviewers have recognized:

- Our paper's success in addressing key limitations of previous benchmarks, such as unnatural and monotonous language, the absence of symbolic language and complete reasoning chains, and disconnected or contradictory premises (Reviewers NAgL, BNmr, 64s6).
- The novelty of our framework (Reviewers NAgL, BNmr, 64s6), and the clarity and quality of the paper's presentation (all Reviewers).
- The experiments as interesting, clear, and sound (Reviewers NAgL, BNmr).
- The high quality of the ProverGen dataset, along with scalability, diversity, and faithfulness (Reviewers NAgL, BNmr, 64s6).

We have carefully addressed the concerns and questions from each reviewer, providing detailed responses. Based on this valuable feedback, we have revised the paper with the following updates (highlighted in red for easy identification):

- Discussed data contamination issues in manually-annotated datasets and how our framework addresses them, thanks to Reviewer NAgL's insightful suggestion.
- Emphasized the importance of reducing disconnected and contradictory cases, as suggested by Reviewer 64s6.
- Introduced a new section detailing the quality control process in our framework, in response to questions from Reviewer 64s6 and oQpi.

Once again, we would like to thank all the reviewers for their time and efforts in helping us enhance the paper!
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper proposes a method to generate first order reasoning QA dataset to evaluate the reasoning abilities of LLMs. Whether LLMs indeed learn to reason has been an important topic for at least 2-3 years. Here, there are a few main considerations. First, how to truly verify whether a LLM reasons. Second, is the result generally applicable to some other datasets. Third, can the dataset be beneficial to improve LLM reasoning. This paper in general is well written and easy to follow. And technically, this paper does a solid answer to all of the three main considerations above. The proposed method is novel and generative in its nature, which potentially can alleviate the problem of data pollution. Furthermore, the generated proof tree is guaranteed to be correct. And the OOD-results is somewhat encouraging. In terms of the limitations, I would encourage the authors to further expand the dataset and include more comparison with more LLMs and do a more comprehensive analysis with other datasets that also highlight reasoning. The comparison could provide more insights.