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

## Abstract

Abstract Complex logical reasoning tasks require a long sequence of reasoning, which a large language model (LLM) with chain-of-thought prompting still falls short. To alleviate this issue, neurosymbolic approaches incorporate a symbolic solver. Specifically, an LLM only translates a natural language problem into a satisfiability (SAT) problem that consists of first-order logic formulas, and a sound symbolic solver returns a mathematically correct solution.
However, we discover that LLMs have difficulties to capture complex logical semantics hidden in the natural language during translation. To resolve this limitation, we propose a C ompositional First-Order Lo gic Translation . An LLM first parses a natural language sentence into newly defined logical dependency structures that consist of an atomic subsentence and its dependents, then sequentially translate the parsed subsentences.
Since multiple logical dependency structures and sequential translations are possible for a single sentence, we also introduce two Ver ification algorithms to ensure more reliable results. We utilize an SAT solver to rigorously compare semantics of generated first-order logic formulas and select the most probable one.
We evaluate the proposed method, dubbed CLOVER, on seven logical reasoning benchmarks and show that it outperforms the previous neurosymbolic approaches and achieves new state-of-the-art results.

## 1 Introduction

Logical reasoning involves reaching conclusions through a structured process. It entails drawing inferences by converting the information provided in a set of premises into a final conclusion (Nunes, ; Bronkhorst et al., ).
Logical reasoning ability is one of the most challenging metrics to measure intelligence. As the language model size grows exponentially, large language models (LLMs) (Brown, ; Chen et al., ; Thoppilan et al., ) unlock the ability of machine to reason.

Chain-of-thought (CoT) prompting (Wei et al., ) significantly improve the performance of LLMs on simple logical reasoning tasks that require few forward reasoning steps. However, CoT falls short in complex logical reasoning tasks which need longer sequence of reasoning (Ye et al., ; Pan et al., ). To resolve this issue, several neurosymbolic approaches (Ye et al., ; Pan et al., ; Kirtania et al., ; Olausson et al., ) utilize an LLM with a symbolic solver (e.g., an SAT solver) on these complex logical reasoning tasks by the following two steps: 1) an LLM translates the natural language logical reasoning problem into a set of first-order logic formulas, 2) a symbolic solver automatically plans the reasoning steps and executes those to predict an answer of the logical reasoning problem.
These approaches take advantages by considering an LLM only as a semantic parser (i.e., a first-order logic translator), which can avoid planning and execution errors by using a symbolic solver.

Figure: (a)
Refer to caption: x1.png

However, we have discovered that LLMs still cannot translate sentences that represent complex first-order logic.
Our experimental evidence in Fig. 1(a) presents the drastic performance drop of the previous work (Pan et al., ) on complex first-order logic translation.(^1^11To evaluate the complexity and performance of each first-order logic formula, we sample the first problem from each set of problems that share the same context in the AR-LSAT test set and manually annotate the ground truth formulas. Detailed information of measuring complexity is in Appendix B and the process of the annotated subset construction is described in Appendix E.) The result indicates that an LLM performs first-order logic translation faithfully to a certain degree of complexity but falls short beyond that limit.
A representative example in Fig. 1(b) presents an incorrect output of the previous work (Pan et al., ) on complex first-order logic translation. The task is to translate a sentence “The Sales division is toured on two consecutive days, and on no other days.” into a corresponding first-order logic formula given declarations. An LLM correctly translates a natural language clause “The Sales division is toured on two consecutive days.” into a subformula $(\exists d:\textit{days})\,(\textit{toured}(d)=\textit{Sales})\land(\textit{
toured}(d+1)=\textit{Sales})$ which contains simple logic, but fails to translate “and on no other days” which represents more complex logic.
Specifically, the incorrectly translated subformula is always true, which has no semantic meaning.
After further extensive qualitative error analysis (Appendix I), we conclude that LLMs show promising performance on simple first-order logic translations but does not on complex ones, and the reason is that LLMs have difficulties to discover complex logical structures hidden behind the natural language.

To resolve this limitation, we take a hint from how humans perceive a complex logical sentence to their mind and how they translate it to a first-order logic formula. Since it is hard to immediately comprehend the semantics of a complex logical sentence, humans first understand the semantics of a simpler subsentence and then understand the whole (Montague et al., ; Frazier & Fodor, ; Sweller, ). Inspired by this observation, we use LLM to find the atomic subsentence that does not contain any complex logic and understand other sentence components as dependents of the atomic subsentence. Then, starting with the atomic subsentence, we use LLM to translate subsentences by accumulating sentence components. This could help LLM to preserve first-order logic semantics during translation.
To rigorously define the atomic subsentence and sentence components with logical meaning, we introduce a new parsing method for natural language that represents first-order logic, called logical dependency parsing (Section 3.1).

Based on logical dependency parsing, we propose a compositional first-order logic translation (Section 3.2) by few-shot learning with an LLM. It consists of the following three steps: logical dependency parsing, component accumulation, and sequential translation. First, a target sentence is parsed into logical dependency structures which consist of components of the sentence and their logical dependencies. Second, components are accumulated while preserving their logical dependencies, where the last accumulated sentence is the target sentence. Finally, each accumulated sentence is sequentially translated into first-order logic formula in the order of accumulations, where the last formula is an estimated formula of the target sentence.

Not only that, since there could be multiple outputs on logical dependency parsing and sequential translation, we introduce verification algorithms to ensure more reliable first-order logic translation (Section 3.3).
We propose two verification algorithms: logical consistency and disproving by counter-interpretation. To fully leverage the deterministic nature of first-order logic, we use an SAT solver to compare any two formulas.
Logical consistency selects the most frequent logically equivalent formulas. However, we observe that an LLM sometimes make logically consistent translation errors.
To overcome such a limitation, we devise disproving by counter-interpretation. It sequentially compares two formulas and disprove one of them by determining if a counter-interpretation to equivalence of two formulas satisfies the target sentence. The last formula remained is then selected.
To save computational cost, we compare each one of logically equivalent formulas.

We evaluate the proposed CLOVER, a Compositional First-Order Logic Translation and Verification, on seven logical reasoning benchmarks (Section 4).
CLOVER outperforms the previous neurosymbolic approaches and achieves the new state-of-the-art performance. It also significantly enhances the first-order logic translation accuracy across all levels of complexity and the largest performance gain occurs at the highest first-order logic complexity (Fig. 1(a)).

To summarize our contributions,

- 1.
We introduce CLOVER, a novel neurosymbolic approach that enhances complex logical reasoning in LLMs by compositional translation of natural language into first-order logic and verification of logical semantics.
- 2.
We newly define a logical dependency structure to decompose logical sentences while preserving an underlying first-order logic semantics.
- 3.
We also propose two SAT-based first-order logic verification algorithms that can faithfully select a correctly translated formula.
- 4.
We evaluate CLOVER on seven logical reasoning benchmarks and show that CLOVER outperforms the previous neurosymbolic apporoaches and achieves the new state-of-the-art performance.

## 2 Problem Formulation

Through the lens of (many-sorted) first-order logic(^2^22Many-sorted first-order logic is one of the variants of the standard first-order logic that allows variables to have different domains, which is called sorts $S$. We provide related preliminaries in Appendix A.), a logical reasoning problem $x$ is a natural language description of a $\Sigma$-theory $\mathcal{T}$(^3^33A theory assigns specific meanings to symbols of formulas. For simplicity, we presume that a theory $\mathcal{T}$ incorporates the most commonly applied theories (e.g., theory of equality, arithmetic, etc.).), constraints $\Phi$, and a query $q$, denoted as $x=NL(\mathcal{T},\Phi,q)$.
A $\Sigma$-theory $\mathcal{T}$ is a non-empty set of any $\Sigma$-structure where a signature $\Sigma=(S,F,P)$ consists of sorts $S$, function symbols $F$, and predicate symbols $P$. Hereinafter, we denote the vocabulary of first-order logic as italic for clarity, and omit the prefix “$\Sigma$-” for simplicity. A structure of a theory indicates the semantics of formulas.
Constraints $\Phi$ are a set of formulas that are true, denoted as $\Phi=\{\phi_{1},\phi_{2},\cdots,\phi_{K}\}$. A query $q$ is also a formula which is yet determined as true, false, or unknown given the constraints $\Phi$.

