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
Venue: ICLR 2025 Poster (2025)
Keywords: logical reasoning
symbolic provers
LLMs evaluation
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We propose a framework for generating diverse and human-like high quality first-order logic dataset by combining LLMs and a symbolic prover.

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}

Published as a conference paper at ICLR 2025
LARGE LANGUAGE MODELS MEET SYMBOLIC PROVERS FOR LOGICAL REASONING EVALUATION
Chengwen Qi Ren Ma
Bowen Li
He Du
Binyuan Hui
Jinwang Wu'
Yuanjun Laili 1455 Conghui He
!Beihang University SShangaai Artificial Intelligence Laboratory
FFudan University *Zhongguaneun Laboratory
State Key Laboratory of Intelligent Manufacturing Systems Technology, Beijing [Chengwen.qi, {maren, libowen, heconghui 88p jlab.or
jun) sequaa.edu.co eddu.cn
ABSTRACT
First-order logic (FOL) reasoning, which involves sequential deduction, is pivotal for intelligent systems and serves as a valuable task for evaluating reasoning ca- pabilities, particularly in mmain-of-thougee (CoT) contexts. Existing benchmarks often rely on extensive human annotation or handcrafted templates, making dif- fieult to achieve the necessary complexity, scalability, and diversity for robust evaluation. To address these limitations, we propose a novel framework called ProverGien that synergizes the generative strengths of Large Language Models (LLMs) with the rigor and precision of symbolic provers, enabling the creation of scalable, diverse, and high-quality FOL reasoning dataset, ProverQA. ProverQA is also distinguished by its inclusion of accessible and logically coherent interme- diate reasoning steps for each problem. Our evaluation shows that state-of-the oh-the-art LLMs struggle to solve ProverQA problems, even with CoT prompting, highlight- ing the dataset's challenging nature. We also finetune Llama3.1 1-8t-Isstuttt on a separate training generated by our framework. The finetuned model demon- strates consistent improvements on both in-distribution and -utoo--distribution test sets, suggesting the value of our proposed data generation framework. Code avail- com/ httpp/ennnnaaaaaaeeeeeeeeeeeeeee
able at:
INTRODUCTION
First-order logic (FOL) reasoning, which involves sequential deduction and the application of facts and logical rules to derive conclusions or make decisions, is a fundamental aspect of human intelli- gence (Saparov & He 2022 Pan et al. (023). The complexity of performing multi-step reasoning while maintaining logical coherence across these steps makes FOL reasoning an ideal testbed for evaluating the reasoning capabilities of Large Language Models (LLMs), particularly in scenarios such as Chain-of- Chain-of-Thought (CoT) prompting (Wei et al. 2022) and planning (Wang et al., 2024] Valmeekam et al. 2022). An effective benchmark for FOL reasoning should satisfy several key criteria: (1) Scalability, enabling expansion in both volume and complexity with minimal manual intervention; (2) Natural and Diverse Language, capturing a wide range of natural language ex- pressions to reflect real-world linguistic variability; (3) Symbolic Representations, providing formal symbolic structures that can be validated through automated symbolic provers, ensuring dataset integrity and supporting downstream tasks like NL-FOL translation and tool based logic problem solving (Pan et al.] 2023 Olausson et al.) 2023);; and (4) Faithful Reasoning Chains, where each instance includes intermediate reasoning steps clearly articulated in both symbolic and natural lan- guage formats, promoting transparency and facilitating further model training.
However, existing FOL. reasoning datasets only partially fulfill these requirements (see Table | for more details). Template-based datasets such as ProntoQA (Saparov & He 2022 Saparov et al.]
2024
Proo/Writer (Tafjord et al. 202T), and RuleTaker (Clark et al. 202 are scalable but often
Equal contribution
Corresponding authors

---

Published as a conference paper at ICLR 2025
lack diversity and rely overly simplistic rules. On the contrary, manually curated datasets like FOLIO (Han et al. 2022) offer rich diversity in natural language expressions and more complex logic rules, but they are limited in size due to the extensive human effort needed for creation. Additionally, data contamination is also a significant issue in manually annotated datasets, as it is difficult to update them frequently. This limitation due to potential data leakage. Another common limitation across previous datasets is the lack of well-defined and easily accessible reasoning chains. FOLIO, for instance, does not provide any reasoning chains, while ProofWriter and RuleTaker include reasoning chains, but they are not readily accessible and require users implement additional code to extract them for each problem.
lead to biased evaluations and hinder true generalization
Table 1: Comparison of existing FOL reasoning datasets with ProverQA.
Creation
Natural & Diverse
Symbolic Representations
Faithful
Dataset
Scalability
Method
Language
Reasoning Chains
RuleTaker
Synthetic
ProofWriter
Synthetic
X
ProntoQA
Synthetie
ProntoQA-OOD
Synthetic
X
LogicNLI
Synthetic
FOLIO
Manual
ProverQA
Synthetic
To address these gaps, we propose novel framework that leverages the strengths of LLMs and sym- bolic provers to generate an extensible, diverse, and high-quality dataset for FOL reasoning. While LLMs have been increasingly utilized for synthesizing datasets across various tasks (Taori et al.)
2023 Acharya et al. 2023 Gajjar & Shah 2024). they fall short in producing reliable reasoning,
often lacking faithfulness and transparency (Golovneva et al. 2022 Ribeiro al, 2022 Lyu al.
2023), particularly when it comes to long reasoning chains. On the other hand, symbolic provers are known for their reliability and precision in executing complex logical inferences. By combining the generative capabilities of LLMs with the rigor of symbolic provers, our framework offers a robust solution for producing FOL reasoning data that ensures both diversity and logical soundness. also mitigates the data contamination challenge by enabling the generation of new datasets using diverse models and controlled complexity, ensuring that the datasets remain fresh and uncontaminated. Our framework follows a structured three-step pipeline: (1) we first use an LLM to generate a unique background story for each problem based on a given subject and a characteristic keyword; (2) we employ symbolic prover (i.e., Prover9) to construct reasoning trees and compute the truth values of relevant facts; and (3) we utilize an LLM to translate these logical expressions into natural language statements.
We use 100na3..-70B-Instruue within our proposed generation framework to create a new FOL rea- soning benchmark, ProverQA, consisting of 1,500 instances across three difficulty levels: easy, medium, and hard. We evaluate ProverQA on several state-of-the-art (SOTA) LLMs and find that with CoT prompting, models barely exceed 50% accuracy the hard subset, highlighting the significant challenge posed by ProverQA. ProverQA's difficulty settings are carefully designed to ensure appropriate complexity, avoiding both performance saturation and uninformative under- performance (c.g., random guessing). enabling accurate evaluation of both powerful and smaller language models' reasoning abilities. To further explore the potential of our proposed generation framework, we finetune Llama3. -8B--Instruct observe substantial performance gains on in in-distribution (ID) evaluations. Remarkably, this fine- tuned model also shows consistent improvements out-of-distribution (OOD) test sets, signifi- cantly outperforming the same model finetuned on other existing FOL training sets.
separately generated ProverQA training set and
RELATED WORKS
Logical Reasoning Datasets Logical reasoning is fundamental ability of intelligent systems and researchers have proposed a number of datasets to evaluate logical reasoning abilities language models. These datasets be divided into two groups: manually crafted ones and automatically
2

---

