Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning

Due to the space limit, we continue our answering in the following.

Q1. Line 115: "To save computational cost, we compare each one of logically equivalent formulas". You probably mean to "compare each logically equivalent formula". How can this save computational cost?

A. To clarify the meaning of the sentence in line 115, here is an explanation using an example in Figure 2. After compositional first-order logic translation, there are six candidate formulas. For disproving by counter-interpretation, we should compare all the possible 15 pairs of six formulas. To save computational cost, we first group logically equivalent formulas which in fact there are only two logically different formulas, and then we could compare a single pair of the two formulas.

Q2. Line 149: How to read this formula in natural language?

A. For intuitive explanation, Eq. 1 means that in prior neurosymbolic approaches [1, 2, 3], an LLM translates a logical reasoning problem $x$ into a theory $\hat{T}$ and pairs of first-order logic formula and its natural language description. Note that a theory $\hat{T}$ includes 1) declarations of sorts, functions, and predicates and 2) the most commonly applied theories (e.g., theory of equality, arithmetic, etc.). For simplicity, we presume that a theory $\hat{T}$ always incorporates the most commonly applied theories.

Q3. What is the output for the sentence "A barber shaves all who do not shave themselves."?

A. Following our problem formulation, we first run a preprocessing step as in Eq. 2. An LLM returns a theory $\hat{T}$ that involves the following declarations: A sort named $*people*$, a predicate named $*shaves*$ of the type $*people* \times *people*$, and a constant named $*barber*$ of sort $*people*$ (a constant is a function with zero arity). An LLM also returns a target sentence same as the original sentence.

Now, we perform compositional first-order logic translation to translate the target sentence under the estimated theory.

1. Logical Dependency Parsing
   Structure #1:
   U1="A barber shaves all", D1="who do not shave themselves"
   D1 -> U1
   Structure #2:
   U1="A barber shaves all", U2="People do not shave themselves", C1="(merge)"
   U1 -> C1, U2 -> C1

2. Component Accumulation
   For Structure #1:
   1) A barber shaves all.
   2) A barber shaves all who do not shave themselves.
   For Structure #2:
   1) A barber shaves all.
   2) People do not shave themselves.
   3) A barber shaves all who do not shave themselves.

3. Sequential Translation
   For Structure #1:
   1) $(\forall p : *people*)\, (*shaves*(*barber*, p))$
   2) $(\forall p : *people*)\, (\lnot *shaves*(p, p) \rightarrow *shaves*(*barber*, p))$ (Formula #1)
   For Structure #2:
   1) $(\forall p : *people*)\, (*shaves*(*barber*, p))$
   2) $(\forall p : *people*)\, (\lnot *shaves*(p, p))$
   3) $(\forall p : *people*)\, (\lnot *shaves*(p, p) \rightarrow *shaves*(*barber*, p))$ (Formula #2)

Lastly, we perform first-order logic verification to select the most probable formula. As described in line 310-311, we first filter out $\hat{T}$-unsatisfiable formulas using a SAT solver. Since Formula #1 and #2 are both $\hat{T}$-satisfiable, those are not filtered out. Those two formulas are syntactically the same, so we do not have to further proceed the verification. The output formula is $(\forall p : *people*)\, (\lnot *shaves*(p, p) \rightarrow *shaves*(*barber*, p))$.

Q4. How are "Declarations" created?

A. The first equation in Eq. 2 (line 170) shows how declarations are generated. According to the equation, an LLM takes a logical reasoning problem $x$ as a input and generates a theory $\hat{T}$ and a set of target natural language sentences. A theory $\hat{T}$ corresponds to the "Declarations".

Q5. How to decide a sentence not fit for your system? (or how to decide an unintended input sentence?)

A. The first equation in Eq. 2 (line 170) also decides which sentence to translate. As the reviewer points out, a logical reasoning problem often contains sentences for declarations or even no information to solve the problem. To resolve this issue, we add a preprocessing step before applying CLOVER. Other neurosymbolic approaches [1, 2] decide which sentence to translate as in Eq. 1.

---

[1] Satlm: Satisfiability-aided language models using declarative prompting. Ye et al., 2024.
[2] Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. Pan et al., 2023.
[3] Linc: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. Olausson et al., 2023.
[4] Faithful logical reasoning via symbolic chain-of-thought. Xu et al., 2024.

We thank the reviewer for the constructive and detailed comments. Q denotes a Question, and W denotes a Weakness not addressed in the Questions.

Misunderstanding in Summary

We observe that there is a slight misunderstanding on the reviewer's summary in the following:

The first step is to translate a long and complex sentence into a number of short sentences, the second step is to translate each short sentence into simple first-order logical forms and the connections between/among these short sentences into corresponding logical connectors.

To clarify our method, the proposed compositional first-order logic translation consists of three steps. The first step is to parse a target sentence into logical dependency structures, the second step is to progressively accumulate each component of the structure while preserving its logical dependency, and the last step is to sequentially translate starting from the atomic subsentence until the target sentence.
Not only that, the proposed first-order logic verification algorithms are another novelty of this paper. To fully leverage the semantics of first-order logic, 1) we select the most frequent logically equivalent formulas (Logical Consistency), or 2) we disprove one of two formulas by judging if a counter-interpretation satisfies the target sentence. These are visually summarized in Figure 2.