#### Prior works.

Prior neurosymbolic approaches (Ye et al., ; Pan et al., ; Kirtania et al., ; Olausson et al., ) directly translate the logical reasoning problem $x$ into a set of first-order logic using an LLM and then employ a symbolic solver (e.g., an SAT solver) to solve an SAT problem. In these methods, an LLM performs a single inference for the first-order logic translation as follows:

$$ $\hat{\mathcal{T}},\{\hat{\varphi}_{k},\hat{NL}(\varphi_{k})\}_{k=1}^{K+1}\sim P _{\text{LLM}}(\mathcal{T},\{\varphi_{k},NL(\varphi_{k})\}_{k=1}^{K+1}\mid x, \mathbf{x}_{\text{fs}})$ (1) $$

where $\varphi_{k}=\phi_{k}$ for $1\leq k\leq K$ and $\varphi_{K+1}=q$, and a few-shot exemplar set $\mathbf{x}_{\text{fs}}=\{x^{(i)},\mathcal{T}^{(i)},\{\varphi_{k}^{(i)},NL(
\varphi_{k}^{(i)})\}_{k=1}^{K^{(i)}+1}\}_{i=1}^{N}$ with the size of the set $N$.
However, it often generates more than one formulas for a single target sentence or generates a formula which is a translation of combination of a target sentence and part of other sentences. Though it might be logically correct as a whole, we cannot further analyze and verify the translation at a sentence-level.

#### First-order logic translation.

To resolve this drawback, we perform first-order logic translation for each sentence.
Since sentence-level translations require a pre-defined theory, we first generate a theory $\hat{\mathcal{T}}$ and a set of natural language sentences $\{\hat{NL}(\varphi_{k})\}_{k=1}^{K+1}$ from $x$, and then generate $\hat{\mathcal{T}}$-satisfiable formula $\hat{\varphi}_{k}$ for each sentence $\hat{NL}(\varphi_{k})$.
To be specific, the single inference by the LLM in Eq. 1 is separated into the following two steps: 1) given a logical reasoning problem $x$ and a few-shot exemplar set $\mathbf{x}_{\text{fs}}^{\text{prep}}=\{x^{(i)},\mathcal{T}^{(i)},\{NL(\varphi_
{k}^{(i)})\}_{k=1}^{K^{(i)}+1}\}_{i=1}^{N}$, the LLM generates a tuple of an estimated theory and a set of natural language sentences, denoted $x^{\text{prep}}=(\hat{\mathcal{T}},\{\hat{NL}(\varphi_{k})\}_{k=1}^{K+1})$, 2) given the theory $\hat{\mathcal{T}}$ and a set of few-shot exemplar sets $\mathbf{X}_{\text{fs}}$, the proposed CLOVER translates each natural language sentence $\hat{NL}(\varphi_{k})$ into the estimated formula $\hat{\varphi}_{k}$ that is $\hat{\mathcal{T}}$-satisfiable as follows:

$$ $\displaystyle\hat{\mathcal{T}},\{\hat{NL}(\varphi_{k})\}_{k=1}^{K+1}$ $\displaystyle\sim P_{\text{LLM}}(\mathcal{T},\{NL(\varphi_{k})\}_{k=1}^{K+1} \mid x,\mathbf{x}_{\text{fs}}^{\text{prep}})$ (2) $\displaystyle\hat{\varphi}_{k}$ $\displaystyle=\text{CLOVER}(\hat{\mathcal{T}},\hat{NL}(\varphi_{k}),\mathbf{X} _{\text{fs}}),\forall{k}\in\{1,2,\cdots,K+1\}.$ $$

A detailed description of the set of few-shot exemplar sets $\mathbf{X}_{\text{fs}}=\{\mathbf{x}_{\text{fs}}^{\text{parse}},\mathbf{x}_{
\text{fs}}^{\text{accum}},\mathbf{x}_{\text{fs}}^{\text{trans}},\mathbf{x}_{
\text{fs}}^{\text{disprv}}\}$ and the proposed CLOVER for $x^{\text{prep}}=(\hat{\mathcal{T}},\{\hat{NL}(\varphi_{k})\}_{k=1}^{K+1})$ will be discussed in the following section.

#### SAT problem solving.

Once the estimations of the theory $\hat{\mathcal{T}}$, constraints $\hat{\Phi}=\{\hat{\varphi}_{1},\hat{\varphi}_{2},\cdots,\hat{\varphi}_{K}\}$, and a query $\hat{q}=\hat{\varphi}_{K+1}$ are completed for the logical reasoning problem $x$, these form an SAT problem $\mathcal{P}=(\hat{\mathcal{T}},\hat{\Phi},\hat{q})$.
An automated SAT solver then determines the $\hat{\mathcal{T}}$-satisfiability of the query $\hat{q}$ under the constraints $\hat{\Phi}$, which is a final prediction of an answer of the logical reasoning problem $x$.
We use a Z3 theorem prover (De Moura & Bjørner, ) as an SAT solver in the implementation.

## 3 CLOVER

Figure: Figure 2: Overview of CLOVER. Given declarations of a theory, CLOVER parses a target sentence to several possible logical dependency structures, accumulates components according to logical dependencies, and sequentially translates subsentences to first-order logic formulas. Then, CLOVER verifies a set of estimated formulas. Logical consistency selects the most frequent logically equivalent formulas. Disproving by counter-interpretation sequentially compares two formulas and disprove one by determining if a counter-interpretation satisfies the target sentence.
Refer to caption: x3.png

In this section, we propose CLOVER, a Compositional First-Order Logic Translation and Verification for complex logical reasoning.
To fully capture first-order logic semantics in natural language, it first parses a single natural language sentence into logical dependency structures. Then, it sequentially translates parsed subsentences with an LLM.
Since there are multiple ways to parse and translate the sentences, we also introduce two SAT-based verification algorithms to thoroughly compare semantics of translated first-order logic formulas.

### 3.1 Logical Dependency Structures

Logical dependency structure $\mathcal{A}$ of a sentence $NL(\varphi)$ under the theory $\mathcal{T}$ where $\varphi$ is $\mathcal{T}$-satisfiable is defined by components and their logical dependencies.
First, components are natural language building blocks of logical dependency structures of a sentence, which consist of logic units $U$, logic couplers $C$, and logic dependents $D$. The following definitions formally describe each of them.

###### Definition 1 (Logic units) .

Given a sentence $NL(\varphi)$ and a theory $\mathcal{T}$ where $\varphi$ is $\mathcal{T}$-satisfiable, logic units $U$ are the natural language descriptions of an atom of $\varphi$.

###### Definition 2 (Logic couplers) .

Logic couplers $C$ are either conjunctions or an operator named merge. Merge combines two logic units which contain the natural language describing the same term without adding any conjunction.

###### Definition 3 (Logic dependents) .

Logic dependents $D$ are components neither logic units nor logic couplers which logically depend on another component.

Second, we define logical dependency between two components, and the following definition formally describes it.

###### Definition 4 (Logical dependency) .

The component $X$ is said to logically depend on the component $Y$ in the given sentence if and only if the meaning of $Y$ is (or includes) a predicate and the meaning of $X$ is an argument of this predicate in the sentence.

We also introduce properties of logical dependency structure stemmed from its definition.

###### Remark 1 .

A given sentence and theory can have multiple logical dependency structures.

###### Remark 2 .

All components except for one should logically depend on another component.

###### Remark 3 .

No logic dependent logically depends on a logic coupler.

We present an example of logical dependency structures in Fig. 2 and additional examples in Appendix D.

###### Definition 1 (Logic units) .

###### Definition 2 (Logic couplers) .

###### Definition 3 (Logic dependents) .