Published as a conference paper at ICLR 2025
generated ones. cranted datasets typically sourced from existing examinations Yuu et al.
2019 Liu et al. 2021 2023 Zhong et al. (02I) or directly written by domain experts (Hu et al.
2023
Han et al. 2022 Although they often exhibit higher quality and complexity. they also suffer
from limited quantity and high creation costs. Automatically generated datasets are often created
using rules and predefined natural language templates (Sinha et al. 22099 Hahn et al. 2021 Clark iet al. 2021 Tafjord et al., [022]] Tian et al. [022]] Saparov & He 2022 Saparov et al. 2024 Sun
al., 2021). While these datasets enable automatic problem generation, they often lack linguistic
diversity and are constrained by rigid, monotonous rules. None of them cover all aspects of first- order logic, and they cannot be used to generate problems with more complex rules.
Symbolic Prover Augmented LLMs Symbolic provers are computer programs used to gen- erate proofs and solutions of mathematical theorems automatically. In logical reasoning prob- lems, symbolic provers, such as SymPy (Meurer et al. 2017). Z3 (De Moura & Bjømer 2008), Lean (De Moura et al.] 2015), Pyke (Frederiksen) 2008 and Prover9 (McCune 2005). stand out with faithful solutions and traceable intermediate processes. Recent works (Pan et al. 2023 Olaus- son et al. 2023 Ye et al. 2024 Zhang et al.) 2024) combines LLMs and symbolic provers to solve logic reasoning problems. They LLMs to translate problems from natural language into sym- bolic representations and then solve that problem with a symbolic prover. In contrast to previous works that utilize symbolic provers solely as problem solvers, our approach integrates symbolic provers into the generation process of first-order logic (FOL) problems. This integration allows us to bypass the intricate interrelations and couplings among logical relations, enabling the generation of diverse rules and their correct chaining to form comprehensive problems.
3 METHODOLOGY
3.1 TASK FORMULATION
Given a set of premises P, consisting of facts F and rules R., denoted as P = (F, the goal of FOL reasoning is to determine whether given goal G (which can a fact or a rule) is True, False, or Uncertain. Specifically, F = [2,, f2. fm represents set of facts, where each fact fi (1 S i < m) is a declarative statement describing attributes or characteristics of subjects. For example, Sawyer has good dance skills is fact that specifies the attribute (has good dance skills) of the subject (Sawyer). Similarly, R = {ri, T2. F'a] comprises a set of rules, where each rule ry (1 و S n) defines relationships between multiple facts using seven FOL symbols: conjunction (A), disjunction (V), negation (-), implication (-), equivalence (=) universal quan- tifier (A), and existential quantifier (3). For example, the rule If Sawyer has good dance skills and has chari sma, ther. he is a successful dancer illustrates a rela- tionship between two facts and their conclusion. It is worth noting that some existing datasets, such as ProntoQA (Saparov & He (022) and ProofWriter (Tafjord et al., 202T], do not fully encompass all seven FOL relationships, whereas our proposed framework ensures complete coverage.
3.2 LLM & PROVER-EMPOWERRD GENERATION FRAMEWORK
Our proposed generation framework, which integrates the generative capabilities of LLMs with the precision of symbolic prover, generates FOL reasoning problems through structured three- stage process, as illustrated Figure [ First, a background story created for each problem using sampled subject names and keywords to ensure linguistic diversity. In the next stage, the logic skeleton generation employs a symbolic prover (i.e., Prover9) to construct reasoning trees and determine the truth values of the relevant facts. Finally, the statement translation phase uses LLMs to convert these logical expressions, including both premises and goals, into natural language, ensuring clarity and coherence. An example of generated FOL problem is shown in Figure 2
3.2.1 BACKGROUND STORY GENERATION
Achieving naturalness in language expression is crucial for creating a plausible FOL dataset. Ex- isting approaches often rely on extensive human annotation or rigidly structured templates. For in-
In line with previous datasets, replace equivalence (=) with exclusive disjunction (0), which can be interpreted as combination of equivalence (=) and negation (-): fi f2 = -(fi = fa)
3

---

Published as a conference paper at ICLR 2025
Subject Name
Keyword
Top-down Generation Bottom-up Reasoning ng
Facts
Rules
Distractions
Background
GOAL
LLMs
Expression Sampling
LLMs
Truth Value Calculation with Prover9 Distraction Generation
Generated Background
Translation Process
fi)
BackgroundSSoon
Rules
e
Sawyerwas was
Instantiation
charismatic and elegant,
(di @ di) f
True
True
dancer who ruled the ballroom scene 19th-
poet(Sawye) musician(Swwye)
Translation
century Paris, into family of modest means, he discovered his passion for dance yound age and worked tirelessly to hone skills. Sawyer's big break came when he was invited perform at the prestiglous Opéra Garnier, His dashing
Universal Rule
di
Uncertain
True
fr f
Everyone is aither a musician or poet, but
not both.
LLMs X
Specific Rule
Sawyer either musician not both
LLMs
(do
fs f
Facts
Instantiation
poet(Sawyer)
Sawyer poet
False
Uncertain
True
Translation
(a) Background Story Generation
(b) Logic Skeleton Generation
(c) Statement Translation
An overview of our ProverGen framework. (a) Background Story Generation (Section 3.2.1 Given a subject, Sawyer, and a seed keyword, elegant, LLMs generate background
Figure 1:
story to establish context and ensure linguistic diversity. (b) Logic Skeleton Generation (Section 3.2.2 A top-down approach is used to generate the logic skeleton, forming the reasoning tree for the FOL problem. This involves two iterative steps: expression sampling and truth value calculation using the Prover9 prover. Distractions are also incorporated to test the robustness of model's reason- ing capabilities. (c) Statement Translation (Section (32.3). LLMs translate the facts and rules from the logic skeleton into natural language, guided by the previously generated background story. Each rule translated into a universal version and specific version. The universal version is preferred if' it does not contradict with common sense, otherwise the specific one is selected.
stance, ProntoQA (Saparov & He 2022) and ProofWriter (Tafjord et al. 2021 employ handcrafted templates, which result in datasets lacking linguistic diversity and naturalness
In contrast, FOLIO (Han et al. 2022) retrieves documents from Wikipedia and manually extracts facts and rules. However, this process requires substantial human effort and is susceptible to syn- tactic typos and reasoning errors introduced during annotation, as observed FOLIO. Additionally, models may exploit shortcuts by leveraging pre-trained knowledge predict answers directly, by- passing rigorous logical reasoning (Qi et al. 2023 Geirhos et al. 2020), since the facts and rules in the dataset are often derived from the real-life.
To efficiently synthesize plausible natural FOL problems, we leverage L.MMs to generate a unique background story for the subject of each problem, which serves instantiate the statements (both premises and goals) within the problem. However, simply prompting LLMs to generate stories without any guidance can be suboptimal, as they struggle produce diversified content with high quality, as noted Jenzzsch & Kersting (2023); Sudalairaj et al. (2024). To mitigate these issues, we prepare characteristic keyword for the subject within the problem to guide the generation, Specif- ically, the process begins by assigning unique name to the subject, which is randomly sampled
Booth Proo/Writer and PrOntoQA generate natural language expressions by using predefined templates for each logical rule. For example, for a rule like + B, they may define a template such as Every & B, and then randomly select words to replace A and B. PrOntoQA intentionally avoids real-world concepts to prevent confficts with realdworld knowledge. They also evaluate LLMs' behavior on examples that contain facts and rules that consistent (or inconsistent) with the real-world knowledge. In contrast, ProofWriter does incorporate such mechanism.
4

---

Published as a conference paper at ICLR 2025
from publicly accessible datasets of human names and pet name Next, sample keyword from WordNet (Miller 1995) to serve as a defining characteristic or attribute the subject, ensur- ing semantic diversity the generated content. These elements, the name and the characteristic keyword, are then integrated into the prompt to guide LLMss to generate a contextually rich and var- ied background story. This controlled generation helps promote diversity in the dataset. The detailed prompt used in our experiments is outlined in Appendix
Premises
Reasoning Process
Sawyer has charisma. (f2) Sawyer performer. (fs)
Sawyer is (f-)
Step1
charismu(Sowyer)
performer(Saxyed
(Sel(Sawyer)
if Sawyer is performes, then he oither has good dance skills is musician. (fs - F-))
Fact: Sawyer is post. (fe)
performer(Sowwer (geod donce skills(Sawyer) @ musician(Soayer)
Rule: Sawyer either musician poet, not bath. (f4 @ f6)
Sawyer either musician poet, but not both. (T+ @ fo)
poet(Sowyer) @ musiclan(Sawyee
Conclusion: Sawyer is not musician, (-f4)
if Sawyer has good dance skills and has charisma, then he is successful dancer. (ffi fi) ff) (good dencee (kills/Swwssss charisma(Sowyee)) successfu
Step2
Fact: Sawyer is performer. (f+)
Distractions (Type
Sawyer not musician. (-f4)
James has charisma. (di) charisma
Alice is poet. (dk)
Rute: Sawyer performer, then he either has gond cance skills or is musician, but not both. (fs (fi fa))
(pe((Alice)
Distractions (Type II)
Conclusion: Sawyer has good dance skills, (f)
someone either sings opara or plays instrument, then musician ((ds
Step3
Vix (sings operafs) plays instrumentóx) musicianó0
Everyone who either practices waltz or masters tango has good dance skills ((sh @ dz) +
Sawyer good skills,
(prectices, waltz() mesters_tongabbk tangofd) + good dance skills(0)
mosters
Fact: Sawyer chrisma
Savyer masters tanga (da)
Sawyer (de)a.(d.) sings opere(Sawye)))
Fawayyr gaod charisma, then he is successful dancer. (fft f2) fs)
mosters tongofsowyerd
Goal
Goal
Sawyer successful dancer
Sawyer is a successful dancer.
(a) A Generated FOL Problem
(b) Reasoning Process
Figure 2: A generated FOL problem (a) with its corresponding reasoning process (b).
3.2.2 LOGIC SKELETON GENERATION
Logical soundness is a fundamental requirement in constructing a robust FOL reasoning dataset. While LLMs are highly proficient generating natural language, they often fall short in maintain- ing logical coherence, particularly when dealing with intricate, multi-step reasoning processes. To address this limitation, we introduce a novel approach that integrates symbolic prover into the data generation pipeline, allowing for the construction of logically rigorous FOL reasoning problems.
In our data generation framework, we start with constructing logic skeleton for each problem, rep- resented reasoning tree with the ultimate goal at its root (as shown in Figure [(b).. Previous works typically generate reasoning problems in bottom-up approach by starting with premises and building toward conclusions. We argue that this approach could be flawed as it can often result in disconnected or contradictory premises, making it difficult to ensure that all facts are logically coher- ent with each other. For instance, if the problem includes facts such as fi: Sawyer is a poet, fa: Sawyer comes from Mars, and fa: Sawyer is a large, fluffy Maine Coon cat, then integrating these elements into consistent reasoning chain is challenging. Therefore, framework adopts novel top-down approach, which begins with the goal and works backward to derive the relevant premises and rules needed logically support that goal. This method ensures that each fact and rule contributes directly to the reasoning process, improving both the coherence and logical soundness of the generated problems. Moreover, this top-down structure simplifies the problem of logical consistency by allowing LLMs to focus on facts that are directly relevant to the conclusion, without needing to reconcile them with unrelated information.
More specifically, as shown in Figure [bb.. we begin by setting the truth value of the goal, denoted as fs True, and treat this as the root node of the reasoning tree. Next, we sample a logical expression
jaon
5

---

Published as a conference paper at ICLR 2025
for this node, (f) - fa. which establishes relationship between the goal fa and the premises fi and f2. At this stage, we use the symbolic prover Prover9 to calculate the truth values of fi and f2. ensuring that the premises logically support the goal. Once fi and fz are assigned truth values, they become the current nodes in the reasoning tree. For each of these nodes, we continue the process by sampling new logical expressions. For instance, for fi True, we sample a new rule fs + (fi @ fa), where fo and fa are additional facts to be evaluated. We then calculate the truth values for these new premises using Prover9, and they become the next current nodes in the tree. This iterative process is repeated for each current node, expanding the reasoning tree step by step. The process continues until we have generated the desired number of reasoning steps, ensuring that each layer of the reasoning tree is logically consistent and fully developed, forming coherent and complete logical structure for the problem.
To further assess the robustness of models in handling FOL. reasoning, we introduce distractions into the generated problems. Distractions, denoted as d, are an additional set of facts and rules not essential to solving the problem. The inclusion of distractions forces models to distinguish between relevant and distracting information. We implement two types of distractions in our framework. The first type follows existing works (Tafjord al., 2021 Saparov & He, 2022), where we randomly introduce facts or rules that are related to the problem domain but use a different subject name (see Figure 2). The second, more complex type of distraction leverages the power of symbolic provers to introduce facts and rules that are semantically or logically related to the reasoning chain, but which lead to an Uncertain judgment. This type of distraction requires models to reason over logically relevant information that does not directly impact the truth value of the core facts needed reach the final conclusion. For instance, suppose fi is critical fact in the reasoning tree, and we introduce two distractions, d1 True and d2 Uncertain, with the rule (d2 @ d2) - fi. Here, the truth value of fi remains Uncertain because the rule involves incomplete information. Models must reason through these distractions, yet ultimately recognize that they do not alter the critical facts that drive the reasoning chain forward.
3.2.3 STATEMENT TRANSLATION
After generating the logical skeleton of problem, we use LLMS to translate each rule and fact into natural language within the framework of the background story generated in Section 3.2.1 As illustrated in Figure [c), we first prompt LLMs to instantiate placeholders (such as fe and fa) in the logic expressions with appropriate predicates, like poet and musician. Once the placeholders are instantiated, the logic expressions are translated into natural language. To maintain consistency throughout the translation process, we provide the previously translated facts and rules as references in the prompt for subsequent translations (details of the translation prompt can be found in Appendix B
To ensure the plausibility and soundness of the rules, we instruct LLMs to generate two versions of each rule: universal and specific version. The universal rule refers to statements that apply to everyone or everything, such as Everyone is either a musician or a poet, but not both. The specific rule, on the other hand, applies to an individual subject, such as Sawyer is either a musician or a poet, , but not both. LLMs then assess whether the universal rule aligns with common sense. If it does, we use the universal version; not, we opt for the specific rule. For instance, the universal rule in Figure does not align with common sense (as there are more professions than just musicians and poets), so we choose the specific version of the rule. The final stage of the proposed framework involves assembling the facts, rules, and distractions generated in previous stages into a complete FOL problem. An example of the constructed problem with its corresponding reasoning steps is provided in Figure? 2
3.3 THE PROVERQA BENCHMARK
We utilize Llama3.1 Instruct throughout our proposed generation framework to develop new FOL reasoning benchmark, ProverQA, comprising 1,500 instances. The benchmark is evenly di- vided into three subsets based on the length of the reasoning chains: easy (1-2 steps), medium (3-5 steps), and hard (6-9 steps). In addition to the number of reasoning steps, the hard subset is char- acterized by more diverse reasoning directions. Reasoning in the easy and medium subsets typically follows a straightforward left-to-right progression. For example, given fi = True and fi > fa. the model can deduce that f2 True. In contrast, the hard subset involves more complex patterns,

---

Published as a conference paper at ICLR 2025
requiring models to infer fi False given f2 False and fi f2. thus demonstrating more intricate reasoning process. Each problem in the benchmark contains two types of distractions (see Section 3.2.2). where the number of distractions for each type is randomly sampled. Moreover, to further challenge the robustness of models, we shuffle the order of the premises within each prob- lem, ensuring that models cannot exploit fixed patterns sequences derive conclusions. Detailed examples of the ProverQA are provided in Appendix D
4
EVALUATION ON THE PROVERQA
4.1
EXPERIMENTAL SETUP
We evaluate current
SOTA
proprietary LLMs (GPT-4o OOpenAl 2024) and
Claude3.5 Anthropic
2024
and open-source LLMs (Mistral Inst ruct. (Jiang et al. 2023
Distral-Laage--nstt-ee
2024 and Llama3. 1-BBhhttt, Llama3. 1-70B-c-- (Dubey et al., 2024 on the ProverQA. We utilize two prompting strategies: Standard and CoT. Standard prompting uses 2-shot in-context learning to prompt LLMS to answer questions directly, whereas CoT prompting employs 2-shot examples instruct the model to solve questions step by step. Examples of both prompting strategies can be found in Appendix
4.2
MAIN RESULTS
Table 2: The performance of LLMs on ProverQA and existing FOL reasoning datasets. The average performance improvement of CoT prompting over Standard prompting across models each evaluation set, which indicates the average gain CoT prompting brings on each set.
ProverQA
ProntoQA
ProofWriter
FOLIO
Avg
Easy
Medium
Hard
Standard Prompting
GPT-4o
87.20
68.60
46.20
91.80
56.33
67.86
69.66
Saude-3.5-Somne
85.00
68.20
42.80
88.60
55.00
77.85
69.58
Llama3.1 1--aaB...BBBBB- -nstruutt
46.60
43.00
39.00
50.40
43.80
54.29
46.18
Llama3. 1rrma3.1-70B... -nstuet
82.00
64.20
47.60
80.60
50.33
67.86
65.28
Mistral-7B-Inntrucct
56.80
46.80
37.20
50.00
42.33
54.29
47.90
Mistral-Large-Inntruett
84.60
69.20
49.60
71.00
60.33
77.14
68.65
Mixtral-8x22B-IInstru
75.40
57.40
39.00
65.20
40.17
74.29
58.58
CoT Prompting
GPT-4o
94.20
79.40
50.00
100,00
67.33
72.
77.18
Claude-3.5-Somme
95.20
83.60
56.40
99.20
76.33
80.71
81.91
Llama3.1 I-8t-tnstruct
75.60
46.60
33.60
79.60
56.83
63.57
59.30
Llama3.1-70B-- 1-7tt--Istt
90.40
73.20
46.80
95.40
71.17
74.29
75.21
Briraal-BBInnstuue
72.00
51.00
41.80
61.20
46.00
63.58
55.93
Mistrall-arge-Instruet
92.60
75.80
52.20
98.60
73.50
83.57
79.38
Mixtral-8x22B Instrucct
87.60
66.80
47.60
79.60
57.67
73.57
68.81
Avg 1
12.86
8,43
3.86
16.57
14.36
5.41
10.25
ProverQA as New Challenge Overall, model performance on ProverQA declines as problem difficulty increases, with the lowest scores observed on the hard subset across all existing datasets as seen in Table Specifically, strong models such as GPT-4o, Claude-3.5-Somee Instruct barely exceed 50% accuracy on the hard subset, even with CoT prompting. This result
and Mistral-Large
*The version of GPT-4o used in our experiments is 200t-40-2024-0--00 and the version of C1 c1aude3.5 5 used is cl alade---- 3-55e-3-5-- 3-5-sonnet- -2024060002000.

---

Published as a conference paper at ICLR 2025
indicates that even the most advanced LLMs perform poorly sufficiently complex problems with long reasoning chains. contrast, simpler benchmarks like ProntoQA appear to be nearly solved by models like GPT-4o and Claude-3.5-Sonnet However, smaller models still struggle achieve satisfactory performance, even on the easy subset of ProverQA, suggesting that these models are not yet equipped to handle FOL reasoning effectively.
Comparison of prompting strategies Compared with Standard prompting, CoT prompting no- tably enhances the performance of models on easy datasets but does not yield a similar improvement harder datasets, as presented in the last of Table The improvement more pronounced because performance on easy problems is probably limited by the CoTT capability, whereas the bottleneck for hard problems may involve other factors beyond CoT capability. We have also conducted experiments using 5-shot examples; the results can be found in Appendix
the easy dataset is
4.3 ABLATION STUDY ON DISTRACTIONS AND PREMISE ORDER
By default, the ProverQA benchmark includes two types of distractions and shuffles the order of premises within each problem (see Section 3.3). To assess how these two factors influence the evaluation results of LLMs, we conduct ablation studies using GPT-4o with Co7 prompting in this section. Specifically, in the first setting, we remove all distractions from the problems observe how the absence of irrelevant information affects the model's 's reasoning performance. Results in Table B exhibit that the model performs better this situation. In the second setting, we additionally reorder the premises to match the logical progression of the underlying reasoning chain. This turns out that the model performs even better when premises are presented a coherent sequence. Consequently, these findings suggest both factors are valuable for constructing robust FOL reasoning benchmark for LLMs.
Table 3:
Performance of GPT-4o on different variants of ProverQA using CoT prompting. The first row represents the default ProverQA setting, which features distractions and shuffled premises.
Distractions
Shuffled Premises
Easy
Medium
Hard
/
94.20
79.40
50.00
/
94.40
82.20
57.40
X
X 95.60
87.40
62.40
5 FINETUNING WITH PROVERQA TRAIN DATA
Beyond its role as evaluation benchmark, also investigate whether the training data synthe- sized by our proposed framework can improve model's FOL. reasoning capabilities, particularly in out-of-distribution (OOD) scenarios. To this end, we generate dedicated training set and finetune an open-ponneee open-source model, existing FOL reasoning datasets, such ProofWriter and FOLIO. We exclude ProntoQA from this experiment due to the absence of a publicly available training set. Detailed training configurations provided in Appendix
For comparison, we also finetune the same model on
5.1 EVALUATION RESULTS
In-Distribution (ID) Performance As shown in Table finetuning the ProverQA training set results in a substantial performance improvement across all subsets of the ProverQA benchmark. Specifically, the model's performance increases by 21.4%, 44.0%, and 34.6% in the easy, medium, and hard subsets the ProverQA benchmark, respectively. Similarly, fine-tuning on ProofWriter and FOLIO leads to performance gains on their corresponding test sets, expected.
(OOD) Performance While the ID performance of finetuned models can exhibit the positive effeets of specialized finetuning, OOD performance provides more insights as it demonstrates the generalizability of the finetuned models. As shown in Table 4 finetuning
8

---

Published as a conference paper at ICLR 2025
Table 4: Performance of Llama3.1-88 1-8t-rnttrcctt finetuned with different FOL. training sets. Green cells indicate in-distribution (ID) evaluation results, while red cells represent out-of- distribution (OOD) evaluation results. The change of performance after finetuning is shown in small fonts along with the evaluation results. f: the average change of performance across all OOD evaluation sets for each training configuration.
FOL Training Set
ProverQA
OOD Avg A
ProntoQA
ProofWriter
FOLIO
Easy
Medium
Hard
Llama3. 1-8B- SB-Instruct
75.60
46.60
33.60
79.60
56.83
63.57
Finetuned Llama3. 1-8B-Instruct
ProofWriter
44.60
55.00
47.20
92.00
71.67
+14.8
50.00
-13.8
-2.0
FOLIO
53.20
-22.4
44.80
-1.8
31.00
-2.6
63.40
-16.2
42.83
-14.0
70.00
+6.4
-11.4
ProverQA
97.00
+21-4
90.60
+41.0
68.20
+34.6
88.40
+5
65.67
+8.8
68.57
+5.0
+7.5
ProverQA yields performance increase on OOD test sets (ProntoQA. ProofWriter, FOLIO) by about 5% to 8.8%. Finetuning on ProverQA obtains the best OOD improvement on average with large leading margin compared models finetuned ProofWriter and FOLIO, indicating the limited utility of these prior datasets for promoting the reasoning capabilities of LLMs. The model finetuned on ProofWriter achieves the highest performance ProntoQA. This anomaly could be attributed to the high similarity between ProntoQA and ProtfWriter: Both datasets utilize predefined templates for generating logic and corresponding natural language.
5.2
CASE STUDY
We show examples from the FOLIO test set in table demonstrate how finetuning on ProverQA improves model performance. Before finetuning, models fail to solve the problems because of various reasons, such as using a common sense shortcut, being unfaithful to the context, and being unable to extend the reasoning chain. After training on ProverQA, models are able to derive valid reasoning chain up to the goal based on the context, and the reasoning process rigidly adheres to the facts and rules.
CONCLUSIONS
In this work, presented novel framework called ProverGen for automatically generating FOL reasoning datasets by leveraging the strengths of LLMs in producing diverse natural language ex- pressions and the rigor of symbolic provers in ensuring logical consisteney. Using this framework, we developed ProverQA, a high-quality FOL reasoning benchmark that is both extensible and di- verse. ProverQA encompasses complex rules, diverse natural language expressions, and faithful intermediate reasoning chains, providing comprehensive evaluation benchmark for FOL reason- ing. Our evaluation shows that SOTA LLMs struggle solve ProverQA problems, even with CoT prompting, demonstrating the unique challenge posed by our dataset. We also finetuned 1lama3.1- 8B-Instruct on separately generated training set and observed consistent performance improve- ments on both in in-distribution and out-of out-of-distribution test sets. We hope that our generation frame- work and the resulting dataset could contribute to the development of more robust and capable models in this area.
ETHICS STATEMENT
The keywords and names used in this paper are sourced entirely from public repositories and databases. Specifically, the names were collected from two public GitHub repositories under MIT

---

Published as a conference paper at ICLR 2025
Table 5: Typical errors made by models and how finetuning correct them. Reasoning chains before and after finetuning are both displayed for comparison.
Error Type
Context
Before Finetuning
After Finetuning
All stdents are hamanss somoone sudies, thas hobie is student. person eiher studies tenches. No young person Jery neither teaches a manager. Rose is young or student, Quesiion: Jony is not young.
person stidies tesches, young per- soe tesches. Thersfore, a young person studies. If
Jenry neither nor manager
A person either studies. or ieaches. Jemy stdies. Jerry studies, If some- studies, hohke studest. Jeny is studeni, Jeny is studen. All studenis are humons. Jerry human. Accordingg the context and cunclusions
womeome stadies, then they Therefone, a young person human. People are either young or old. Therefore, a youing person not old. Jeny netheer teaches nor manager Therefore, Jeny studies. Sinee Jerry fore, Jerry is young. Answer: falee
student. All
Common sense shortcut
a
Jerry not There-
have already been drawn, we can deduce that il is uncer- tain that lenry is not young. Answer: uncertain.
Beijing capital People's public Chins. Beijing woeld's meal populons national eapital city. Bei- jing located in Northern China. Bei- jing bosed Sammer Panalympics Games. Beijing his hosted both the Summer and Winter Olympics, along with the Summer Winter Paralympics.
Beijang hasted Summer Piralympies Games. However. there &s no infommtioon about Beijing bosting Winter Olympics. Therefore, the statemeat is uncertain explisilly has hosted Winter Clympics, explicitty stated that his uot.
Olympics
Beijiag, hasted 2008 Summer
Olympics and Paralympics Games. Beijing has bosted both the Summer and Winter Olympics, along with and Winter Pumlympics. Reijing has hasted both the 2008 Summer Olympics and winter olympics. Therefore, has basted. both the 2008 Summer Olympics and winter olympics. Ansver: trne.
Olympics
Beijing also not
Unfaithful to the context
Anewer: uncertain.
Beijing
Question: Beijing has hosted both 2008 Summer Olympics and winter olympics.
Robert Lewandowski a striker Stikers are soceer players. Kobert Lewandowski left Bayern Munchen. If a player left team they longer play for that team. Question: Robert Lewandowsk plays Bayem Munchen.
Robert Lewandowski stilker Strikess cer playess. Therefore, Robert Lewandowski soccer player. Robert Lewandowski left Bayem Munchen. If a player left team, they longer play
Robert Lewandowski left Bayern Munchen.
player left team they no longer play for that team. Robert Lewzadowski does not play Bayem Munchen. hereffore, Robert Lewandowski plays for Bayern Munchen. Answer. talse.
Unable to extend the reasoning chain
Therefore, Robert Lewandowshs longer plays for Bayer Munchen, Harwever, question is asking hie plays for Bayem Munchen, not it he left. The information does not state that he
curisntly plays another Answer: uncertain.
licenses, and the keywords were obtained from WordNet. All sources have licenses permitting free usage, and our work complies with these terms. Our dataset does not involve human participants, nor does present any immediately harmful insights. For the release, we plan open source the code for creating the benchmark and the dataset we created for the experiments in this paper.
8 REPRODUCIBILITY STATEMENT
For our submission, we have uploaded the entirety of the source code as a zipped file that has been properly anonymized. The source code contains inline documentation that details purpose and usage of different parts of the codebase. In addition, we also include the full set of model's responses and the evaluation script. As discussed in the ethics statement, plan to more formally release ProverQA to the public as an open source repository with thorough details that describes the framewrok, outlines the code, and details its usage.
ACKNOWLEDGMENTS
This work is supported by National Key Research and Development Program of China (Grant No. 2024YFB331 1902), National Natural Science Foundation of China (Grant No. 62173017), Beijing Natural Science Foundation (Grant No. L241018), Beijing Nova Program (Grant No. 2024085), and Shanghai Artificial Intelligence Laboratory.
REFERENCES
Arkadeep Acharya, Brijraj Singh, and Naoyuki Onoe. Lim based generation of iiem-ddsccrppion for recommendation system. In Proceedings of the 17th ACM Conference on Recommender Systems, pp. 1204-1207, 2023.
10

---

Published as a conference paper at ICLR 2025
Anthropic. Claude 3.5 sonnet. 2024.
URL httos://ww.atttropi......
=laude-3-S-sonnet
Peter Clark, Oyvind Tafjord, and Kyle Richardson. Transformers as soft reasoners over language. In Proceedings of the Twenty-Nini International Conference on International Joint Conferences Artificial Intelligence, pp. 3882-3890 2021.
Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smi solver. In International conference Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340. Springer, 2008.
Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob Raumer. The lean theorem prover (system description). In Automated Deduction- Ciotuction-CADE-22 CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp- 378-388. Springer, 2015.
Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The llama 3 herd of models. arXiv preprint arXiv:2407.2 1783, 2024.
Bruce Frederiksen. Applying expert system technology to code reuse with pyke. PyCon: Chicago, 2008.
Pranshav Gajjar and Vijay K Shah. Oran-bench- 13k: An open source benchmark for assessing Ilms in open radio access networks. arXiv preprint 2rXXi:2407.062455 2024.
Robert Geirhos, Jörn-Henrik Jacobsen, Claudio Michaelis, Richard Zemel, Wieland Brendel, Matthias Bethge, and Felix A Wichmann. Shortcut learning in deep neural networks. Nature Machine Intelligence, 2(1 2(11):665-6 673, 2020.
Olga Golovneva, Moya Peng Chen, Spencer Poff, Martin Corredor, Luke Zettlemoyer, Maryam and Asli Celikyilmaz. Roscoe: A suite of metrics for scoring step-by-step reason- ing. In The Eleventh International Conference Learning Representations, 2022.
Christopher Hahn, Frederik Schmitt, Jens Kreber, Markus Norman Rabe, and Bernd Finkbeiner. Teaching temporal logics to neural networks. In International Conference Learning Represen- tations, 2021.
Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Luke Benson, Lucy Sun, Ekaterina Zubova, Yujie Qiao, Matthew Burtell, et al. Folio: Natural language reasoning with first-order logic. arXiv preprint ar09 000900 2022.
Shengding Hu, Yifan Luo, Huadong Wang, Xingyi Cheng, Zhiyuan Liu, and Maosong Sun. Won't get fooled again: Answering questions with false premises. arXiv preprint 207.024307 2023.
Sophie Freya Jentzsch and Kristian Kersting, Chatgpt is fun, but it is not funny! humor is still challenging large language models. In 61st Annual Meeting of the Association for Computational Linguistics, ACL 2023, 2023.
Albert Q Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, et al. Mistral 7b. arXiv preprint arXiv:2310.06825, 2023.
Albert Jiang, Alexandre Sablayrolles, Antoine Roux, Arthur Mensch, Blanche Savary, Chris Bam- ford, Devendra Singh Chaplot, Diego de las Casas, Emma Bou Hanna, Florian Bressand, et al. Mixtral of experts. arXiv preprint arXhv:2401.04088 2024.
Hanmeng Liu, Jian Liu, Leyang Cui, Zhiyang Teng.
Nan Duan, Ming Zhou, and Yue Zhang. Logiqa 2.0 improved dataset for logical reasoning in natural language understanding. JEEE/ACM Transactions on Audio, Speech, and Language Processing, 31:2947-2966 2023. doi: 10.1109/ TASL TASL.P.203..32930
11

---

Published as a conference paper at ICLR 2025
Jian Liu, Leyang Cui, Hanmeng Liu, Dandan Huang, Yile Wang, and Yue Zhang. Logiqa: chal- lenge dataset for machine reading comprehension with logical reasoning. In Proceedings of the Twenty-Ninth International Conference International Joint Conferences Artificial Intelli- gence, pp. 6622-3628, 2021.
Qing Lyu, Shreya Havaldar, Adam Stein, Li Zhang, Delip Rao, Eric Wong, Marianna Apidianaki. and Chris Callison- Ballisoo-Buuchh. Faithful chain-of of-thought reasoning. In The 13th International Joint Conference on Natural Language Processing and the 3rd Conference of the Asia- asia-Pacific Chapter of the Association for Computational Linguistics (IJCNLP-AACL 2023). 2023.
William McCune, Release of prover9, In Mile high conference on quasigroups, loops and nonasso- ciative systems, Denver, Colorado, 2005.
Aaron Meurer, Christopher P. Smith, Mateusz Paprocki, Ondřej Čertík, Sergey B. Kirpichev, Matthew Rocklin, Amit Kumar, Sergiu Ivanov, Jason K. Moore, Sartaj Singh, Thilina Rath- nayake, Sean Vig, Brian E. Granger, Richard P. Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, Fredrik Johansson, Fabian Pedregosa, Matthew J. Curry, Andy R. Terrel, Stěpán Roučka, Ashutosh Saboo, Isuru Fernando, Sumith Kulal, Robert Cimrman, and Anthony Scopatz. Sympy: symbolic computing in python. PeerJ Computer Science, 103, January 2017. ISSN 2376-5992. doi: 10.7717/peerj-os. 103. URL http::://///::ttrr///// org/ /0. 701. 7717/peerr cs. 103
George A Miller. Wordnet: lexical database for english. Communications of the ACM, 38(11): 39-41, 1995.
Theo X Olausson, Alex Gu, Ben Lipkin, Cedegao E Zhang, Armando Solar-Lezama, Joshua B Tenenbaum, and Roger P Levy. Line: A neurosymbolic approach for logical reasoning by com- bining language models with first-order logic provers. In The 2023 Conference on Empirical Methods in Natural Language Processing, 2023.
OpenAI. Hello GPT-4o. 2024.
Liangging Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. Logic-Im: Empower- ing large language models with symbolic solvers for faithful logical reasoning. arXiv preprint arXiv: 12295, 2023.
Chengwen Qi, Bowen Li, Binyuan Hui, Bailin Wang, Jinyang Li, Jinwang Wu, and Yuanjun Laili. An investigation of lims' inefficacy in understanding converse relations. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Prucessing, pp. 6932-6953, 2023.
Danilo Neves Ribeiro, Shen Wang, Xiaofei Ma. Henghui Zhu, Rui Dong, Deguang Kong, Juli- ette Burger, Anjelica Ramos, William Yang Wang. George Karypis, et al. Street: A multi-task structured reasoning and explanation benchmark. In The Eleventh International Conference on Learning Representations, 2022.
Abulhair Saparov and He He. Language models are greedy reasoners: A systematic formal analysis of chain-of-thoughi In The Eleventh International Conference on Learning Representations, 2022.
Abulhair Saparov, Richard Yuanzhe Pang, Vishakh Padmakumar, Nitish Joshi, Mehran Kazemi, Najoung Kim, and He He. Testing the general deductive reasoning capacity of large language models using ood examples. Advances in Neural Information Processing Systems, 36, 2024.
Koustuy Sinha, Shagun Sodhani. Jin Dong. Joelle Pineau, and William L Hamilton. Clutrr: A diag- nostic benchmark for inductive reasoning from text. Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP), pp. 4506 4515, 2019.
Shivehander Sudalairaj, Abhishek Bhandwaldar, Aldo Pareja, Kai Xu, David Cox, and Akash Srivastava. Lab; Large-scale alignment for chatbots, 2024. URL https: httpps:///axxv...t
abs/ / 22/22440.00000 01081
Haitian Sun, William W Cohen, and Ruslan Salakhutdinov. Conditionalqa: A complex reading comprehension dataset with conditional answers. arXiv preprint arXiv:21 10.00.2/10.06888 2021.
12

---

Published as a conference paper at ICLR 2025
Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. Proofwriter: Generating implications, proofs, and abductive statements over natural language. Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pp. 3621-3634. 2021.
Rohan Taori, Ishaan Guirajani, Tianyi Zhang, Yann Dubois, Xuechen Li, Carlos Guestrin, Percy Liang, and Tatsunori B. Hashimoto. Stanford alpaca: An instruction-following llama model.
dattps:/ee https://github. github. wom/tatsu--ae htwillaabstaafeee stanfordnoforrooo/ooo alpaca) 2023.
Jidong Tian, Yitian Li, Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. Diagnosing the first-order logical reasoning ability through logicnli. In Proceedings of the 2021 Conference on Empirical Methods Natural Language Processing, pp. 3738-3747, 2021.
Karthik Valmeekam, Alberto Olmo, Sarath Sreedharan, and Subbarao Kambhampati. Large lan- guage models still can't t plan (a benchmark for Ilms planning and reasoning about change). In NewrlPS 2022 Foundation Models for Decision Making Workshop, 2022.
Zihao Wang, Shaofei Cai, Guanzhou Chen, Anji Liu, Xiaojian Shawn Ma, and Yitao Liang. De- scribe, explain, plan and select: interactive planning with Ilms enables open-world multi-task agents. Advances in Neural Information Processing Systems, 36, 2024.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi. Quoc V Le, Denny Zhou, et al. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824-24882 2022.
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. Satlm: Satisfiability-iide language models using declarative prompting. Advances in Neural Information Processing Systems, 36, 2024.
Weihao Yu, Zihang Jiang, Yanfei Dong, and Jiashi Feng. Reclor: A reading comprehension dataset requiring logical reasoning. In International Conference Learning Representations, 2019.
Yu Zhang, Hui-Ling Zhen, Zehua Pei, Yingzhao Lian, Lihao Yin, Mingxuan Yuan, and Bei Yu. Sola: Solver-layer adaption of Im for better logic reasoning. arXiv preprint arXiv:2402.1 19033, 2024.
Wanjun Zhong, Siyuan Wang, Duyu Tang, Zenan Xu, Daya Guo, Jiahai Wang, Jian Yin, Ming Zhou, and Nan Duan. Ar-lsat: Investigating analytical reasoning of text. arXiv preprint arXiv:2104.06598, 2021.
A PROMPT FOR GENERATING BACKGROUND STORY
System:
be glven keyword and name (can person's a name or an animals' name). Your task is to generale beckground story with more than 150 words according to the keyword about this name. Your answer should be in JSOK format with keys: estagory, story.
User:
keyword: swift
name: Jack
Assistant:
"calegory"; "cal",
"story": *Jack was sleek, agile cat known for his swift novements. Born in the bustling city, he quickly learned navigate the narrow alleyways and rooftops
ease.
Hia speed and lyy made him legerd among the local fel community. Jack's favorite pastime was chasing the elusive city birds, darzing through the air with unnatched precisien. Despite his wild spirit, he had soft spot for the elderly woman who Zed him daily. She naned him Jack after the nimble character from her fevorite childhood story, believing that Jzck's a swift nature wasn't just physicel; he had quick wit and an uncanny ability to sanse danger, keeping becane symbol of agility and cleverness in the neighborhoodd."
was sign good fortune.
in the urban jungle. Bis lagend grex, and
User:
keyword: success
name: Any
13

---

Published as a conference paper at ICLR 2025
Assistant:
"category"; "human",
"story":
"Amy in small town where opportunities wes determined to make something of herself. After excelling in high school, she carnad achclarship acience and quickly became known for her innovative Ideaa. Opon graduation, Amy co- founded tech startup
Despite the odds, she
prestigioua university. There, she majored in computor
focused sustainable sechnology. Her company quickly gadd traction, securing major inveatments and partnerships. Any'a relent work ethic and visionary leadership Lirned her starcup into mulli- milli-nillion dollar enterprise within five years. Today, the celebrazed not only for her business acumen but also for her commitment to mentoring young enssepreneurs and giving back har community. Amy's atory tastament to the powar perseverance, vision, and hard work."
User:
keyword: loyal
nome: Bolla
Assistant:
"calegory"; *dog",
"story": "Bells was a golden retriever with heart as puze as geld. From the noment she was adopted by the Thempson family, she became their steadfast guardian and companion. Balla had an uncanny ability to sense when somsone in the family needed comfort, with auzzle young Timny got lest in the woods behind their house, Bells tracked his scent :irelessly, refusing rest until she found him. the cold night, keeping hin and safe until help arrived. Bella's unwavering loyalty and love made her not just a pet, but cherished nember of the family."
alwaya
wagging tail,
loyalty
evident
stayed by his side through
User:
keyword: [XEYWORD] (NAKD)
B PROMPTS FOR TRANSLATING LOGIC EXPRESSIONS INTO NATURAL LANGUAGE
We utilized three examples for each type of logical expression to guide the L.MMs translating them into natural language. An example of the prompt we used in our experiments is shown below.
System:
will provided logic expression, expression, and background stocy. Your task is to zeplace the placeholde:s in the logic expression with appropriate predicates more than words) that the provided logic expression represent real world common sense rule.
exiated precicate the logio
Do use 'not', De not the words the Forbiddes 1ist. The words that eimilar in meaning to the words in the forbidden 11st are also not al lowed.
Your answer is not zequired te clusely connected to the background scory. You can use any predicates you as leng their length
Your answer ahould be 3SON fornat with the provided keys.
User:
background story:
Moriarty was large, fluffy Maine Coon cat with surprisingly warm and gentle nature. Daspita his intimidating size and nysterious name inspired by fanous literary villain, Moriarty was the epitome of warmth and confort. Be 1ived in a onzy bookstorB run by Mrs. Lindon, an elderly wonan who had taken him in as stray, Moriarty had a apecial talent for sensing when custemer needed bit of extra warmth, often curling zead. His thick fur and gentle parring provided solace to many, especially during the cold
in their laps they winter months. Moriarty's presence tuzned bookstore into beleved pecple came not just for the books, but for the warm, conforting presence of their favorite friend.
haven,
reference: le le_flužfy
is_fluffy (Moriarty) fluffy, then he is either warm and gentle or calning, but not hoth. forbidden list: ['deeneand_eentle "provide_comfozt', 'attract_customet" fis friendde'' "brings_joy", "ia_flutšy', 'is_calming')
(wamm_and_eente (Koriarty) & is_calming (Korierty) 15 Soriarty is
14

---

Published as a conference paper at ICLR 2025
logic expression: (#7)x) (is fluffy () keys: (*F7', "FB', "univeraal_rule"" "opeol
Note: belonga to cat.
Assistant:
"playful", "P8"; flove_attention",
"universai_rule" "A1l playful cata are ruurty and love attencion.",
" *If Moriarty is playful, then be is beth flufły and loves actention."
Examples
User:
background story:
Colt bri lant botanist the Avicemilaees family, specifically the nangzove plants, which thrive in the hazzhest of coastal environments. development of innovative solutions for coastal conservalion. Be discovered that the Avicencia species possessed remarkable adaptability, allewing then to survive in areas with high salinity and limited exygen. Colt's findings opened doors enosystema and protecting andangered species. As a leading expart in hig field, Golt collaporated international organisations the delicate balance of cur planet's mangrove ecoeystems. lii dedication to the Avicenniareae family lasting impact on scientific community.
passion
plant species. He spent years studying
groundbreaking research
unique plants
methods for restoring danaged
implement
helping preserve
reference: totpurte_tteevvvomeetteeeee conservaiion
rerrrrsacttrrrrccccccccao (Colti mako_grounabreaking www.ovirriaaaaeeee. (Colt)
contribute_to__eoo cestt__tt__vvvveee rommnttremmenta ronmental conmental__onaerves ioonservatton (Co t)): If Colt la dedicated to research, ther he
groundbreaking discoveries
contribute environmental conservalion.
forbidden list: [' ('dedicated_te ressersrchhtt waak__gruunbreekiin
www..nbbeeeiingg.iceeeeseseeeeee discoveries',
'contribute wtw.bbbtteoooovvviiooeeeeee htt.rr/ooo.o.mmmaooooooorrrotoo.
surasa__igher_ediiaa
aacome_leading_cem
kays: ('P5', 'F6', funiveraal cetrrributet__eevvveeee sc_envirommenta aww.ronnaaa....oeeeeiiioo.a. A (6(x))
logic expression: Vx (#5 + (contribute_te
'specific_rule"
Note: x belongs to human.
C POTENTIAL SHORTCUT PROBLEM
To further investigate the potential use shortcuts, we conducted an experiment by removing uni- versal rules from 60 randomly selected instances in ProverQA. We evaluated GPT-4 and 1lama-3.1- 70B- Ins-rnst on this corrupted dataset. If the models were relying heavily on inherent knowledge shortcuts, their performance would remain roughly unaffected despite the absence of universal rules, However, the results Table showed significant drop in performance, indicating that these models do not heavily rely on background knowledge solve the problems.
Table 6: Comparative performance of GPT-4o and and the corresponding corrupted version.
on the original dataset
Model
Prompting Strategy
Original
Corrupted
Ace A
GPT-40
Direct
58.33
43.33
-15.00
GPT-4o
CoT
68.33
45.00
-23.33
Llama-3.1-70B-Insttee
Direct
65,00
48.33
-16.67
Llama-3.1-70B-Instteee
CoT
65.00
53.33
-11.67
D EXAMPLES FROM THE THREE SUBSETS OF PROVERQA
ProverQA-Easy
For every elephant, the elephans is either domesticated wild, but not both.
domeat elephant.
15

---

Published as a conference paper at ICLR 2025
Question: Based the above information, is the following statement true, false, uncertain? Anakin is not a wild elephant.
Options:
True
B1 Palse
The correct option 1s:
Proofs
Step1
fact1: Anakin is domesticated elephant.
sule: For every elephant, the elephant either domesticated or wild, bus not both. conclusion: Anakin is not wild elephant.
Therefore,
Anakin wild elephant. The opt
ProverQAA-Medium
Context:
Everyone who either practices waltz oz masters Lazgo (but not both) has good dance skills. Sawyer has cherisma. sawyer performer. Saxyer good dance skills then he is suscessful dancer. Sowyer is either musician or peat, but not both. Alice is a poet. Sawyer is poet. It Sawyer pertormer, then he is either skillec at cancing or musician, but not beth.
charisma,
Question: Based the ahove information, the following statement false, uncertain?
Sawyez is successful dancer.
Options:
True
False
Uncertain
The correct option is: A
Proofs
Stepl-
fact1: Sawyer is post.
sule: Sazyer is sither musician or poet, but not both.
concluaion: Sawyar not musician.
Step2-
fact1: Sawyar is a performer.
fact2: Sawyer
musician.
rule: If Sauyer is performer, then ha is either skilled at dancing or musicion, but both,
conclusion: Bawyer has good dance skills.
Step3
Sawyer good skills. fact2: Sawyar has charisma. zules If Sawyer has good dance skilla and has chariama, then he successful dancer. conclusion: Bawyer successful dancer.
factl:
Therefore, is that Sawyer successfu". dancer. The correcs option A.
ProverQA-Hard
Context:
Suste: does not respond to calls. All doga that Listen to commands and behave properly are well trained.
either obedient or playful, ast necessarily Buster follows coutines. suster is either playful or leving for both!. If suster eicher responds to calls or follows routines (but. not both), than Histens to commands. obedient and have good manners. Sustez behaves properly.
wall-trained dags are
Question:
Sased the above information, the folloving statement false, uncertain?
Buster is laving.
Options: True
16

---

Published as a conference paper at ICLR 2025
Uncertain
The correct option is:
Proofs
Step1
Buater doea not respond to calls, fact2: Buster follows routines. zule: if Buster sither responds to calls or follows routines (but not both), then Listens commands.
factl:
conclusion: Buster liatens to commands.
Step2
facti: Buster listens commands
fact2: Bestar behaves preperly.
rules
Hattn commands and behave properly well--rained.
conclusion: Buster is well tzained.
Step3
facti: Buster sell-trained.
rules All wall wall-trained dogs are obedient and have good manners. conclusion:
obedlent.
factl: Buster is obedient. rules Buster aither obadient playful, but necessorily both. conclusion: Bustar is not playful.
StepS
factl: Buster is pleyful.
zule: Buster is either playful or loving (or both). conclusion: Bustar loving.
Therefore,
Buster loving. correct option is:
E EXAMPLES OF THE TWO PROMPTING METHODS
The prompts of the two prompting strategics we used in our experiments are listed below. We adopt 2-shot in-context learning for both staddard and CoT prompting strategies.
Standard Prompting
System:
ven probl em atatement as contexta, the task 1s to answer logical reasoning question. Your answer should be in JSON Tornat with key:
Anyone who can solve problems and communicate effectively has practicel skills. If Pacls appreciates beauty, then values precision enjoys manual work. Pacla is either skilled in mathematics. has practical skills, but not both. If someare enjoys manual work and values attention detail, then they can eraft with their hands. Paola is eithes skilled in mathematics artistically inclined, but surprisingly, she is actually both. Paola values attention to detail, Anyone who crafts with their hands has practical ak:
appseciates beasty.
Question: Bazed the above information, is the following statement true, false, or uncertaia? artistically inclined.
Options: True
Bi False
correct option is: "answer*: "A*
Another Example
Context: [[CONTEXT]]
17

---

Published as a conference paper at ICLR 2025
Question: ([QUESTTON)
Options: [[0PTION:]]]
The correct option 1s:
CoT Prompting
System:
Given a problem statement as contexta, the Lask Le to answer logical reasoning question. Your answez should be JSON format with keys: ressoning,
Context:
Anyone who can solve problems and communicate effectively has practicsl skills. -f Pacls appreciates beauty, then values precision enjoys manual work. Paola appreciates beasty. Paola la either skilled in mathematics manual wozk and values atteation to detail, then they can craft with their hands. Paola is either skilled in mathematics
has practical akills, but not both. If someane enjoys
artistically inclined, but surprisingly, she is actually both. Pacla values attantion to detail. Anyone who crafts with their hands has practical sk:lls.
sased the above information, is the following statement true, false, or uncertain? Pacla is artistical inclined.
Question:
Options:
True
False
The correct option 1s:
"reasoning"; "Paola appreciates beauty. Paola appreciates beauty, then she values precision and enjoys manual work, Paola enjoys manusl werk. Fsola enjoys manual work. #scla values actention detail. somsone anjoys manual work and valuea sttention to detai then they can graft with their r hands. Pao crafts erafts with their
with hands, 2acla erafts with hes hands. Anyone has practical skills. Paola has practical aki 111.,. Paola has pract feal skills. Paola either skilled in nathematica or has practical sxills, but not both. Paola not skilled in mathematics. Paols is either skilled in mathematics or artistically inclined, but surprisingly, la actually bath. Paola is artistically inalined. Tharefore, it ia true that Paola is artiatically inclined, The correct option 18: A.",
skilled in mathematics. Paols
"answer";
Another Example
Context:
[[CONTEXT]]
Question: [[QUESTION]
Options: [[OPTrONS)
The correct option is:
F TRAINING DETAILS
To create the ProverQA train set, we started by generating 5,000 instances for each difficulty level: easy, medium, and hard. We then applied data augmentation techniques expand the dataset. Specifically, for each problem, we broke down every step of its reasoning chain to form new ques- tions. Additionally, we replaced the final conclusions with random facts create problems whose answer is uncertain. This process expanded our generated data pool 50,000 instances.
Our experiments show that, as the number of training instances increased, the model's performance consistently improved in-distribution datasets and two out-of-distributiion datasets: Proo/Writer and ProntoQA. However, performance on FOLIO fluctuated as the number of training instances increases. After further experimentation, we found that 5,000 is sweet spot that reaches good balance between in-distribution and out-of-din autto--distriuution performance. Therefore, we sample 5,000 instances from the generated data pool as the final training set for finetuning experiments.
18

---

Published as a conference paper at ICLR 2025
Since FOLIO lacks reasoning chains, could not apply the same augmentation techniques it. We used the full set of FOLIO, consisting of 1,001 instances. For ProofWriter, which includes mul- tiple questions per context similar to data augmentation, we did not apply further augmentation.
We also finetuned the model on the full set ProofWriter, which has 45,290 instances. The perfor- mance is comparable compared to the performance of model trained of 5,000 instances, indicating that the model may already be saturated at this size for an 8B param- eter model. As a result, we report the results of the sampled subset.
sampled subset consisting
For all finetuning experiments, we experimented with different training hyper-parameters, such as training epochs, learning rate and training set size, and selected the best configurations on held-out validation sets.
G EXPERIMENTING WITH 5-SHOT EXAMPLES
To further explore the impact of few-shot examples, we conducted additional experiments using 5-shot prompts. The results are presented in Table 7 It can be concluded that incorporating more examples (5-shot vs. 2-shot) into the prompt did not consistently improve the performance of LLMs. This inconsistency may stem from several factors, including variations in the models' in-context learning capabilities.
H QUALITY CONTROL
The ProverGen framework employs three heuristic methods to ensure the quality of the generated data, addressing different aspects of data integrity and consistency.
Logic Validation: Our framework includes robust logic validation step. For each in- stance, we input both core premises and distractions into the symbolic prover to ensure they correctly deduce the conclusion's 's truth value.
Conflicts Resolution: During rule translation, we check for previously used predicates to avoid redundancy and potential conficting facts. Additionally, we utilize LLMs to assess whether the generated universal rules align with real-world knowledge. In cases of conflict, we opt for specific rules instead.
Translation Quality Control: We apply heuristic method to ensure that all involved entities appear in both symbolic expression and natural language expression. For example, when translating "poet(Sawyer)" into "Sawyer is poet", we verify that both the name "Sawyer" and the predicate "poet" are present the translation.
Additionally, the training part of the paper also serves as quality-checking process. Finctuning on the generated dataset enhances the performance of LLMs both in-distribution and Out-of- Distribution datasets, indicating the relatively high quality the generated data.
To further investigate the quality of the generated data, performed manual evaluation of 60 randomly sampled examples (20 from each subset) from our dataset. The evaluation revealed no translation errors indirect contradictions, suggesting that the likelihood of potential errors is less than 2%.
19

---

Published as a conference paper at ICLR 2025
Table 7: The performance of LLMs in the 5-shot setting. The values in parentheses indicate the change in performance relative the 2-shot setting.
ProverQA
ProntoQA
ProofWriter
FOLIO Avg
Easy
Medium
Hard
Standard Prompting
85.20
68.40
43.80
88.20
57.33
72.86
GPT-4o
-0.37
(-2.00)
(-0.20)
(-2.40)
(-3.60)
(+1.00)
(+5.00)
93.80
76.80
51.00
85.20
50.33
74.29
Claude-3.5-Sonne
+2.23
(+8.20)
(+8.60)
(+8.20)
(-3.40)
(-4.67)
(-3,56)
64.40
41.80
38.00
58.00
44.50
46.43
10-ma3.1-8B-Imae
+2.67
(+17.80)
(-1.20)
(-1.00)
(+7.60)
(40.70)
(-7.86)
82.80
64.40
49.20
74.00
51.33
69.29
1lamaa.1-770BIIstii
-0.26
(+0.80)
(+0.20)
(+1.60)
(-6.60)
(+1.00)
(+1,43)
57.40
48.40
37.40
52.40
47.83
52.86
Mistral-7B Iinstrcc-BIInstructt
+1.48
(+0.60)
(+1.60)
(40.20)
(+2.40)
(45.50)
(-1.43)
85.00
71,40
53.60
67.40
63.50
76.43
Mistral--Large-Istrie
+0.91
(+0.40)
(+2.20)
(+4.00)
(-3.60)
(+3.17)
(-0.71)
77.60
58.00
39.60
60.00
40.50
73.57
Mixtral-8x22B-Insie
-0.37
(+2.20)
(+0.60)
(+0.60)
(-5.20)
(40.33)
(-0.72)
CoT Prompting
95.00
81.20
55.00
99.20
71.00
74.29
GPT-4o
+2.10
(+0.80)
(+1.80)
(+5.00)
(-0.80)
(43.67)
(+2.15)
92.00
81.60
61.00
95.80
75.50
82.86
Claude-3.5-Sonnet
-0.45
(-3.20)
(-2.00)
(+4.60)
(-3.40)
(-0.83)
(+2.15)
80.60
45.40
31.20
74.80
58.67
57.86
-1.21
(+5.00)
(-1.20)
(-2.40)
(-4.80)
(+1.84)
(-5.68)
92.60
73.40
50.20
92.80
67,00
75.00
Llama3.1 1-70B Instruct
-0.04
(+2.20)
(+0.20)
(+3.40)
(-2.60)
(4.17)
(+0.71)
65.60
50.20
38.00
65.80
48.33
63.57
Mistral-7B-Instee
-0.68
(-6.40)
(-0.80)
(-3.80)
(+4.60)
(42,33)
(-0.01)
94.40
77.60
56.60
99.00
77.67
82.86
Mistral-Large-Insste Instruct
+1.98
(+1.80)
(+1.80)
(+4.40)
(+0.40)
(+4.17)
(-0.71)
91.00
73.80
50.20
86.20
59.67
72.14
Settra-8x22B-IMMe
+3.36
(+3.40)
(+7.00)
(+2.60)
(+6.60)
(+2.00)
(-1.43)
20


Reviews:
[{"review_id": "KGhPC1KggT", "reviewer": "Reviewer_NAgL", "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.\n\nInterestingly, the authors also show that fine-tuning models on ProverGen improves their OOD reasoning capabilities on datasets such as FOLIO and PrOntoQA.", "questions": "I provide more detailed questions and comments below. The paper is well-written with only a small number of grammatical errors.\n\nTable 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).\n\nLine 86: \"ProverGen’s difficulty setting demonstrates a fine-grained complexity\"\n  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.\n\nIt 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.\n\nFootnote 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.\n\nSection 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?\n\nLine 303: \"we opt to the specific rule\" -> \"we opt for the specific rule\"\n\nHave the authors experimented with more than 2 few-shot examples in the prompt? If so, were there any significant differences in behavior?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "- The authors present a pipeline approach for generating QA data to test the reasoning abilities of LLMs.\n- 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.\n- 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).\n- 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).\n- 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "uIe2CeYI9P", "reviewer": "Reviewer_BNmr", "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.", "questions": "1. Please discuss the points mentioned in the weakness section.\n\n2. In the case study section, are there any statistics showing how many cases improved with the help of training?\n\n3. Would changing the generation model from Llama3.1-70B-Instruct to a more advanced model make any difference?\n\n4. Is this generation pipeline only helpful for building benchmarks, or can the synthetic dataset be used for future training?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The paper is well-written with clear presentation. The authors effectively explain how ProverGen differs from existing FOL reasoning benchmarks.\n\n2. 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.\n\n3. 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.\n\n4. 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.\n\n2. 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.\n\n3. Lacks detailed analysis of domain distribution in the generated dataset. The diversity of the generated data is not fully revealed.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "QR03zD1bu5", "reviewer": "Reviewer_64s6", "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.", "questions": "(1)\tHow 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?\n\n(2)\tDoes the LLM introduce any errors when translating FOL statements into natural language, as well as during the Logic Skeleton Generation?\n\n(3)\tIs there any invalid case generated and is there a quality control process in place to filter out invalid cases?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "I also work on logical reasoning, and I personally really like this paper. It addresses some key limitations of the previous benchmarks.\n\n(1)\tFor 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.\n\n(2)\tExperiments demonstrate that this benchmark poses a significant challenge to state-of-the-art LLMs.\n\n(3)\tFine-tuning using this new dataset results in greater improvements compared to previous logical reasoning datasets, highlighting the advantages of the dataset.\n\n(4)\tIt 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:\n\n(1)\tSome 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.\n\n(2)\tYou 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?\n\n(3)\tIt might be helpful to emphasize the importance of reducing disconnected and contradictory cases in your contribution, as they hinder the reliability of the evaluation.\n\n(4)\tGiven 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.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "JxUqY70xvM", "reviewer": "Reviewer_oQpi", "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.", "questions": "see above", "limitations": "", "rating": 3, "confidence": 4, "soundness": 1, "presentation": 3, "contribution": 1, "strengths": "see below", "weaknesses": "## Novelty\n\nAs 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.\n\n\n## Quality\n\nThere are several issues with the creation of the dataset.\n\nSome FOL reasoning cases are potentially not covered by this benchmark:\n- 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)*\n\nLack of dataset quality check:\n- There lacks a check on whether the translated NL statement actually align with the ground-truth FOL rule\n- 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.\n- 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.\n\nFinetuning results interpretation:\n- 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.\n\n## Clarity\n\nThis paper is generally easy to follow.\n\n## Significance\n\nAnother major concern of mine is the significance of this benchmark.\n- 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.\n- 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?\n\nThat said, the authors need to address this issue before this work can be considered significant.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)