W1. Authors did not discuss what sentences cannot be translated to first-order logic forms. This work is valued within fixed benchmark datasets where the meaning of natural language is a logical formula.

A. We would like to emphasize that logical reasoning, where the problems are formally represented as a first-order logic, is one major category of reasoning. [2] states that logical reasoning plays a central role in intelligent systems for problem-solving, decision-making, and critical thinking. This paper and other prior works [1, 2, 3, 4] focus on enhancing the logical reasoning ability of LLMs. The other reasoning problems such as reading comprehension are out of the scope of this line of works.

W2. Authors use a SAT solver in evaluating and selecting correct first-order logical forms. This limits the method only for the case where SAT solvers work.

A. As we state in the answer of W1, every logical reasoning problem could be translated into first-order logic, which forms a SAT problem consists of a theory, constraints, and a query. Then, a sound SAT solver could investigate if two formulas are logically equivalent, or find counter-interpretations of the two formulas which are then used for disproving.

W3. The formalism of the paper is not easy to read.

A. We describe our problem formulation and method with mathematical notations to precisely explain those. To make those easy to read, we add corresponding mathematical notations to Figure 2.

# Declarations
people = [barber, person_1, person_2, person_3]
shaves = Function([people, people] -> [bool])

# Formula
f = ForAll([p:people], Not(shaves(p, p)) == shaves(barber, p))

# Checking satisfiability
solver = Solver()
solver.add(f)
print(solver.check() == sat)

We thank the reviewer for the constructive and detailed comments. Q denotes a Question, and W denotes a Weakness not addressed in the Questions.

W1. In Table 3, what is "Is Clover?" and why is the simplest ablation outperforming Logic-LM on AR-LSAT?

A. To answer the first question, "Is Clover?" means if a method is the proposed CLOVER or if it is one of the ablations. In Table 3, the last two rows correspond to CLOVER, which use both compositional translation and verification. In contrast, the first three rows correspond to the ablations, which do not use either compositional translation (i.e., use direct translation) or verification or both. To clarify this, we add related captions in Table 3.

To answer the second question, the result that the simplest ablation outperforming Logic-LM only applies for the AR-LSAT dataset, and it comes from the specialized data characteristics. Unlike other datasets, we additionally need to predict solver functions according to the question of the logical reasoning problem. For instance, if the question is "Which of the queries CAN be true?", then we need to assign a function that checks a satisfiability of the query given the constraints. If the question is "Which of the queries MUST be true?", then we need to assign a function that checks a validity of the query given the constraints.
Logic-LM predicts a solver function together with the first-order logic translation by a single inference in Eq. 1. For CLOVER, to incorporate solver function prediction in our problem formulation in Eq. 2, we perform this prediction at the preprocessing step. Comparing those two solver predictions, the latter one has significantly less load to an LLM since the task gets much simpler. Therefore, using the latter one improves accuracy to predict solver functions, where 10.9% gain comes from this. To support this analysis, we compare performance of the simplest ablation and Logic-LM on the three other datasets in the following table.

The results indicate that the simplest ablation and Logic-LM have almost the same performance on the other datasets. This is because the other datasets use a single solver function, where there is no need for solver function predictions. We add the details of the solver function prediction on AR-LSAT in Appendix E. Overall, the performance gain on AR-LSAT is a side effect of the problem formulation.

W2. I believe the paper would benefit greatly from expanding on the models being evaluated.

A. We include the answer to Q3 of the reviewer 5CZv in the following.

In this paper, we evaluate CLOVER on two language models, gpt-4o and gpt-4o-mini (The results using gpt-4o-mini are presented in Table 5, Appendix G). For further evaluation, we include additional two language models including gpt-3.5-turbo and gpt-3.5-turbo-instruct, which are another chat-focused model and an instruction-following model, respectively. As in Table 5, we compare performance of CLOVER and neurosymbolic approach baselines on the Puzzle and Symbol datasets. If the symbolic solver cannot execute the solution, then we take random guesses. We exclude the performance of SymbCoT using gpt-3.5-turbo-instruct since the prompt including few-shot examples exceeds the context window of the language model. The following results show that CLOVER clearly outperforms the baselines across different language models. We add this results in Appendix G. Due to the limitation of computational resources, we mainly use OpenAI models, but we will expand our evaluation on other proprietary models and open-sourced models.

Performance on Puzzle dataset using different language models.

Puzzle	Logic-LM	SymbCoT	CLOVER
gpt-4o-mini	42.5	60.0	60.5
gpt-3.5-turbo	42.5	35.0	63.5
gpt-3.5-turbo-instruct	46.0	N/A	59.0

Performance on Symbol dataset using different language models.