###### Definition 4 (Logical dependency) .

###### Remark 1 .

###### Remark 2 .

###### Remark 3 .

### 3.2 Compositional First-Order Logic Translation

To compositionally translate natural language sentences to first-order logic formulas under given theory for $x^{\text{prep}}=(\hat{\mathcal{T}},\{\hat{NL}(\varphi_{k})\}_{k=1}^{K+1})$, we adhere to the following three steps by few-shot learning with an LLM. We describe the following steps for a single target sentence $\hat{NL}(\varphi)$ of a formula $\varphi\in\{\varphi_{k}\}_{k=1}^{K+1}$.

#### Logical Dependency Parsing.

In the first step, a target sentence is parsed into different possible logical dependency structures.
An LLM is given a definition of logical dependency structures (Section 3.1), a target sentence $\hat{NL}(\varphi)$ and its theory $\hat{\mathcal{T}}$, and a few-shot exemplar set $\mathbf{x}_{\text{fs}}^{\text{parse}}=\{\mathcal{T}^{(i)},NL(\varphi^{(i)}),\{
\mathcal{A}^{(i)}_{l}\}_{l=1}^{L^{(i)}}\}_{i=1}^{N}$ for logical dependency parsing. $L^{(i)}$ is a size of a set of different possible logical dependency structures of a sentence $NL(\varphi^{(i)})$ under the theory $\mathcal{T}^{(i)}$, and $N$ is a size of the few-shot exemplar set.
Then, LLM generates a set of different possible logical dependency structures $\{\hat{\mathcal{A}}_{l}\}_{l=1}^{\hat{L}}$ of the target sentence with the size of the set $\hat{L}$ as follows:

$$ $\displaystyle\hat{L},\{\hat{\mathcal{A}}_{l}\}_{l=1}^{\hat{L}}\sim P_{\text{ LLM}}(L,\{\mathcal{A}_{l}\}_{l=1}^{L}\mid\hat{\mathcal{T}},\hat{NL}(\varphi), \mathbf{x}_{\text{fs}}^{\text{parse}}).$ (3) $$

#### Component Accumulation.

In the second step, components of a logical dependency structure are accumulated to gradually compose new sentences until those reach the target sentence. We present the rules for component accumulation in Appendix C.
An LLM is given a definition of logical dependency structures (Section 3.1), rules for component accumulation (Appendix C), a target sentence $\hat{NL}(\varphi)$ and one of its logical dependency structures $\hat{\mathcal{A}}_{l}$ where $l\in\{1,2,\cdots,\hat{L}\}$, and a few-shot exemplar set $\mathbf{x}_{\text{fs}}^{\text{accum}}=\{NL(\varphi^{(i)}),\mathcal{A}^{(i)},(S
^{(i)}_{m})_{m=1}^{M^{(i)}}\}_{i=1}^{N}$ for component accumulation. $(S^{(i)}_{m})_{m=1}^{M^{(i)}}$ is a sequence of accumulated sentences where $M^{(i)}$ is the length of the sequence.
Then, LLM generates a sequence of sentences $(\hat{S}_{l,m})_{m=1}^{\hat{M}_{l}}$ where $\hat{M}_{l}$ is the length of the estimated sequence as follows:

$$ $\displaystyle\hat{M}_{l},(\hat{S}_{l,m})_{m=1}^{\hat{M}_{l}}\sim P_{\text{LLM} }(M_{l},(S_{l,m})_{m=1}^{M_{l}}\mid\hat{NL}(\varphi),\hat{\mathcal{A}}_{l}, \mathbf{x}_{\text{fs}}^{\text{accum}}),\forall l\in\{1,2,\cdots,\hat{L}\}.$ (4) $$

The last sentence of accumulation $\hat{S}_{l,\hat{M}_{l}}$ is the target sentence $\hat{NL}(\varphi)$.
We present examples of component accumulation in Appendix D.

#### Sequential Translation.

In the last step, accumulated natural language sentences are sequentially translated into first-order logic formulas, which the target sentence is finally translated.
An LLM is given a sequence of accumulated sentences $(\hat{S}_{l,m})_{m=1}^{\hat{M}_{l}}$ of a target sentence where $l\in\{1,2,\cdots,\hat{L}\}$, a theory $\hat{\mathcal{T}}$, and a few-shot exemplar set $\mathbf{x}_{\text{fs}}^{\text{trans}}=\{\mathcal{T}^{(i)},(S^{(i)}_{m})_{m=1}^
{M^{(i)}},(\varphi^{(i)}_{m})_{m=1}^{M^{(i)}}\}_{i=1}^{N}$ for first-order logic translation.
Then, LLM generates a sequence of formulas $(\hat{\varphi}_{l,m})_{m=1}^{\hat{M}_{l}}$ as follows:

$$ $\displaystyle(\hat{\varphi}_{l,m})_{m=1}^{\hat{M}_{l}}\sim P_{\text{LLM}}(( \varphi_{l,m})_{m=1}^{\hat{M}_{l}}\mid\hat{\mathcal{T}},(\hat{S}_{l,m})_{m=1}^ {\hat{M}_{l}},\mathbf{x}_{\text{fs}}^{\text{trans}}),\forall l\in\{1,2,\cdots, \hat{L}\}.$ (5) $$

The last formula of the sequence is the first-order logic translation of the target sentence (i.e., $\hat{\varphi}_{l}=\hat{\varphi}_{l,\hat{M}_{l}}$). For $\forall l\in\{1,2,\cdots,\hat{L}\}$, we could generate a set of estimated formulas $\hat{\Psi}=\{\hat{\varphi}_{l}\}_{l=1}^{\hat{L}}$ for a target sentence $NL(\varphi)$.
In practice, we randomly sample multiple times to enrich the pool of estimated formulas that benefits the second stage of CLOVER, first-order logic verification.

### 3.3 First-Order Logic Verification

To select the most probable formula in a set of compositionally translated first-order logic formulas $\hat{\Psi}$, we introduce the following two algorithms using an SAT solver (and few-shot learning with an LLM).
As in Section 3.2, we describe the following algorithms for a single target sentence $\hat{NL}(\varphi)$ under the theory $\hat{\mathcal{T}}$ (i.e., The algorithms select a verified formula $\varphi^{*}$ in a set of estimated formulas $\hat{\Psi}$).
Prior to describing the detailed algorithms, we filter out the formulas that are syntactically incorrect or $\hat{\mathcal{T}}$-unsatisfiable in $\hat{\Psi}$ using an SAT solver and call the processed set $\hat{\Psi}_{\text{sat}}$.

#### Logical Consistency.

We select the most frequent logically equivalent formulas, which we call this algorithm logical consistency.
It presumes an LLM utilizes different logical dependency structures to generate several formulas that are logically equivalent. An LLM might also make mistake in intermediate steps of compositional first-order logic translation and generate incorrect formulas, but these are less likely to be logically equivalent.
For each pair of formulas $(\varphi_{p},\varphi_{q})$ such that $\varphi_{p}\in\hat{\Psi}_{\text{sat}}$, $\varphi_{q}\in\hat{\Psi}_{\text{sat}}$, and $p\neq q$, an SAT solver determines their $\hat{\mathcal{T}}$-equivalence. Then, we group $\hat{\mathcal{T}}$-equivalent formulas and select any formula in the group that has the largest number of elements.
However, we observe that an LLM sometimes makes consistent mistakes in the last step of compositional first-order logic translation, which leads to logically equivalent incorrect formulas.

#### Disproving by Counter-Interpretation.

