Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation
logical reasoning;symbolic provers;LLMs evaluation
Yes
No ethics review needed.
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?
- 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).
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.
- 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.
Yes
No ethics review needed.
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?
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.
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.
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.
Yes
No ethics review needed.
(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?
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.
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.
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.
Yes
No ethics review needed.
see above
see below
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.
## 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.
We propose a framework for generating diverse and human-like high quality first-order logic dataset by combining LLMs and a symbolic prover.
@inproceedings{
anonymous2024large,
title={Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation},
author={Anonymous},
booktitle={Submitted to The Thirteenth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=C25SgeXWjE},
note={under review}
}
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 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, ProverGen. Our evaluation shows that state-of-the-art LLMs struggle to solve ProverGen 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\footnote{We will release our code as well as the dataset.}.
I certify that there is no URL (e.g., github page) that could be used to find authors’ identity.
I acknowledge that I and all co-authors of this work have read and commit to adhering to the ICLR Code of Ethics.
logical reasoning symbolic provers LLMs evaluation
I certify that there is no acknowledgement section in this submission for double blind review.
/pdf/e4930cef23f71736b4f25a5425179264b955200f.pdf
neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
I understand the reciprocal reviewing requirement as described on https://iclr.cc/Conferences/2025/CallForPapers. If none of the authors are registered as a reviewer, it may result in a desk rejection at the discretion of the program chairs. To request an exception, please complete this form at https://forms.gle/Huojr6VjkFxiQsUp6.
I certify that this submission complies with the submission instructions as described on https://iclr.cc/Conferences/2025/AuthorGuide.
/attachment/1acf0ccb3ae41519285493612d188c6f7c661863.zip
Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation
ICLR 2025 Conference Submission
ICLR.cc/2025/Conference/Submission