Symbol	Logic-LM	SymbCoT	CLOVER
gpt-4o-mini	38.4	46.5	71.7
gpt-3.5-turbo	24.2	27.3	60.6
gpt-3.5-turbo-instruct	50.5	N/A	70.7

Due to the space limit, we continue our answering in the following.

Q3. The paper only reports results using one language model. Can the authors evaluate CLOVER on a wider range of language models?

A. In this paper, we evaluate CLOVER on two language models, gpt-4o and gpt-4o-mini (The results using gpt-4o-mini are presented in Table 5, Appendix G). For further evaluation, we include additional two language models including gpt-3.5-turbo and gpt-3.5-turbo-instruct, which are another chat-focused model and an instruction-following model, respectively. As in Table 5, we compare performance of CLOVER and neurosymbolic approach baselines on the Puzzle and Symbol datasets. If the symbolic solver cannot execute the solution, then we take random guesses. We exclude the performance of SymbCoT using gpt-3.5-turbo-instruct since the prompt including few-shot examples exceeds the context window of the language model. The following results show that CLOVER clearly outperforms the baselines across different language models. We add this results in Appendix G. Due to the limitation of computational resources, we mainly use OpenAI models, but we will expand our evaluation on other proprietary models and open-sourced models.

Performance on Puzzle dataset using different language models.

Performance on Symbol dataset using different language models.

---

[1] Satlm: Satisfiability-aided language models using declarative prompting. Ye et al., 2024.
[2] Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. Pan et al., 2023.
[3] Linc: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. Olausson et al., 2023.
[4] Faithful logical reasoning via symbolic chain-of-thought. Xu et al., 2024.
[5] Chain-of-thought prompting elicits reasoning in large language models. Wei et al., 2022.
[6] Reliable reasoning beyond natural language. Borazjanizadeh & Piantadosi, 2024.

We thank the reviewer for the constructive and detailed comments. Q denotes a Question, and W denotes a Weakness not addressed in the Questions.

W1. The core idea of breaking down tasks into subtasks, using multiple samples, and verifying to select the best generation is not novel.

A. We would like to say that breaking down tasks into smaller ones and selecting the best generation is not our novelty. The novelty of this paper comes from how we break down logical sentences while preserving underlying logical structures and how we select the best first-order logic formula by fully leveraging the first-order logic semantics. To achieve the former one, we newly define a semantic parsing method called logical dependency parsing, and to achieve the latter one, we proposes two verification algorithms using a SAT solver. These contributions are summarized in the last paragraph of Introduction.

Q1. The approach is primarily applicable to problems that can be represented in a SAT solver, limiting its generalizability to other reasoning datasets, such as mathematical equations or visual reasoning tasks. Is it possible to extend CLOVER on these tasks?

A. We would like to emphasize that logical reasoning, where the problems are formally represented as a first-order logic, is one major category of reasoning. [2] states that logical reasoning plays a central role in intelligent systems for problem-solving, decision-making, and critical thinking. This paper and other prior works [1, 2, 3, 4] focus on enhancing the logical reasoning ability of LLMs. The other reasoning problems which require math or visual reasoning are out of the scope of this line of works.

Q2. The paper lacks comparison with CoT-based methods designed to improve implicit reasoning of language models [6]. Can the authors provide more insights into how CLOVER compares with these methods?

A. To clarify the meaning of CoT-based methods in the reviwer's question, we prepare two different answers.
If the reviewer means CoT-based methods as extracting information (i.e., natural language comments with logical code) that is implied but not directly stated, SatLM [1], Logic-LM [2], and SymbCoT [4] belongs to the methods designed to improve implicit reasoning of language models as in [6]. Specfically, [1] and [2] shares nearly the same method with [6] where the main difference comes from what symbolic solvers they use. CoT [5] also extracts implicit information in natural language. We do compare CLOVER with these methods in Table 1, and the results show that CLOVER clearly outperforms all these methods. For CLOVER, the preprocessing step (first equation of Eq. 2) includes extracting natural language sentences that are implied but not directly stated.

If the reviewer means CoT-based methods as CoT as is (i.e., step-by-step implicit reasoning through natural language), we want to emphasize the advantage of neurosymbolic approaches compared to CoT. While CoT falls short in complex logical reasoning tasks which need long sequence of reasoning, the neurosymbolic approaches including CLOVER resolve this issue by integrating a sound symbolic solver (line 39-48).

Dear Reviewer 5CZv,

We appreciate the time and effort you have dedicated to reviewing our paper. We hope our responses and additional results have addressed your concerns. If you have any further questions or suggestions, we would be grateful to hear them. Thank you once again for your valuable feedback throughout this process!

Best,
Authors

Dear Reviewer 5CZv,

As the discussion period deadline approaches, we hope we have addressed your concerns regarding the novelty of our approach, its generalizability to other reasoning tasks, comparisons with CoT-based methods, and evaluations on additional language models. We would greatly appreciate it if you could provide a response to our rebuttal. Please let us know if you have any further questions or concerns!

Best,
Authors