To resolve this issue, we introduce an advanced algorithm that sequentially disproves incorrect formulas by counter-interpretation. Following this algorithm, an accurate formula remains the last if it exists in $\hat{\Psi}_{\text{sat}}$.
Specifically, we select a random element $\hat{\varphi}_{0}$ in $\hat{\Psi}_{\text{sat}}$ and initialize the verified formula $\varphi^{*}$ to $\hat{\varphi}_{0}$. For each estimated formula $\hat{\varphi}$ in $\hat{\Psi}_{\text{sat}}\setminus\{\hat{\varphi}_{0}\}$, an SAT solver determines if $(\varphi^{*}\land\lnot\hat{\varphi})$ is $\hat{\mathcal{T}}$-satisfiable.
First, if it is $\hat{\mathcal{T}}$-satisfiable, an SAT solver finds a counter-interpretation $I$ to a $\hat{\mathcal{T}}$-equivalence of $\varphi^{*}$ and $\hat{\varphi}$ that satisfies $(\varphi^{*}\land\lnot\hat{\varphi})$. Given a target sentence $\hat{NL}(\varphi)$, a counter-interpretation $I$, and a few-shot exemplar set $\mathbf{x}_{\text{fs}}^{\text{disprv}}=\{NL(\varphi)^{(i)},I^{(i)},e^{(i)}\}_{
i=1}^{N}$ for disproving, an LLM decides if $I$ satisfies $\varphi$, which returns a boolean value $\hat{e}$.
If $\hat{e}$ is True, then $\hat{\varphi}$ is disproved since $I$ does not satisfy $\hat{\varphi}$ but satisfies $\varphi$. If $\hat{e}$ is False, then $\varphi^{*}$ is disproved since $I$ satisfies $\varphi^{*}$ but does not satisfy $\varphi$.
Second, if $(\varphi^{*}\land\lnot\hat{\varphi})$ is $\hat{\mathcal{T}}$-unsatisfiable, it is equivalent to $(\varphi^{*}\rightarrow\hat{\varphi})$ is $\hat{\mathcal{T}}$-satisfiable, and no $I$ exists.
After repeating this decision process for $(\hat{\varphi}\land\lnot\varphi^{*})$, we can consider a counter-interpretation $I$ that satisfies $(\hat{\varphi}\land\lnot\varphi^{*})$ and disproves accordingly. We select the verified formula $\varphi^{*}$ that remains the last. Algorithm 1 summarizes the whole process.

Figure: Algorithm 1 First-Order Logic Verification (Disproving by Counter-Interpretation)

## 4 Experiments

### 4.1 Setup

#### Tasks.

We evaluate CLOVER on seven logical reasoning tasks: AR-LSAT (Zhong et al., ), ZebraLogic (Bill Yuchen Lin, ), Logic grid puzzle (Puzzle), Symbol interpretation (Symbol), and Logical deduction (Deduction) from the BigBench collaborative benchmark (Srivastava et al., ), FOLIO (Han et al., ), and ProofWriter (Tafjord et al., ).
AR-LSAT consists of analytical reasoning problems of the law school admission test, and ZebraLogic is a benchmark for zebra puzzles. Puzzle, Symbol, and Deduction are tasks from logical reasoning category in the BigBench.
FOLIO(^4^44We use a revised version of FOLIO that improves sample quality and fixes errors, which is released on: [https://huggingface.co/datasets/yale-nlp/FOLIO](https://huggingface.co/datasets/yale-nlp/FOLIO).) is an expert-written first-order logic reasoning task, and ProofWriter is a deductive reasoning benchmark.
Note that all tasks except ZebraLogic are multiple choice problems, and Appendix E describes details of each task.

#### Language Models.

We perform our experiments mainly on gpt-4o (OpenAI, ), a current state-of-the-art LLM for complex, multi-step tasks, unless stated.
We also evaluate CLOVER and the baselines using a smaller model, gpt-4o-mini (OpenAI, ).(^5^55To specify language model versions provided by OpenAI, we use gpt-4o-2024-05-13 and gpt-4o-mini-2024-07-18 on our experiments.)
To reproduce our experiments, we set the temperature to 0 and select the highest probability response from the model.

#### Baselines.

We compare CLOVER primarily to Logic-LM (Pan et al., ), a state-of-the-art neurosymbolic approach for logical reasoning. There are few more works (Ye et al., ; Olausson et al., ) nearly the same to Logic-LM, but we focus on Logic-LM since their difference is marginal.
We also compare CLOVER to another neurosymbolic approach (Xu et al., ) which uses an LLM to solve SAT problems instead of using a symbolic solver.
In addition, we compare to the standard prompting and CoT prompting that leverages in-context learning capability of the base LLMs.
For fair comparison, we manually sample or derive our few-shot exemplar sets from those in the previous works (Pan et al., ; Xu et al., ) if it is possible.
Since the previous works do not evaluate their models on ZebraLogic, Puzzle, and Symbol, we randomly select a single exemplar problem outside the test set.
We demonstrate exemplar few-shot prompts in Appendix H.

#### Evaluation metrics.

We measure the performance of CLOVER and the baselines primarily by the correctness of the logical reasoning problem.
For neurosymbolic approaches with a symbolic solver, if the solver cannot execute the translated SAT problem, we fall back to CoT predictions.
From this unique property, following Pan et al. (), we use three additional evaluation metrics: program accuracy, execution rate, and execution accuracy, for multiple choice problems. Program accuracy does not include the CoT predictions for unexecutable problems. Execution rate measures the portion of executable problems, and execution accuracy indicates the accuracy for executable problems.

### 4.2 Results

Table: Table 1: Performance on logical reasoning tasks using CLOVER and the baseline methods.

Table: Table 2: Comparison of program accuracy, execution rate, and execution accuracy of CLOVER and Logic-LM.

We present the performance of CLOVER and the baselines on different tasks, different evaluation metrics, and different language model scales.
First, Table 1 compares the performance of CLOVER and the baselines on seven logical reasoning tasks.
CLOVER outperforms Logic-LM and other baselines by a significant margin across different logical reasoning tasks.
CLOVER shows marked improvement on hard logical reasoning tasks.
Specifically, it enhances the performance of Logic-LM on AR-LSAT by 20.4% and ZebraLogic by 30.0%.
Overall, neurosymbolic approaches with a symbolic solver (CLOVER and Logic-LM) show remarkable improvement on these hard reasoning tasks.

Second, Table 2 presents three additional evaluations for the neurosymbolic approaches with a symbolic solver.
CLOVER shows higher execution rate on every task, which indicates that CLOVER has better capability to generate syntactically correct first-order logic formulas than Logic-LM. CLOVER also shows higher execution accuracy on most tasks, which indicates that CLOVER has better capability to generate logically (or semantically) correct formulas than Logic-LM. These two observations lead to an outperforming program accuracy of CLOVER across different logical reasoning tasks.
Specifically, CLOVER increases the execution rate of Logic-LM on AR-LSAT by 25.9% and the execution accuracy by 27.0%, which finally leads to more than doubled program accuracy of Logic-LM.
Lastly, we compare the performance of CLOVER and the baselines on different languange model scales in Appendix F.

### 4.3 Ablations

Table: Table 3: Ablation of CLOVER on AR-LSAT and ZebraLogic.

We conduct ablation studies of CLOVER on two perspectives: compositional translation and verification, in Table 3.
Ablating verification from CLOVER (i.e., random selection) shows 6.9% and 4.2% performance degradation on AR-LSAT and ZebraLogic, respectively. It clearly supports the effectiveness of the verification.
Ablating compositional translation from CLOVER (i.e., direct translation) shows 7.3% and 14.6% performance degradation on AR-LSAT and ZebraLogic, respectively. It also clearly supports the effectiveness of the compositional translation. To maintain the verification stage as is, we repeat the sampling of direct translation five times, which is slightly larger than the average number of estimated formulas of CLOVER.
Ablating both compositional translation and verification from CLOVER shows further performance loss.
Additionally, disproving by counter-interpretation yields better performance than logical consistency.

### 4.4 Analysis

#### Types of Errors.

We analyze error types of CLOVER on AR-LSAT and compare those to Logic-LM’s in Figure 3. Since an SAT solver is sound and does not cause any error, our error analysis focuses on the first-order logic translation.
Logic-LM’s errors are mainly caused by incorrect logic (or semantic) and incorrect syntax, which take 53.7% of the total errors. There are preprocessing errors and other errors caused by an incorrect selection of a satisfiability function and limited expressiveness of a Z3 theorem prover.
In contrast, we highlight that CLOVER has nearly no logic or syntax error. CLOVER’s errors are primarily caused by preprocessing and other errors, which takes 78.6% of the total errors.
This analysis indicates that CLOVER significantly enhances the ability of a language model to generate both syntactically and semantically precise first-order logic formulas.

#### Robustness on Reasoning Length.

We present robustness of CLOVER on long sequence of reasoning and compare the results with CoT-based reasoning LLMs(^6^66We use CoT-based reasoning LLMs that were recently released from OpenAI, specifically o1-preview-2024-09-12 and o1-mini-2024-09-12, for our analysis.) in Figure 4. We also add the results of Logic-LM to measure the effect of neurosymbolic approach on reasoning length.
We observe a noticeable performance drop of CoT-based reasoning LLMs on long sequence of reasoning, which is a frequently pointed-out drawback of the CoT-based approaches. However, neurosymbolic approaches show robustness to the reasoning length. Specifically, CLOVER shows only 12.5% performance drop between the tasks of the shortest and longest sequence of reasoning.

Figure: Figure 3: Occurences of different error types of CLOVER and Logic-LM on AR-LSAT annotated subset.

Figure: Figure 4: Performance on different reasoning lengths using CoT-based reasoning LLMs and neurosymbolic approaches on ZebraLogic. Each example is a puzzle of five houses with varying # of features.

## 5 Related Works

#### LLM-based neurosymbolic approach for reasoning.

Previous works (Ye et al., ; Pan et al., ; Olausson et al., ; Kirtania et al., ) utilize an LLM as a semantic parser which translates the natural language logical reasoning problems into first-order logic formulas, and then use a symbolic solver to automatically solve an SAT problem.
There is another work (Xu et al., ) that utilizes an LLM as not only a semantic parser but also a symbolic solver and a verifier for semantic parsing and symbolic solving.
However, these previous works share a common drawback that an LLM cannot faithfully perform complex first-order logic translation, which fundamentally limits the performance of neurosymbolic approaches on complex logical reasoning tasks.

#### LLM-based problem decomposition.

To solve natural language tasks, previous works explore decomposing complex problems into several simpler ones using LLMs.
Drozdov et al. () use an LLM to syntactically parse the natural language sentence into several subsentences and performs compositional semantic parsing for simple tasks such as text-to-SQL.
However, since a syntactic parsing cannot preserve the semantic of logic, Drozdov et al. () is not applicable to complex logical reasoning tasks.
Other works (Zhou et al., ; Khot et al., ; Press et al., ; Dua et al., ; Ye et al., ) focus on decomposing simple question-answering problems by prompting LLMs with few-shot examples. However, if LLMs simply rely on few-shot examples for decomposing complex logical reasoning problems, then the problems might be incorrectly decomposed, which leads to an unexpected performance loss.

#### LLM-generated formal language verification.

There are lines of works to verify formal language generated by LLMs.
Chen et al. () and Madaan et al. () first generate a code from natural language, get feedback from an LLM, and refine the code based on the feedback. Chen et al. () additionally utilizes an external feedback signal from an executor.
Ni et al. () first generates candidate codes from natural language and then verify by predicting their correctness using a trained neural network.
However, these model-based verifications show limited performance on complex logical reasoning tasks (Appendix G).

## 6 Conclusion

We propose CLOVER, a compositional first-order logic translation and verification for complex logical reasoning.
CLOVER first parses the natural language sentence into newly defined logical dependency structures, which reflect first-order logic semantics hidden in the natural language, and then compositionally translates the sentence.
We also introduce two verification algorithms using satisfiability to fully cover first-order logic semantics.
Empirical results show that CLOVER achieves state-of-the-art performance on seven logical reasoning benchmarks.

## Appendix A First-Order Logic Preliminaries

To clarify the first-order logic vocabularies used in the paper, we give basic definitions as preliminaries based on Ranise et al. () and Jovanović & Barrett ().
To help understanding, we also provide an example of the definitions, where the example is sampled from the AR-LSAT test set (Zhong et al., ).
In this work, we use many-sorted first-order logic, which is one of the variants of the standard first-order logic, to better reflect the scenarios of the real-world logical reasoning problems.

### A.1 Syntax

The syntax of many-sorted first-order logic is built on signatures. We first define signatures, and on top of that, we define variables, terms, atoms, literals, clauses, and formulas.

###### Definition 5 (Signatures) .

A signature $\Sigma=(S,F,P)$ consists of countable sets of sorts $S$, function symbols $F$, and predicate symbols $P$.
Each function symbol $f$ is associated with a type $s_{1}\times\cdots\times s_{n}\rightarrow s$, where $n\geq 0$ and $s_{1},\cdots,s_{n},s\in S$. Function symbols with $n=0$ (i.e. zero arity) are called constants of sort $s$.
Each predicate symbol $p$ is associated with a type $s_{1}\times\cdots\times s_{n}$, where $n\geq 1$ and $s_{1},\cdots,s_{n}\in S$.

Let $\Sigma$ be a signature.
A set $X$ of $\Sigma$-variables (or simply variables) is a countable set of variable names. Each variable name is associated with a sort in $\Sigma$.
Based on variables, we define terms. Intuitively, terms are variables or functions applied to a tuple of other terms.

###### Definition 6 (Terms) .

$\Sigma$-terms over $X$ (or simply terms) are defined as follows. Each variable $x\in X$ of sort $s$ is a term of sort $s$. If $t_{1},\cdots,t_{n}$ are terms of sorts $s_{1},\cdots,s_{n}$, respectively, and $f$ is a function symbol of type $s_{1}\times\cdots\times s_{n}\rightarrow s$, then $f(t_{1},\cdots,t_{n})$ is a term of sort $s$.

Based on terms, we define atoms. Intuitively, atoms are predicates applied to a tuple of terms.

###### Definition 7 (Atoms) .

$\Sigma$-atoms over $X$ (or simply atoms) are defined as follows. If $t_{1},\cdots,t_{n}$ are $\Sigma$-terms over $X$ of sorts $s_{1},\cdots,s_{n}$, respectively, and $p$ is a predicate symbol with the type $s_{1}\times\cdots\times s_{n}$, then $p(t_{1},\cdots,t_{n})$ is an atom.

Additionally, literals are atoms or negation of atoms, and clauses are disjunctions of literals.
We finally define formulas by using above definitions with logical connectives and quantifiers.

###### Definition 8 (Formulas) .

$\Sigma$-formulas over $X$ (or simply formulas) are defined as follows. Each $\Sigma$-atom over $X$ is a formula. If $\alpha$ and $\beta$ are formulas, then so are $\lnot\alpha$, $\alpha\land\beta$, and $\alpha\lor\beta$. If $x\in X$ is a variable of sort $s$ and $\alpha$ is a formula, then so are $\exists x\,\alpha$ and $\forall x\,\alpha$.

We give an example of the definitions of first-order logic syntax with the following formula in the AR-LSAT test set.

###### Example 1 .

A signature is given as

$$ $\Sigma_{1}=(\{\textit{positions},\textit{potters}\},F,P)$ $$

where $F=\{\textit{displayed},\textit{Reigel},1,6\}$ such that displayed has the type $\textit{positions}\rightarrow\textit{potters}$, Reigel is a constant of sort potters, and $1$ and $6$ are constants of sort positions, and $P=\{\approx\}$ such that $\approx$ is of the type $\textit{positions}\times\textit{positions}$. We note that the equality symbol $\approx$ is always implicit from the context.
If $p$ is a variable of sort positions, then $p$ and $\textit{displayed}(p)$ are $\Sigma_{1}$-terms of sort positions.
Then, $\textit{displayed}(p)\approx\textit{Reigel}$, $p\approx 1$, and $p\approx 6$ are $\Sigma_{1}$-atoms.
Finally, the following is one example of a $\Sigma_{1}$-formula

$$ $(\forall p:\textit{positions})\,(\textit{displayed}(p)\approx\textit{Reigel}) \rightarrow(p\approx 1\lor p\approx 6)$ $$

which is the first-order logic translation of the natural language sentence “Reigel’s bowl can be displayed only in either position 1 or position 6”.

###### Definition 5 (Signatures) .

###### Definition 6 (Terms) .

###### Definition 7 (Atoms) .

###### Definition 8 (Formulas) .

###### Example 1 .

### A.2 Semantics

The semantics of many-sorted first-order logic is indicated by structures. We first define structures and extend its concept to define interpretations. On top of those, we define theories with models and consequences.

A signature $\Sigma=(S,F,P)$ only describes the names of sorts, functions, and predicates. However, it does not describe assignments of elements to each sort and evaluations of functions and predicates on the elements of sorts. Structures add this information.

###### Definition 9 (Structures) .

A $\Sigma$-structure $I$ assigns a non-empty domain set $D_{s}$ to each sort $s\in S$, a function $f^{I}:D_{s_{1}}\times\cdots\times D_{s_{n}}\rightarrow D_{s}$ for each function symbol $f\in F$ of type $s_{1}\times\cdots\times s_{n}\rightarrow s$, and a predicate $p^{I}:D_{s_{1}}\times\cdots\times D_{s_{n}}\rightarrow\{\text{F},\text{T}\}$ for each predicate symbol $p\in P$ of type $s_{1}\times\cdots\times s_{n}$.
Note that each constant $c$ of sort $s$ is mapped to an element $c^{I}\in D_{s}$.

To evaluate terms and formulas, we extend structures to variables and define interpretations.

###### Definition 10 (Interpretations) .

$\Sigma$-interpretation $I$ over $X$ (or simply interpretation) is a $\Sigma$-structure that additionally assigns a value $x^{I}\in D_{s}$ to each variable $x\in X$ of sort $s$.

We denote $I\vDash\phi$ if an interpretation $I$ evaluates a formula $\phi$ to true. However, we are not usually interested in the evaluation of formulas in a given structure, but interested in specific meaning of functions and predicates. Theories deal with this problem.

###### Definition 11 (Theories) .

A $\Sigma$-theory $T$ (or simply theory) is a non-empty set of $\Sigma$-structures.

To solve practical problems, we additionally define the followings. A $T$-interpretation is a $\Sigma$-interpretation $I$ that extends some structure in the theory $T$. A formula $\phi$ is $T$-satisfiable if $I\vDash\phi$ for some $T$-interpretation $I$. A formula $\phi$ is $T$-valid, denoted by $\vDash_{T}\phi$, if $I\vDash\phi$ for all $T$-interpretations $I$.
We also introduce definitions to describe the relationship between an interpretation and a formula, and between two formulas.

###### Definition 12 (Models) .

A $T$-interpretation $I$ such that $I\vDash\phi$ is called a $T$-model of $\phi$.

###### Definition 13 (Consequences) .

A formula $\phi$ is a $T$-consequence of a formula $\psi$, denoted by $\psi\vDash_{T}\phi$, if $I\vDash\psi$ implies $I\vDash\phi$ for all $T$-interpretations $I$.

We give an example of the definitions of first-order logic semantics by continuing Example 1.

###### Example 2 .

Let us consider the extended signature $\Sigma_{2}=(\{\textit{positions},\textit{potters}\},F,\{\approx\})$ where

$$ $F=\{\textit{displayed},\textit{Larsen},\textit{Mills},\textit{Neiman},\textit{ Olivera},\textit{Park},\textit{Reigel},\textit{Serra},\textit{Vance},1,2,3,4,5 ,6\}.$ $$

There are many possible $\Sigma_{2}$-structures, and one exemplar structure $I_{2}$ is:

- $\bm{\cdot}$
$D_{\text{positions}}=\{1,2,3,4,5,6\}$,
- $\bm{\cdot}$
$D_{\text{potters}}=\{\textit{Larsen},\textit{Mills},\textit{Neiman},\textit{
Olivera},\textit{Park},\textit{Reigel},\textit{Serra},\textit{Vance}\}$,
- $\bm{\cdot}$
$\textit{Larsen}^{I_{2}}=\textit{Larsen}$, $\textit{Mills}^{I_{2}}=\textit{Mills}$, $\textit{Neiman}^{I_{2}}=\textit{Neiman}$, $\textit{Olivera}^{I_{2}}=\textit{Olivera}$,
$\textit{Park}^{I_{2}}=\textit{Park}$, $\textit{Reigel}^{I_{2}}=\textit{Reigel}$, $\textit{Serra}^{I_{2}}=\textit{Serra}$, $\textit{Vance}^{I_{2}}=\textit{Vance}$,
- $\bm{\cdot}$
$1^{I_{2}}=1$, $2^{I_{2}}=2$, $3^{I_{2}}=3$, $4^{I_{2}}=4$, $5^{I_{2}}=5$, $6^{I_{2}}=6$, and
- $\bm{\cdot}$
$\textit{displayed}^{I_{2}}(1)=\textit{Reigel}$, $\textit{displayed}^{I_{2}}(2)=\textit{Larsen}$, $\textit{displayed}^{I_{2}}(3)=\textit{Reigel}$,
$\textit{displayed}^{I_{2}}(4)=\textit{Reigel}$, $\textit{displayed}^{I_{2}}(5)=\textit{Reigel}$, $\textit{displayed}^{I_{2}}(6)=\textit{Reigel}$.

Since we do not consider any additional variable here, $\Sigma_{2}$-interpretation $I_{2}^{\prime}$ is the same as $I_{2}$.

Now, let the theory $T_{2}$ be the $\Sigma_{2}$-theory consisting only of the $\Sigma_{2}$-structure $I$ which has the same domain assignment to each sort and the same constant function assignments with $I_{2}$.
$I_{2}$ is a $T_{2}$-interpretation. If we consider the formula $\phi$ in Example 1, $\phi$ is $T_{2}$-satisfiable, but not $T_{2}$-valid.

Lastly, let us determine if $I_{2}$ satisfies $\phi$. Reigel’s bowl is displayed in the positions $1$ and $6$, but it is also displayed in positions $3$, $4$, and $5$. A $T_{2}$-interpretation $I_{2}$ does not satisfy the formula $\phi$, which means $I_{2}$ is not a $T_{2}$-model of $\phi$.

###### Definition 9 (Structures) .

###### Definition 10 (Interpretations) .

###### Definition 11 (Theories) .

###### Definition 12 (Models) .

###### Definition 13 (Consequences) .

###### Example 2 .

## Appendix B First-Order Logic Complexity

To quantitatively measure the complexity of first-order logic formulas, we use a parameter following Arias & Khardon ().
The target formula is first transformed into an expression in a conjunctive normal form (CNF).
Then, the complexity parameter is defined as a sum of three components, the number of clauses in the CNF expression, the maximum number of distinct terms in any clause of the CNF expression, and the maximum number of literals in any clause of the CNF expression. We implement the parameter by using a Z3 theorem prover (De Moura & Bjørner, ).

We present two exemplar formulas and their complexity from the AR-LSAT test set. The first example is as follows:

$$ $(\exists C:\textit{children})\,(\lnot(C\approx\textit{Juan})\land(\textit{ assigned}(C)\approx\textit{assigned}(\textit{Juan}))).$ $$

The formula is already in the CNF expression.
It contains two clauses; $\lnot(C\approx\textit{Juan})$ and $\textit{assigned}(C)\approx\textit{assigned}(\textit{Juan})$. The first clause has two distinct terms; $C$ and Juan, and one literal; $\lnot(C\approx\textit{Juan})$. The second clause has four distinct terms; $C$, Juan, $\textit{assigned}(C)$, and $\textit{assigned}(\textit{Juan})$, and one literal; $\textit{assigned}(C)\approx\textit{assigned}(\textit{Juan})$.
The measured complexity is $2+4+1=7$.

The second example is as follows:

$$ $(\textit{onSale}(\textit{newPop})\land\textit{onSale}(\textit{usedPop})) \rightarrow(\textit{onSale}(\textit{newSoul})\land\textit{onSale}(\textit{ usedSoul})).$ $$

The formula is first transformed into a CNF expression as follows:

$$ $(\textit{onSale}(\textit{newSoul})\lor\lnot\textit{onSale}(\textit{newPop}) \lor\lnot\textit{onSale}(\textit{usedPop}))\land$ $$

$$ $(\textit{onSale}(\textit{usedSoul})\lor\lnot\textit{onSale}(\textit{newPop}) \lor\lnot\textit{onSale}(\textit{usedPop})).$ $$

It contains two clauses. The first clause has three distinct terms; newSoul, newPop, and usedPop, and three literals; $\textit{onSale}(\textit{newSoul})$, $\lnot\textit{onSale}(\textit{newPop})$, and $\lnot\textit{onSale}(\textit{usedPop})$. The second clause has the same number of distinct terms and literals.
The measured complexity is $2+3+3=8$.

## Appendix C Component Accumulation Rules

We describe rules for component accumulation according to a logical dependency structure. It aims to add components on simple subsentences to compose more complex subsentences in a specific order that preserves the underlying first-order logic semantics. We note that the rules are deduced from the definition of logical dependency structure (Section 3.1). The followings are the rules for component accumulation:

- Rule 1.
Start with copying logic units.
- Rule 2.
If a logic dependent $D$ is the only dependent of a logic unit $U$, then integrate $D$ into $U$ and add the updated U.
- Rule 3.
If a logic dependent $D_{1}$ depends on another logic dependent $D_{2}$, then integrate $D_{1}$ into a logic unit $U$ that includes $D_{2}$ and add the updated $U$.
- Rule 4.
If more than one logic dependents $D_{1},D_{2},\cdots,D_{k}$ depend on a logic unit $U$, then add $k$ sentences that include $U$ and each logic dependent $D_{i}$ ($i=1,2,\cdots,k$). After that, integrate all logic dependents into $U$ and add the updated $U$.
- Rule 5.
If more than one components $X_{1},X_{2},\cdots,X_{k}$ depend on a logic coupler $C$, then integrate all components into $C$ and add the updated $C$.

We present three examples of component accumulation given sentences and their logical dependency structures in the following section.

## Appendix D Examples of Logical Dependency Parsing and Component Accumulation

We present three examples of logical dependency parsing and component accumulation. For component accumulation, the applied rules and corresponding logical dependencies are indicated for each accumulation step. (Integration) is additionally inserted for Rule 4 to maintain consistency.

Figure: Figure 5: Example of logical dependency parsing and component accumulation on AR-LSAT.

Figure: Figure 6: Another example of logical dependency parsing and component accumulation on AR-LSAT.

## Appendix E Dataset Statistics

In this section, we present dataset statistics of the logical reasoning tasks in Table 4.
We describe the details in the following paragraphs. If not mentioned, we use the entire test set provided by the dataset.

#### AR-LSAT-annotated.

We annotate a representative subset of AR-LSAT test set (Zhong et al., ) to measure first-order logic translation accuracy at a formula-level.
First, we sample the first problem from each set of problems that share the same context in the AR-LSAT test set.
Then, we preprocess the logical reasoning problem to generate a theory $\hat{\mathcal{T}}$ and a set of natural language sentences, following the steps in Section 2.
For each problem, we note that the sentences for constraints represent diverse first-order logic semantics while the sentences for five queries represent (nearly) the same first-order logic semantics. We therefore exclude other four queries and leave only the first one.
For each sentence, we carefully annotate $\hat{\mathcal{T}}$-satisfiable first-order logic formula and double-check its correctness. If a $\hat{\mathcal{T}}$ cannot express the context of the logical reasoning problem, we exclude the sentences in that problem.
As a result, we collect a total of 305 annotated formulas.

#### ZebraLogic.

The ZebraLogic test test (Bill Yuchen Lin, ) consists of 1,000 zebra puzzles where the puzzle size varies from $2\times 2$ to $6\times 6$. There are 25 different puzzle sizes, and each size has 40 samples. To evaluate the models on the most challenging puzzles, we use six hardest puzzle sizes ($4\times 6$, $5\times 5$, $5\times 6$, $6\times 4$, $6\times 5$, and $6\times 6$) for our test set, which yields a total of 240 puzzles.

#### Puzzle.

The entire dataset (Srivastava et al., ) consists of 1,000 samples. To split a test set, we sample the last 200 samples in the order of the samples listed in the dataset.

#### Symbol.

The entire dataset (Srivastava et al., ) includes 990 samples, which are categorized into five subsets (plain, adversarial, tricky, agnostic name-side, and agnostic emoji-side) with the same size. All examples in different subsets share the same logical meaning with each other where the only difference is the semantic link between the emojis and their names.
To focus on a first-order logic translation, we evaluate the models on the plain subset which includes 198 samples. The plain subset consists of three subgroups with the same size categorized by their difficulties. To construct a test set, we sample the second half of each subgroup in the order of the samples listed in the dataset, which yields a total of 99 samples.

#### Deduction.

The entire dataset (Srivastava et al., ) consists of 1,500 samples. We use the test set following Pan et al. () which consists of 300 samples.

#### ProofWriter.

We use the test set following Pan et al. (), which is a set of randomly sampled 600 examples from the most challenging depth-5 subset.

Table: Table 4: Number of few-shot examples, test examples, and options, and license of the logical reasoning tasks used in the paper.

## Appendix F Performance on Different Language Model Scales

Table 5 compares the performance of CLOVER and the neurosymbolic approach baselines on different languange model scales. If the symbolic solver cannot execute the solution, then we take random guesses.
The larger the language model scale, the higher the performance across all tasks and methods. We also discover that CLOVER with gpt-4o-mini on Symbol performs significantly better than Logic-LM with gpt-4o, which highlights the effectiveness of CLOVER.

Table: Table 5: Performance with language models of different scales using CLOVER and neurosymbolic approach baselines.

## Appendix G Impact of SAT-based First-Order Logic Verification

To further analyze an impact of using satisfiability in the verification algorithms, we compare those to two baselines: syntax consistency and LLM with instruction. First, we select the most frequent syntactically same formulas, which we call syntax consistency. Compared to logical consistency, logically equivalent but syntactically different formulas count as different formulas here. Second, we prompt LLM to select the most probable formula with reasoning, which we call LLM with instruction. LLM-based first-order logic verification is inspired by the previous works (Pan et al., ; Kirtania et al., ; Xu et al., ; Chen et al., ; Madaan et al., ; Ni et al., ).

We report the results in Table 6. The baselines show poor performance than the proposed SAT-based verification algorithms. Compared to a random selection, syntax consistency show 4.7% performance increment on AR-LSAT, but 0.8% marginal increment on ZebraLogic. LLM with instruction does not show any performance improvement on both tasks, which points out the limited capability of LLM to verify first-order logic formulas.
These results show that SAT-based first-order logic verification is the most appropriate algorithm that fully covers first-order logic semantics.

Table: Table 6: Comparison of different first-order logic verification approaches on AR-LSAT and ZebraLogic.

## Appendix H Few-shot Prompt Examples

Figure: Figure 7: Prompt used for logical dependency parsing on AR-LSAT.

Figure: Figure 8: Prompt used for component accumulation on AR-LSAT.

Figure: Figure 9: Prompt used for sequential translation on AR-LSAT.

Figure: Figure 10: Prompt used for disproving by counter-interpretation on AR-LSAT.

## Appendix I Extensive Error Analysis of Logic-LM

We present in-depth error analysis of Logic-LM (Pan et al., ) for first-order logic translation and the corresponding results of CLOVER on the AR-LSAT annotated subset. We follow Pan et al. () and Ye et al. () for the specification of declarations and formulas of first-order logic.
We colorize incorrect translations as red and describe the reason in the following.

Figure: Figure 11: Example #1 of error analysis of Logic-LM.

Figure: Figure 12: Example #2 of error analysis of Logic-LM.

Figure: Figure 13: Example #3 of error analysis of Logic-LM.

Figure: Figure 14: Example #4 of error analysis of Logic-LM.

Figure: Figure 15: Example #5 of error analysis of Logic-LM.

Figure: Figure 16: Example #6 of error analysis of Logic-LM.

Figure: Figure 17: Example #7 of error analysis of Logic-LM.

Figure: Figure 18: Example #8 of error analysis of Logic-LM.

Figure: Figure 19: Example #9 of error analysis of Logic-LM.

## Peer Reviews

confidence: 4
contribution: 2
initial_rating: 5
presentation: 2
questions: 1. Is it possible to extend CLOVER to improve performance on tasks that involve reasoning with data formats beyond natural language, such as mathematical equations or visual reasoning tasks?
2. Can the authors provide more insights into how CLOVER compares with CoT-based methods designed for improving implicit reasoning of LLMs?
3. Why not test CLOVER on a wider range of language models to assess its generalizability?
soundness: 3
strengths: - The paper presents a new approach by breaking down compositional translation into smaller steps and combining it with verification for logical reasoning tasks, leading to improved performance in neurosymbolic translation.
- The experimental results are robust using GPT4-o, showing improvements over other methods across multiple benchmarks.
- The authors propose two SAT-based first-order logic verification algorithms for selecting a sample from LLMs' logical code generations.
summary: The paper introduces CLOVER, an approach designed to enhance the translation of natural language logical problems into logical code, thereby improving the performance of language models on logical reasoning benchmarks. CLOVER achieves this by compositional translation of natural language into first-order logic and verification of logical semantics. The method involves parsing natural language sentences into logical dependency structures, translating these into first-order logic formulas, and employing verification algorithms to ensure accuracy. The authors demonstrate CLOVER's effectiveness on seven logical reasoning benchmarks, showing it outperforms previous neurosymbolic approaches.
weaknesses: - The approach is primarily applicable to problems that can be represented in a SAT solver, limiting its generalizability to other reasoning datasets, such as those involving mathematical equations or visual components, e.g., MATH dataset.
- The core idea of breaking down tasks into subtasks and using multiple samples and tests (e.g., verification, self-reflection, deterministic tests) to select the best generation is not novel.
- The paper lacks comparison with chain-of-thought (CoT) based methods designed to improve implicit reasoning of language models, as in "reliable reasoning beyond natural language". These methods help the model extract information that is implied but not directly stated by interleaving natural language comments with logical code, and can alleviate the translation bottlenecks identified.
- The paper only reports results using one language model, making it unclear if the method would improve performance across different models and weakening the experimental results.

---

confidence: 3
contribution: 2
initial_rating: 5
presentation: 1
questions: 1. 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?

2. Line 149: how to read this formula in natural language? 

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

4. How are "Declarations" created? 

5. How to decide a sentence not fit for your system? (or how to decide an unintended input sentence?)
soundness: 3
strengths: It is reasonable to improve the translation quality by decomposing a complex sentence into several shorter sentences. Using SAT solvers certainly improve the quality.
summary: Authors propose a novel method of using LLMs to translate natural language descriptions into a set of first-order logical forms. This novel method decomposes this challenging task into two steps. 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. Experiments on seven benchmark datasets greatly outperform current SOTA level.
weaknesses: Not all natural language sentences can be translated to first-order logic forms. Authors did not discuss what sentences cannot be translated. 

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

Theoretically, the meaning of natural language is not logical formula. This work is valued within fixed benchmark datasets. 
 
The formalism of the paper is not easy to read.

---

confidence: 4
contribution: 3
initial_rating: 5
presentation: 2
questions: - I'm curious why the execution rate increases when using CLOVER.  As I read the methods section, it looked like CLOVER primarily helps with execution accuracy, but I didn't see much about how it would help repair/fix/generate better code for the SAT solver.  

- It's reported that "CLOVER’s errors are primarily caused by preprocessing and other errors, which takes 78.6% of the total errors", do you have examples of this? Is this an error in the accumulation stage?  I think the paper does a great job of explaining where Logic-LM fails and why CLOVER is needed, but I think expanding on CLOVER errors is just as important to show where researchers can look next.

- How much of the performance gain seen in CLOVER is due to a higher execution rate (runnable code)? I think expanding on how the metrics in Table 2 are computed would be helpful. For example is `Execution Acc = (correct_and_executable_programs / all)` or `Execution Acc = (correct_and_executable_programs / executable_programs)`.  The latter, I think, helps distinguish if you are generating better executable problems or if you are only improving the execution rate (which maybe there is a simple fix to Logic-LM to help it create better executable problems)?
soundness: 2
strengths: - The results are promising; the authors do a fantastic job of motivating their new algorithm CLOVER by showing common failures of previous methods like Logic-LM, then show that their method fixes many of these errors (leading to the performance boost reported in Table 1).

- The method here is pretty novel. Breaking down sentences into atoms isn't too novel, but I haven't seen someone decode them all individually and progressively (tapping into the auto-regressive natural of LMs) to improve the performance of the translation.  The verification algorithms seem pretty intuitive (although they are described complexly), but again, despite being intuitive, I think they are fairly novel as well.
summary: Introduces a new algorithm, CLOVER, for solving logic questions in natural language, specifically by addressing the challenges in parsing natural language into the correct first-order logic so that an SAT solver can determine the answer.  To do this, the paper proposes translating the question into smaller pieces that accumulate based on how each logic unit in natural language relates to other logic units until the resulting sentence is the final sentence that needs to be tested.  Each accumulation from the previous step, including the final sentence, is translated into first-order logic, then the paper introduces two novel verification methods that check if the translations are valid and if there are contradictions in the final translation. The paper shows that with this accumulation strategy with their two verifiers, their method can outperform all baselines (including Logic-LM, a baseline that similarly translates sentences into FOL for SAT solvers) on common logic datasets like AR-LSAT, FOLIO, and ProofWriter.
weaknesses: - The ablations in Table 3 need to be explained more clearly and then discussed.  What is "Is Clover?" and why is the simplest ablation (no clover, direct translation, no verification / essentially none of the new things introduced in this paper) outperforming Logic-LM on AR-LSAT by 10.9% already from Table 1? Does this mean that your direct translation prompt already improves over complex algorithms like Logic-LM? If so, this deflates the papers impact, so it should be addressed (it's possible I am missing something, but others will catch this too, so it's best to explain it away.)

- I believe the paper would benefit greatly from expanding on the models being evaluated; right now, only GPT-4o and GPT-4o-mini are evaluated.  Showing that CLOVER consistently outperforms the baseline methods across model classes would improve the impact of this work.

- (minor point) There is no discussion of inference-time compute costs for CLOVER vs. the other baselines.  I imagine the inference cost is significantly higher, but I am unsure how much.  Is this negligible compared to Logic-LM?  Is there a way to compare CLOVER with baselines that use the equivalent amount of compute during inference?  I think much of this point could be explained away with a textual justification (i.e., this isn't possible, or the compute costs are nearly equivalent, etc.), but I do think it should be mentioned.

- (minor point) Clarity in section 3 could be improved. I would use the example in Figure 2 to clearly define each variable mentioned in the text to help readers follow your algorithm.  For instance, defining with x^prep, T, phi_k, the mapping NL(phi), etc., with values from Figure 2 would help readers follow significantly. This could also be done in Figure 2 if you mark which parts of it are which variables.  The text gets very dense with variables that are derived from other variables quickly; having these concrete instantiations really helps.

Meta-review: The reviewers generally saw the merits of the proposal. There was general interest in the paper. The authors have responded to several issues raised by the reviewers.  On reading the paper at a fairly high-level, it does appear interesting and novel. The authors in the rebuttal have clarified some of the issues raised by the reviewers. I hope these clarifications will be directly incorporated in the final version of the paper. I suggest borderline acceptance.

Decision: Accept (Poster)