Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning
Authors: Hyun Ryu
Gyeongman Kim
Hyemin S. Lee
Eunho Yang
Venue: ICLR 2025 Poster (2025)
Keywords: Logical Reasoning
Large Language Models
Neurosymbolic Approaches
Semantic Decomposition
Formal Language Verification
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We introduce CLOVER, a neurosymbolic approach that enhances complex logical reasoning in large language models by compositional translation of natural language into first-order logic and verification of logical semantics.

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 Compositional First-Order Logic 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 Verification 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.

Published as a conference paper at ICLR 2025
DIVIDE AND TRANSLATE: COMPOSITIONAL FIRST- ORDER LOGIC TRANSLATION AND VERIFICATION FOR COMPLEX LOGICAL REASONING
Hyun Ryu' Gyeongman Kim
Hyemin Lee"
Eunho Yang!
KAIST MIT
syyuhyun1905, gmkim, eunhoy)@kaiist.o. ac. hmstella@mit.edd
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 natural language problem into a satisfiabil- ity (SAT) problem that consists of first-order logic formulas, and sound symbolic solver returns a mathematically correct solution. However, we discover that LLMSs have difficulties to capture complex logical semantics hidden in the natural lan- guage during translation. To resolve this limitation, we propose a Compositional First-Order Logic Translation. An LLM first parses natural language sentence into newly defined logical dependency structures that consist of an atomic sub- sentence and its dependents, then sequentially translate the parsed subsentences. Since multiple logical dependency structures and sequential translations are pos- sible for a single sentence, also introduce two Verification algorithms ensure more reliable results. We utilize an SAT solver to rigorously compare semantics 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- ofte-oofthheart results
INTRODUCTION
Logical reasoning involves reaching conclusions through structured process. It entails drawing inferences by converting information provided in a set of premises into a final conclusion (Nunes)
2012 Bronkhorst et al.) 2020). Logical reasoning ability is one of the most challenging metrics to
measure intelligence. As a model size grows exponentially, large language models (LLMs) (Brown
al. 2020 Chen et al. 2021 Thoppilan al. 2022) unlock the ability of machine to reason.
tffin-of-thought (CoT) prompting (Wei et al. 2022) significantly improve the performance of
L.MSs 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,,
2024 Pan et al., (023). To resolve this issue, several neurosymbolic approaches (Ye al., 2024 Pan et al. 2023 Kirtania et al. 2024 Olausson et al.) (023)) utilize an LLM with symbolic solver (c.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 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.
However, we have discovered that LLMs still cannot translate sentences that represent complex first-order logic. Our experimental evidence in Fig. presents the drastic performance drop of the previous work (Pan et al. 2023) on complex first-order logic translation The result indicates that an
'The source code used the paper is available at intps:t:////... / hwwp:/wwww.ooo//oooooooooo con Ryuu olevr TTo evaluate the complexity and performance of each first-order logic formula, we sample the first problem from each set of problems that share the context in the AR-I.SAT and manually annotate the

---

Published as a conference paper at ICLR 2025
(a)
(b)
The Sales division is toured consecutive days, and other days.
Logic-LM CLOVER
Diroctly translate
100
Logic-LM
Translation accuracy (56)
90
(3d : days))toureddd)) Sales A tourre + 1) Sales)
(Vi (tuure(()))) Sales Ae 1) Sales) (foured Sules))
1. Divide
CLOVER
1) The Sales division is toured.
50
2) The Sales division is loured on two consecutive days.
3) The Sales division is toured on two consecutive days, and on no other days.
40
30
Translate
8
12
16
20
(3dl (tss))to))))((()) Sules)
First-Order Logic Complexity
2) (3d (ays))towred(())
(dwored 1)= Sales)
3) (3d (oorrdd))))) - Sales A tnaraddd 1) Sales A (Vx daps)((r + A
d' 1) - (loured(s) Sales)))
Figure I: Comparison of a first-order logic translation of the proposed CLOVER and Logic-LM with gpt-4o AR-LSAT. (a) Translation accuracy at different levels of first-order logic complexity. We group the formulas in one of five complexity ranges and report the averaged performance for each range. (b) A representative example. Given declarations of sorts and functions, each method translates the natural language sentence into the corresponding first-order logic formula. We colorize incorrect translation as red for visualization purpose.
LLM performs first-order logic translation faithfully to a certain degree of complexity but falls short beyond that limit. A representative example in Fig. Th presents an incorrect output of the previous work (Pan et al. 2023) 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 corresponding first-order logic formula given declarations. An LLM correctly translates natural language clause "The Sales division is toured on two consecutive days." " into a subformula (3d days) (toured(d) Sales) A (toured(d+1)
other Sales) which contains simple logic, but fails to translate "and days" which represents more complex logic. Specifically, the incorrectly translated subformula is always true, which has semantic meaning. After further extensive qualitative error analysis (Appendix K). 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, take hint from how humans perceive 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.) 1970 Frazier & Fodor) 1978 Sweller [988]. 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 subsen- tences by accumulating sentence components. This could help LLM to preserve first-order logic semantics during translation. To rigorously define the atomic subsentence and sentence compo- nents with logical meaning, we introduce a new parsing method for natural language that represents first-order logic, called logical dependency parsing (Section 3.T.
Based on logical dependency parsing, we propose a compositional first-order logic translation (Sec- tion (.2) (.2) by few-shot learning with an LLM. It consists of the following three steps: logical depen- dency 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 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 transla-
ground truth formulas. Detailed information of measuring complexity is in Appendix B and the process of the annotated subset construction descrihed in Appendix
2

---

Published as a conference paper at ICLR 2025
We propose two verification algorithms: logical consistency and disproving by counter- intuter-iteerreetttion 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 equiv- alent formulas. However, we observe that an I.LM sometimes make logically consistent translation errors. To overcome such limitation, we devise disproving by teeeeinneeeeeeeeeeeeee innnttrrinteppettttion It sequen- tially compares two formulas and disprove one of them by determining if counter- cuunttr-interprcaation 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.
tion (Section 3.3
We evaluate the proposed CLOVER, Compositional First-Order Logic Translation and Verification, seven logical reasoning benchmarks (Section 4. CLOVER outperforms the pre- vious neurosymbolic approaches and achieves the new state-of-the-art performance. It also signif- icantly enhances the first-order logic translation accuracy across all levels of complexity and the largest performance gain oceurs the highest first-order logic complexity (Fig. Ta
To summarize our contributions,
1. We introduce CLOVER, novel neurosymbolic approach that enhances complex logical rea- soning 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 preserv- ing underlying first-order logic semantics.
3. We also propose two SAT-based first-order logic verification algorithms that can faithfully se- lect a correctly translated formula.
4. We evaluate CLOVER on seven logical reasoning benchmarks and show that CLOVER out- performs the previous neurosymbolic apporoaches and achieves the new state-of-the-art per- formance.
2 PROBLEM FORMULATION
Through the lens of (many-sorted) first-order logic] logical reasoning problem x is natural language description a E-theory T constraints o, and a query g. denoted as x = NL(T, 4, 4) A E-theory T is non-empty set of any E-structure where signature Σ (S, F, consists of sorts S. function symbols F, and predicate symbols P. Hereinafter, we denote the vocabulary of first-order logic italic for clarity, and omit the prefix "Σ)"" for simplicity. A structure of theory indicates the semantics of formulas. Constraints & are a set of formulas that are true, denoted as A query q is also a formula which yet determined as true, false, or unknown given the constraints 4.
{Ø1, .2.... ΦK}.
Prior works. Prior neurosymbolic approaches (Ye et al. 2024; Pan et al. 2023 Kirtania et al. 2024 Olausson et al.) 2023) directly translate the logical reasoning problem x into a set of first- order logic using an L.LM and then employ symbolic solver (e.g., g., an SAT solver) to solve an SAT problem. In these methods, an LLM performs single inference for the first-order logic translation as follows:
T. T' NL((()))) K+1 (L (y NI(()))) K+1 xx))))
where Pk = OR for 1 < k < and ΦK+1 = q, and a few-shot exemplar set X (zo(), T(,, (xt) ( K more than one formulas for single target sentence or generates a formula which is translation of combination of a target sentence and part of other sentences. Though it might be logically correct as whole, we cannot further analyze and verify the translation at sentence-level.
with the size of the set N. However, often generates
First-order logic translation. To resolve this drawback, we perform first-order logic translation for each sentence. Since sentence-level translations require pre-defined theory and target sen- tences, we first generate theory T and set of natural language sentences [N KK+
K+1 from
3 Monny- first-order logic is one of the variants of the standard first-order logic that allows variables have different domains, which is called sorts S. We provide related preliminaries in Appendix A
A theory assigns specific meanings to symbols of formulas. For simplicity, we presume that theory T incorporates the commonly applied theories (e.g., theory of equality, arithmetic, etc.).
3

---

Published as a conference paper at ICLR 2025
I, and then generate --satisfiable formula Gb for each sentence NI((p)). To be specific, the sin- gle inference by the LLM in Eq. | separated into the following two steps: 1) given a logical
reasoning problem and few-shot exemplar set x -h {-(() T(,, () Kー - M==1 the LLM generates a tuple of an estimated theory and a set of natural language sentences, denoted
-re = (T, {NL(p))) K+1), 2) given the theory T and set of few-shot exemplar sets Xs.- the proposed CLOVER translates each natural language sentence [L((p)) into the estimated formula fk that is -sstisffiale as follows:
t, (NL())))) K+1 (L (NI(P+)) ProP)
Pk CLOVER(T, NNARRRT,,N(AAA ((F)), E (1. 1}.
parse secumn trans dispr)) and detailed description of the set of few-shot exemplar sets X = ( the proposed CLOVER for gPeP = (T, (NL())) will be discussed in the following section.
X xB X
SAT problem solving. Once estimations of the theory T, constraints 4 = {1²1, P2, Px J. and a query i = K- are completed for the logical reasoning problem æ, these form an SAT problem P = (T, 6 f) An automated SAT solver then determines the 7 -satisffabilit the query under the constraints C which is a final prediction of an answer of the logical reasoning problem z. We use Z3 theorem prover (De Moura & Bjørner 2008) as an SAT solver in the implementation.
CLOVER
In this section, we propose CLOVER, Compositional First-Order Logic Translation and Verification for complex logical reasoning. To fully capture first-order logic semantics in natural language, it first parses single natural language sentence into logical dependency structures. Then, sequentially translates parsed subsentences with an LLM. Since there are multiple ways to parse and translate the sentences, 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 A of sentence NL((p) under the theory T where yp is T-satisfiable is defined by components and their logical dependencies. First, components are natural language building blocks of logical dependency structures of sentence, which consist of logic units U, logic couplers C, and logic dependents D. The following definitions formally describe each of them.
Definition (Logic units). Given sentence N L(p)) and theory T where yp is T-satisfiable, logic units U are the natural language descriptions of an atom of sp 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 (Logic dependents). Logic dependents are components neither logic units nor logic couplers which logically depend another component.
Second, we define logical dependency between two components, and the following definition for- mally describes it.
Definition (Logical dependency). The component X is said logically depend on the component Y in the given sentence 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 logical dependency structure stemmed from its definition. Remark given sentence and theory can have multiple logical dependency structures. Remark All components except for one should logically depend on another component. Remark No logic dependent logically depends on logic coupler.
We present examples of logical dependency structures in Fig. 2 and Appendix D
Foor AR-LSAT, we need to check the -validiit depending the problem. More details in Appendix
4

---

Published as a conference paper at ICLR 2025
a Target Sentence (M2()))
Declarations (7)
INPUT
Hanadi cannot be appointed to the same court Perkins
candidates (Hamadi, Kurtz, Li, Ortiz, Perkins)
(appellate, trial] appointed [unccionncandidttees courts)
6
Compositional First-Order Logic Translation
1. Logical Dependency Parsing
2. Component Accumulation (R; 4)
1) "larmadi is appointed to court"
Strueture #1 (4+
Components:
"Perknns appointed court"
Ug
"Hamadi appointed to court",
3) "[armadi cammot appointed lo court"
"Hamaadi cannot appointed the court Perkins"
"Perkins appoiinted
0g "cannot". G "the same as"
3. Sequential Translation
Logical dependeney:
D2 U1
1) &
coarts) (opptts)eeponntee c)
2) L
[3c courts) (eparts))ppppoon (appottte =
formalx #1 (+v
944 Ve courts) (aapoottced
(appotnted(Perkins) =
Set
(We ( (ompointeed(Perrinng e) courte((appotuuaa[(Maeee))
formulas
(fppkintce o) @ courtssaapoontee(Peeknng
(P)
(Ve rourts) (oppoootoopptttneeeeeennn (appainsed(Hamad)) + e) # oppointed((Hamadi)) * uppointel(Perkinn))
First-Order Logic Verification
Logical Consistency
Group logically formiun using SAT solver
(We (urtts((cmpponncc(/ommm))) = c) (uppointed((erkkins)) c))
Pp
(33 sourct)((uppccttee((faaad) c) (uppointed(Perkinn)
P4
courte]aarponneee((cmmoo))
courto((eppinned((eekn (uppolntee((ammad) c))
(Haolated(Hammad)) oppolated((errvine)
Disproving Counteriinerpretation
Find counter-interppetaaiinn using
Judge or satisfy the target sentence using LLM
P
"Havadi appointed Perkcins
9y disproved
(appointea(Hamadd)) trial.
Py selected
1:55 (T-unsottefubble)
appointed((eerkits)) trial
(Ø' 9p))
OUTPUT
(Ve courts[(apponnte((Hmmdd c) (appolnted((errkins) +
Figure 2: Overview of CLOVER, Given declarations theory, CLOVER parses a target sentence to several possible logical dependency structures, accumulates components according to logical de- pendencies, and sequentially translates subsentences first-order logic formulas. Then, CLOVER verifies set of estimated formulas. Logical consistency selects the most frequent logically equiv- alent formulas. Disproving by counter-interpretation sequentially compares two formulas and dis- prove one by determining if coumter-interpretation satisfies the target sentence.
3.2 COMPOSITIONAL ORDER LOGIC TRANSLATION
To compositionally translate natural language sentences first-order logic formulas under given theory for "re = (T, ((+ we adhere to the following three steps by few-shot learning with an LLM. We describe the following steps for single target sentence LL((p) of formula 40 K+1 k+
Logical Dependency Parsing. In the first step, target sentence is parsed into different possi- ble logical dependency structures. An LLM is given definition logical dependency struc- tures (Section 3.1 a target sentence NL((p) and its theory t. and few-shot exemplar set parse (T() NL(())) 10) for logical dependency parsing. 7,00 size of

---

Published as a conference paper at ICLR 2025
of different possible logical dependency structures of sentence [((()() under the theory T(,, and N a size of the few-shot exemplar set. Then, LLM generates set of different possible logical dependency structures (A:]/= of the target sentence with the size of the set L as follows:
ł, (A.) ~ (L, (AH N.(p) X
perse)
Component Accumulation. In the second step, components of a logical dependency structure accumulated gradually compose new sentences until those reach the target sentence. We present the rules for component accumulation in Appendix [ An LLM is given a definition of logical dependency structures (Section 3.I). rules for component accumulation (Appendix C target sentence (yp) and one of its logical dependency structures Ai where I {1, L. and a few-shot exemplar set X = {N L(p(()), A (Sm) MM N mm=1fim1 for component accumulation. mmml sequence of accumulated sentences where M the length of the sequence. Then,
(s M
LLM generates sequence of sentences ($1.m) where M, is the length of the estimated sequence as follows:
Mi, (St, (M (m).)) NT(()) A.. X
2acum) vA E (1,2, f.}.
(4)
The last sentence of accumulation $ . is the target sentence L(p))). We present examples of component accumulation in Appendix
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 (m= of a target sentence where E {1,2,-.. .D),
theory T. and few-shot exemplar set x {T((), (1()) 1869 (0) M
(0MM) N mm= Jm= 1J==1 for first-order
logic translation. Then, LLM generates sequence of formulas (fr.m m
m=1 as follows:
(g). mm= )
Mr
P Mi I,, (St.m ) X
Irans AI f1,2,.... .L}.
(5)
The last formula of the sequence is the first-order logic translation of the target sentence (i.e., 9 = ). For VI E 2,, ... î.), we could generate set of estimated formulas v { for target sentence Lyp) 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 set of compositionally translated first-order logic formulas V, introduce the following two algorithms using SAT solver (and few-shot learning with an LLM). As in Section 3.2 we describe the following algorithms for single target sentence N L(p)) under the theory 7 (i.e., The algorithms select a verified formula yp in a set of estimated formulas V). Prior to describing the detailed algorithms, we filter out the formulas that are syntactically incorrect or 7 -unsatiisfable in using an SAT solver and call the processed set V
Logical Consistency. We select the most frequent logically equivalent formulas, which call this algorithm logical consistency. It presumes an LLM utilizes different logical dependency struc- tures 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 (pp, (pp: such that Pp E Mman 44 E V.a. and + 9. an SAT solver determines their ी -eqquivalence. Then, we group T -eqquivalent formulas and select any formula in the group that has the largest number of elements. However, we observe that an L.MM sometimes makes consistent mistakes in the last step of compo- sitional first-order logic translation, which leads to logically equivalent incorrect formulas.
Disproving by Counter-Interpretation. To resolve this issue, we introduce an advanced algo- rithm that sequentially disproves incorrect formulas by coumter-ineerpreattin.. Following this al-

---

Published as a conference paper at ICLR 2025
Algorithm First-Order Logic Verification (Disproving by Counter-Inierpretttin
Input: Theory T, natural language sentence N ((p) of first-order logic formula y, and set of estimated Tssatisfiable formulas sat
Output: Verified formula "p"
P0 L sat
Select an element Go in randomly Initialize x² to a random element yp
80" - 50
for each ip V sat \ {fo) do
Ptemp t 40
Use temporary variable Premp for the update
for each (pps Pq)) {(p0, , }), (²)))) do
if (9p Apy) is T -ssaiisfialle then find T-interpretation such that I (4p A 7lpg) dispre) è ~ PL [L( I, 1, ) 6. (T, if (ipp 40" - or (1pp 4 ê) then
SAT solver finds if exists b LLM determines if I
Promp f g
end if
end if
end for o- - Premp
> Update D² after checking Tiinterpretations from both side
end for return "0"
gorithm, an accurate formula remains the last if it exists in s Specifically, we select a ran- dom element Po in sar and initialize the verified formula sp" to Go. For each estimated for- mula & in Van {Go)) an SAT solver determines if (sp" A -Gp) is --satisfiable. First, if it is T- satisfiable, an SAT solver finds coumter-interppetatiin I to T-equivalence of ypt and & that satisfies (f* A -x).. Given target sentence NL)(p), counter-interpretatiinn
and few-shot ex- (0) (()),e())))) J Ji=1 for disproving, an LLM decides if satisfies y. which returns a boolean value é. If is True. then & is disproved since I does not satisfy & but satisfies yp é False, then xp disproved since 1 satisfies yp but does not satisfy sp Second, if (sp" A -x) is I T-unsatisfiable, it is equivalent to (4p" - ()) is -satiisfiable, and no I exists. After repeating this consider cuunter-interpretation I that satisfies (6 -
emplar set X
disprv [NL(())
decision process for (48 A -,p"), and disproves accordingly. We select the verified formula 4- that remains the last. Algorithm summarizes the whole process.
EXPERIMENTS
4.1
SETUP
Tasks. We evaluate CLOVER on seven logical reasoning tasks: AR-LSAT (Zhog et al. 2022). ZebraLogic (Lin et al. 2025). Logic grid puzzle (Puzzle), Symbol interpretation (Symbol), and Log- ical deduction (Deduction) from the BigBench collaborative benchmark (Srivastava et al. 2022), FOLIO Han al. 2022). and ProofWriter (Tafjord al. 2021). AR-LSAT consists of analytical reasoning problems of the law school admission test, and Zebraloogie is a benchmark for zebra puz- zles. Puzzle, Symbol, and Deduction FOLIC is an expert-written first-order logic reasoning task, and ProofWriter is a deductive reason- ing benchmark. Note that all tasks except ZebraLogic are multiple choice problems, and Appendix describes details of each task.
tasks from logical reasoning category in the BigBench.
Language Models. We perform our experiments mainly gpt-4o (Achiam et al. 2023 current taate-of-the-art L.L. for complex, multi-step tasks, unless stated. We also evaluate CLOVERR
We use revised version of FOLIO that improves sample quality and fixes emors, which is released on: https::/huggingffae /tt.e/aattttttttalllll....ee.e.e p/FO..0

---

Published as a conference paper at ICLR 2025
Table I: Performance on logical reasoning tasks using CLOVER and the baseline methods.
AR-LSAT
ZobraLoggic
Puzzle
Symbol
Deduction
FOLIO
ProofWriter
Standard
30.3
0.4
63.0
74.7
84.7
70.9
53.7
CoT
36.8
0,4
51.0
80.8
94.0
73.9
78,0
SymbCoT
34.2
0.8
66.5
55.6
90.7
76.9
80.2
Logic-LM
42.4
45.4
64.0
81.8
95.3
75.4
95.3
CLOVER
62.8
75.4
83.5
89.9
99.3
78.8
96.7
Table 2: Comparison of program accuracy, execution rate, and execution accuracy of CLOVER and Logic-LM.
Program Acc CLOVER
Execution Rate
Execution Acc
Logic-LMt
Logic-LM
CLOVER
Logic-LM
CLOVER
AR-LSAT
46.8
33.8
59.7
51.3
78.3
Puzzle
60.0
79.0
79.5
80.0
75.5
98.8
Symbol
49.5
76.8
52.5
82.8
94.2
92.7
Deduction
92.7
99.0
97.3
99.7
95.2
99.3
FOLIO
51.2
62.6
65.5
74,9
78.2
83.6
ProofWrtier
94.2
96.5
96.8
99.2
97.2
97.3
and the baselines using smaller model, gpt-4o-mini (Achiam et al. experiments, we set the temperature and select the highest probability response from the model.
2023
To reproduce
Baselines. We compare CLOVER primarily to Logic-LM (Pan et al. (023). state-of-the-ar neu- rosymbolic approach for logical reasoning. There are few more works (Ye al. 2024 Olausson et al. 2023) nearly the same to Logic-LM, but we focus on Logic-LM since their difference is marginal. We also compare CLOVER another neurosymbolic approach (Xu et al.) 2024) which uses an LLM to solve SAT problems instead of using symbolic solver. In addition, we compare to the standard prompting and CoT prompting that leverages in-context learning capability of the base I.MMs. For fair comparison, we manually sample or derive our few-shot exemplar sets from those in the previous works (Pan et al. 2023 Xu et al. 2024 if is possible. Since the previous works do not evaluate their models on ZebraLogic. Puzzle, and Symbol, randomly select single exemplar problem outside the test set. We demonstrate exemplar few-shot prompts in Appendix
Evaluation metrics. We measure the performance of CLOVER and the baselines primarily by the correctness of logical reasoning problems. For neurosymbolic approaches with symbolic solver, the solver cannot execute the translated SAT problem, we fall back to CoT predictions. From this unique property, following Pan al. (003), 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 por- tion of executable problems, and execution accuracy indicates the accuracy for executable problems.
RESULTS
We present the performance CLOVER and the baselines on different tasks, different evaluation metrics, and different language model scales. First, Table 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 Logic- LM on AR-LSAT by 20.4% and ZebraLogic by 30.0%. Overall, neurosymbolic approaches with symbolie solver (CLOVER and Logic-LM) show remarkable improvement on these hard reasoning tasks. The inference time costs of CLOVER and the baselines reported in Appendix H
"To specify language model versions provided by OpenAL, use gpt-4g-204 -5-15 and got-4o-min -2024-07--000
experiments.
8

---

Published as a conference paper at ICLR 2025
Table 3: Ablation of CLOVER on AR-LSAT and ZebraLogic. The first three rows are ablations of CLOVER, and the last two rows correspond to CLOVER.
Is CLOVER?
Translation
Verification
AR-LSAT
ZebraLogic
direct direct (5x)
X
53.3
45,4
logical consistency
54.6
59,6
compositional
x
55.0
70.0
V
compositional compositional
logical consistency
61.9
74.2
disproving
62.8
75.4
Second, Table 2 presents three additional evaluations for the neurosymbolic approaches with a sym- bolic solver. CLOVER shows higher execution rate 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 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 rea- soning tasks. Specifically, CLOVER increases the execution rate of Logic-LM on AR-LSAT by 25. 25.9% and the execution accuracy by 27.0%, which finally leads more than doubled program ac- curacy of Logic-LM. Lastly, we compare the performance of CLOVER and the baselines on different languange models in Appendix
4.3 ABLATIONS
We conduct ablation studies of CLOVER two perspectives: compositional translation and veri- fication, in Table 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, respec- tively. 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 slightly larger than the average number of estimated formulas of CLOVER. Ablating both compositional translation and verification from CLOVER shows further performance loss. Additionally, disprov- ing by counter-interpretatin 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 Since SAT solver is sound and does not cause any error, 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 eтrors caused by an incorrect selection of a satisfiability function and limited ex- pressiveness of Z3 theorem prover. In contrast, we highlight that CLOVER has nearly no logic or syntax error. CLOVER's '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 rea- soning and compare the results with CoT-based reasoning L.MMs (Jaech et al. 2024 in Figure 4 We also add the results of Logic-LM to measure the effect of neurosymbolic approach on reasoning length. We observe noticeable performance drop of Co'--baeed reasoning LLMs on long sequence of reasoning, which is a frequently pointed-out drawback 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.
We use CoT-based reasoning L.MSs that were recently released from OpenAI, specifically o1-previeww 2w02 00004-09-111 12 and c cl-ming mi -
22024-094 -- for analysis.

---

Published as a conference paper at ICLR 2025
Logic-LM
CLOVER
- -ol--previww - o1-mini Logic-LM CLOVER
100
Occurences
Accuracy (%)
75
50
25
logic error
syntax
prep
others
error
error
I of features
Occurences of different enror types of CLOVER and Logic-LM on AR- LSAT annotated subset.
Figure 3:
Performance different reasoning lengths using CoT-based reasoning LLMs and neu- rosymbolic approaches on ZebraLogic. Each exam- ple is puzzle of five houses with varying # of fea- tures.
Figure 4:
RELATED WORKS
-ased neurosymbolic approach for reasoning. Previous works (Ye et al. 2024 Pan al.
Olausson al. 2023 Kirtania et al. 2024) utilize LLM as semantic parser which trans- lates 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. 2024 that utilizes an L.M 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 common drawback that LLM cannot faithfully perform complex first-order logic translation, which fundamentally limits the performance of neurosymbolic approaches on complex logical reasoning tasks.
2023
LLM-based problem decomposition. To solve natural language tasks, previous works explore decomposing complex problems into several simpler ones using I.LMs. [rroddvv al, (2022) 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 al. (2022 is not applicable to complex logical reasoning tasks. Other works (Zhou et al.) 2023 Khot et al. 2023 Press et al., 2023 Dua
al. 2022 Ye al., 2023) focus decomposing simple question-answeriin problems by prompt- ing LLMs with few-shot examples. However, if LLMs simply rely on few-shot examples for decom- posing 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 lan- guage generated by LLMs. Chen et al. (2024) and Madaan et al. (2224) first generate code from natural language, get feedback from an LLM, and refine the code based on the feedback. Chen et al. (024) additionally utilizes external feedback signal from executor. Ni al. (2023) first gen- crates candidate codes from natural language and then verify by predicting their correctness using trained neural network. However, these model-based verifications show limited performance complex logical reasoning tasks (Appendix[],
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 us- ing satisfiability to fully cover first-order logic semantics. Empirical results show that CLOVER achieves state-of-the the--rr-tt performance on seven logical reasoning benchmarks.
10

---

Published as a conference paper at ICLR 2025
7 ACKNOWLEDGMENTS
This work was partly supported by Institute for Information & communications Technology Pro- mIT)) RRS-2019-11190075 Artificial Intelligence Graduate School Program(KAISTT, No.2022-0-00777 Meta-learning applicable to real-world problems, No.RS-2024-00455888 Al Re- search Hub Project) and National Research Foundation of Korea (NRF) (No.R3 RS-2023- 00209060, A Study on Optimization and Network Interpretation Method for Large-Scale Machine Learning) grant funded by the Korea government (MSIT).
REFERENCES
Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, lige Akkaya, Florencia Leoni Ale- man, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
Marta Arias and Roni Khardon. Complexity parameters for first-order classes. In Inductive Logic Programming: 13th International Conference, ILP 2003, Szeged, Hungary, September 29-
October 1, 2003. Proceedings 13, pp. 22-37. Springer, 2003.
Hugo Bronkhorst, Gerrit Roorda, Cor Suhre, and Martin Goedhart. Logical reasoning in formal and everyday reasoning tasks. International Journal Science and Mathematics Education, 18: 1673-1694, 2020.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. Advances in neural information processing systems, 33:1877-1901, 2020.
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained code. arXiv preprint arXiv:2107.03374, 2021.
Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. Teaching large language models to self-debug. In The Twelfth International Conference on Learning Representations, 2024.
Leonardo De Moura and Nikolaj Bjømer. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340. Springer, 2008
Andrew Drozdov, Nathanael Schärli, Ekin Akyürek, Nathan Scales, Xinying Song, Xinyun Chen, Olivier Bousquet, and Denny Zhou, Compositional semantic parsing with large language models. In The Eleventh International Conference on Learning Representations, 2022.
Dheeru Dua, Shivanshu Gupta, Sameer Singh, and Matt Gardner. Successive prompting for de- composing complex questions. In Proceedings the 2022 Conference on Empirical Methods in Natural Language Processing, pp. 1251-1265, 2022.
Lyn Frazier and Janet Dean Fodor. The sausage machine: new two-stage parsing model. Cogni- tion, 6(4):291-325 1978.
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 XxXv:2209.008400, 2022.
Aaron Jaech, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Aleksander Madry, Alex Beutel, Alex Carney, et al. Openai ol system card. arXiv preprint arXiv:2412. 16720, 2024.
Dejan Jovanovié and Clark Barrett. Sharing is caring: Combination of theories. In Frontiers of Combining Systems: Sth International Symposium, FroCoS 2011, Saarbrücken, Germany, Octo- ber 5-7, 1. Proceedings 8, pp. 195-210. Springer, 2011.

---

Published as a conference paper at ICLR 2025
Tushar Khot, Harsh Trivedi, Matthew Finlayson. Yao Fu, Kyle Richardson, Peter Clark, and Ashish Sabharwal. Decomposed prompting: A modular approach for solving complex tasks. In The Eleventh International Conference Learning Representations, 2023.
Shashank Kirtania, Priyanshu Gupta, and Arjun Radhakirshna. Logic-Im++ Im++: Multi-step refinement for symbolic formulations. arXiv preprint wrXiv:2407.025144 2024.
Bill Yuchen Lin, Ronan Le Bras, Kyle Richardson, Ashish Sabharwal, Radha Poovendran, Peter Clark, and Yejin Choi. Zebralogic: On the scaling limits of Ilms for logical reasoning. arXiv preprint arXiv:2502.01 100, 2025.
Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, et al. Self-refine: Iterative refinement with self-feedhack. Advances in Neural Information Processing Systems, 36, 2024.
Richard Montague et al. Universal grammar. 1974, pp. 222-46, 1970.
Ansong Ni, Srini Iyer, Dragomir Radev, Veselin Stoyanov, Wen-tau Yih, Sida Wang, and Xi Victoria Lin. Lever: Learning to verify annuage-tt-cood generation with execution. In International Conference on Machine Learning, pp. 26 26106-26128. PMLR, 2023.
Terezinha Nunes. Logical reasoning and learning. Encyclopedia of the sciences of learning, pp- 2066-2069, 2012.
Theo X Olausson, Alex Gu, Benjamin Lipkin, Cedegao E. Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. Line: A neurosymbolic approach for logical reasoning by combin- ing language models with first-order logic provers. arXiv preprint arXiv:2310.15164 2023.
Liangming 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:2305. 12.005/.2229.. /2295, 2023.
Ofir Press, Muru Zhang, Sewon Min, Ludwig Schmidt, Noah A Smith, and Mike Lewis. Mcasuring and narrowing the compositionality gap language models. In Findings of the Association for Computational Linguisties: EMNLP 2023, pp. 5687-5711, 2023.
Silvio Ranise, Christophe Ringeissen, and Calogero Zarba. Combining data structures with non- stably infinite theories using many-sorted logic. In International Workshop on Frontiers of Com- bining Systems, pp. 48 64. Springer, 2005.
Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, al. Beyond the imitation game: Quantifying and extrapolating the capabilities of language models. arXiv preprint 246.05500 2022.
John Sweller. Cognitive load during problem solving: Effects on learning. Cognitive science, 12(2): 257-285, 1988.
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-36333 2021.
Romal Thoppilan, Daniel De Freitas, Jamie Hall, Noam Shazeer, Apoorv Kuishreshtha, Heng-Tze Cheng, Alicia Jin, Taylor Bos, Leslie Baker, Yu Du, et al. Lamda: Language models for dialog applications. arXiv preprint arXiv:2201. 08239, 2022.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi. Quoe V Le, Denny Zhou, et al. Chain-of -hthnghf- prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824-2466 24837, 2022.
Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, and Wynne Hsu. Faithful logical reasoning via symbolic chain-of-thought arXiv preprint arXiv:2405. 18357, 2024.
12

---

Published as a conference paper at ICLR 2025
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. Satlm: Satisfiability- aided language models using declarative prompting. Advances in Neural Information Processing Systems, 36, 2024.
Yunhu Ye, Binyuan Hui, Min Yang, Binhua Li, Fei Huang, and Yongbin Li. Large language models versatile decomposers: Decomposing evidence and questions for table-based reasoning. In Proceedings of the 46th International ACM SIGIR Conference on Research and Development in Information Retrieval, pp. 174-184, 2023.
Wanjun Zhong, Siyuan Wang. Duyu Tang, Zenan Xu, Daya Guo, Yining Chen, Jiahai Wang, Jian Yin, Ming Zhou, and Nan Duan. Analytical reasoning of text. In Findings of the Association for Computational Linguistics: NAACL 2022. pp. 2306-2319, 2022.
Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuur- mans, Claire Cui, Olivier Bousquet, Quoe V Le, et al. Least-to-most prompting enables complex reasoning in large language models. In The Eleventh International Conference on Learning Rep- resentations, 2023.
13

---

Published as a conference paper at ICLR 2025
A FIRST-ORDER LOGIC PRELIMINARIES
To clarify the first-order logic vocabularies used in the paper, we give basic definitions as prelim- inaries based on Ranise al. (2005) and Jooanovvć & Barrett (201T). To help understanding, also provide an example the definitions, where the example is sampled from the AR-LSAT test set (Zhong et al. 2022). In this work, we use many-sorted first-order logic, which is one of the vari- ants of the standard first-order logic, to better reflect the scenarios of the real-world logical reasoning problems.
A.I 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 ) (S, F, P) consists of countable sets of sorts S.function symbols F, and predicate symbols P. Each function symbol ff is associated with a type 81 X ... x Sn where 2 0 and $1.-.., Sn, s E S. Funetion symbols with called constants of sort s. Each predicate symbol is associated with a type 81 X ... x 8n. where and 81, 8n E.S.
(i.e. zero arity) are
Let Σ be a signature. A set X of E-variables (or simply variables) is countable set of variable names. Each variable name associated with sort Σ. Based on variables, define terms. Intuitively, terms are variables or functions applied to tuple of other terms.
Definition 6 (Terms). E-terms over X (or simply terms) are defined as follows. Each variable E X of sort is a term of sort If (1," IIn are terms of sorts 81: ....... , respectively, and is a function symbol of type 81 X .... x sn + s, then f(t,,".. ffn is a term of sort s.
Based terms, define atoms. Intuitively, atoms predicates applied to tuple of terms.
Definition 7 (Atoms). E-atoms over X (or simply atoms) are defined as follows. If l,,... bn tterrm over X of sorts 81,". .. Sn. respectively, and p is predicate symbol with the type X ... X Sn, then p(t1.... fx) is an atom.
Additionally, literals are atoms negation atoms, and clauses are disjunctions of literals. We finally define formulas by using above definitions with logical connectives and quantifiers.
Definition 8 (Formulas). E-formulas over X (or simply formulas) are defined as follows. Each E-atom over X is a formula. If a and 3 are formulas, then so are -a, a A B, and a V B. If E a variable of sort and a a formula, then so are Er a and Vx a.
We give example of the definitions of first-order logic syntax with the following formula in the AR-LSAT test set.
Example 1. signature is given
Σ1 = (ppositions, F, P)
where == (displayed Reigel, 1, 1,6) such that displayed has the type positions - polters, Reigel is constant of sort potters, and 1 and 6 constants of sort positions, and P {== such that ss is of the type positions x positions. We note that the equality symbol ss is always implicit from the context. If p variable of sort positions, then p and displayed(p) are Σj-terms of sort positions. Then, displayed(p) z Reigel, p 1, and ~ are atomms. Finally, the following is one example of -formula
(Vp positions) (displayed(p) Rs Reigel) + (p ~ IVp~6)
which is the first-order logic translation of the natural language sentence "Reigel's bowl can be displayed only in either position or position 6"
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.
14

---

Published as a conference paper at ICLR 2025
A signature Σ F, 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 (Structures). A E-structure I assigns non-empty domain set D, each sort E S, function / Day x Ds,, - D2 for each function symbol / E F type 81 x...X. 88n - 8, and predicate p' Do, X... x Da.. + {F, Т} for each predicate symbol p E P of type 81 X sn- Note that each constant e of sort is mapped to an element cf E D,.
To evaluate terms and formulas, we extend structures to variables and define interpretations.
Definition 10 (Interpretations). E-interpretation over X (or simply interpretation) is E-structure that additionally assigns a value x' E D, to each variable x E X of sort 8.
We denote / F Φ if an interpretation / evaluates a formula & to true. However, we are not usually interested in the evaluation of formulas in given structure, but interested in specific meaning of functions and predicates. Theories deal with this problem.
Definition (Theories). A E-theory T (or simply theory) non-empty set of E-structures.
To solve practical problems, additionally define the followings. A T-interpretation is E- interpretation that extends some structure in the theory T. formula ø is --satisfiable if F o for some 7- T-interpretattinn I. A formula Φ is T-valid, denoted by Fr Φ. if I F á 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 T-interpretation such that I F o is called T-model of Φ. Definition 13 (Consequences). A formula & is a T-consequence of a formula vb, denoted by 1 Fr d. F & implies / & for all T-interpretations I.
We give an example of the definitions of first-order logic semantics by continuing Example T Example 2. Let us consider the extended signature Σg potteess, F. (=}) where
F {displayed, Larsen, Mills, Neiman, Olivera, Park, Reigel, Serra, Vance, 1, 2, 4, 6). There are many possible Essstructures, and one exemplar structure I2 is:
positions = [1, 2,5,6,45,6,,
D potters = Larsen, Mills, Neiman, Olivera, Park, Reigel, Serra, Vance),
Larsen l Larsen, Mills Mills, Neiman = Neiman, Olivera = Olivera, Park Park, Reigel' Reigel, Serra" Serra, Vance Vance,
1'2 1,, 2,2 2, 3/2 3. 4 4, 5/2 5, 6 6. and displayed (1) = Reigel, displayed (2) = Larsen, displayed (3) = Reigel,
displayed (4) = Reigel, displayed (5) = Reigel, displayed (6) = Reigel.
Since we not consider any additional variable here, Ee-iinteppretation T/ the same as T2-
Now, let the theory T2 be the Σz-theory consisting only of the Σy-structure I which has the same domain assignment to each sort and the same constant function assignments with 12. 12 is a T2- interpretation. If we consider the formula á in Example] I is T>-satisfiable, but not T2-vlli.
Lastly, us determine /2 satisfies dh. Reigel's bowl is displayed the positions and 6, but also displayed in positions 4, and 5. A Tz-interpretation ln does not satisfy the formula o, which means 1n is not a To-model of d.
15

---

Published as a conference paper at ICLR 2025
B FIRST-ORDER LOGIC COMPLEXITY
To quantitatively measure the complexity of first-order logic formulas, we use a parameter following Arias & Khardon (2003). 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 Bjornr 2008).
We present two exemplar formulas and their complexity from the AR-LSAT test set. The first example is as follows:
(3C: :chldren)) (-(C Juan) (assigned(C) x assigned(Juan))).
The formula is already in the CNF expression. It contains two clauses; -(C' Juan) and assigned(C)) assigned(Juan). The first clause has two distinct terms; C' and Juan, and one literal; -(O x Juan). The second clause has four distinct terms; C, Juan, assigned(C"), and (asigned([uan), and one literal; assigned(C) = assigned(Juan). The measured complexity is 2 - 2-4+1=7.
The second example is as follows:
VynSaeenneWPop onSSae(usedPPop) + (onSale(newSoul) A onSale(useddouul
The formula is first transformed into CNF expression follows:
(onSale(newSoull V -onSale V -oSale(ussdPoo))
(onSale(usedSoul) V -onSale(newPPop) V onSale(usedPop)).
contains two clauses. The first clause has three distinct terms; newSoul. newPop. and usedPop, and three literals; mnSale(newSoote -onSale(newPoy and -nnSale( -onSale(usedPPp)) The second clause has the same number of distinct terms and literals. The measured complexity is
+ 33 8
C COMPONENT ACCUMULATION RULES
We describe rules for component accumulation according to a logical dependency structure. aims add components simple subsentences compose more complex subsentences in 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 B.I. The followings the rules for component accumulation:
Rule 1. Start with copying logic units.
Rule 2. If logic dependent D is the only dependent a logic unit U, then integrate into and add the updated U.
Rule 3. If logic dependent Dj depends on another logic dependent D2, then integrate Dj into logic unit U that includes D2 and add the updated U.
Rule 4. If more than one logic dependents D1, Dz.... Dy depend k sentences that include U and each logic dependent D; (i = 1,2, .k). After that, integrate all logic dependents into U and add the updated U.
logic unit U, then add
Rule 5. If more than one components X1, X2,... ... .g depend logic coupler C, then integrate all components into and add the updated C.
We present three examples of component accumulation given sentences and their logical dependency structures in the following section.
16

---

Published as a conference paper at ICLR 2025
D EXAMPLES OF LOGICAL DEPENDENCY PARSING AND COMPONENT ACCUMULATION
We present three examples of logical dependency parsing and component accumulation. For compo- nent accumulation, the applied rules and corresponding logical dependencies are indicated for each accumulation step. (Integration) is additionally inserted for Rule 4 to maintain consistency.
Input
Target sentence:
Each story is assigned team of interns
photographer's assistant and writer's assistant.
Declarations:
interns = Farber, Gombarick, Hall, Jackson, Kanze, Lha}
stories RRomania, Spain, Tuscany)
assistants (photographer, writer)
assigned Function (interns + stories)
trained = Function (interns - assistants)
Output
Logical dependency parsing:
U1="Each story assigned interm",, U2="There intern a photographer's assistant.". There an intern-a writer's assistant.", "m"eeerg")", C2="(merge"", C3="a team of two and"
U1 Cr, U2 -1, Us Cz Us Cz, Ci + Cs, C2 + Cs
Component accumulation:
Rule 1: Each story is assigned an intern. (U1)
Rule 1: There is an intern-a photographer's assistant. (U2)
Rule 1: There is intern-a writer's assistant. (Us)
Rule 5: Each story is assigned an intern a photographer's assistant. (U1 + CC, CC
Rule 5:
story is assigned an intern-a writer's assistant. (U, - C2 U3 - C2)
Rule 5: Each story is assigned a team of two interns-one photographer's assistant and one writer's
assistant. (C1 -> Cs. C2 Cs)
Input
Target sentence:
Xena and at least three other technicians repair radios.
Declarations:
technicians {Stacy, Urma, Wim, Xena, Yolanda, Zane] }
machines (radiox, televisions, VCRs)
repairs Function(technicions, machines -> bool)
Output
Logical dependency parsing:
Ui=a repairs radios.". Di="and three other technicians". D=="exactly D1 U1, D2 + D;
Component accumulation:
Rule I: Xena repairs radios. (U1)
Rule 2: Xena and three other technicians repair radios. (D) U1)
Rule 3: Xena and at least three other technicians repair radios. (D2 - D1)
Figure 5: Example of logical dependency parsing and component accumulation on AR-LSAY
17

---

Published as a conference paper at ICLR 2025
Input
Target sentence:
Each candidate must speak either first or second at at least one of the meetings.
Declarations:
candidates SQ,R.
meetings = (1,2,3
orders (1,,,3,455]
speaks Function Function(cundidaaee meeting orders)
Output
Logical dependency structure:
U1="Each candidate speaks at one of the orders at one of the meetings.", Dı="must", D2="at least",
Dy="either first second"
D1 U1, D2 U1, U1
Component accumulation:
Rule I: Each candidate speaks at one of the orders one of the meetings. (Ui)
Rule 4: Each candidate must speak of the orders
of the orders at of the meetings. (D) + U1) least Each candidate speaks either first or second at one of the meetings. (D3 + U1)
Rule 4: Each candidate speaks
of the meetings. (D2 U1)
Rule 4:
Rule 4:
Each candidate must speak either first or second at at least one of the meetings. (Integration)
Figure 6:
Another example of logical dependency parsing and component accumulation on AR-
LSAT.
E SAT SOLVER FUNCTION PREDICTION ON AR-LSAT
For the AR-LSAT dataset, we additionally need to predict solver function faalver 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 function that checks satisfiability of the query given the constraints.
question "Which the queries MUST be true?", then we need to assign function that checks validity of the query given the constraints.
Logic-LM predicts solver function together with the first-order logic translation by a single infer- ence follows:
7, (4,, NL(p)) K+1 fsolver ~ PLLM(T, NLLc)) f Ir, xt).
(6)
For CLOVER, to incorporate solver function prediction in our problem formulation Eq. perform this prediction at the preprocessing step follows:
we
t. (NI(+ K+1 frotver PL (NI(+x)))=+ K+1 .sotver xx xxx)
6% = CLOVER(T, ()()),,, 4k f1,2,... K + 1}.
18

---

Published as a conference paper at ICLR 2025
F DATASET STATISTICS
In this section, we present dataset statistics of the logical reasoning tasks in Table We describe the details in the following paragraphs. If not mentioned, use the entire test provided by the dataset.
AR-LSAAT-nmotated. We annotate a representative subset of AR-LSAT test set (Zhong et al, 2022 to measure first-order logic translation accuracy at 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 T and a set of natural language sentences, following the steps in Section 2 For each problem, note that the sentences for con- straints 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 T-satisfialle first-order logic formula and double-check its correctness. If a T cannot express the context of the logical reasoning problem, we exclude the sentences in that problem. As result, we collect total of 305 annotated formulas.
ZebraLogic. The ZebraLogic test test (Lin et al. 2025) consists 1,000 zebra puzzles where the puzzle size varies from 2 x to 6 x 6. There 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 x 6, 5 x 5, 5 6, 6
x 5, and 6 6) for test set, which yields total of 240 puzzles.
Puzzle. The entire dataset (Srivastava et al. 2022) 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., 2022) 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, 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.
evaluate the models on the plain subset which includes 198 samples. The plain
The entire dataset (Srivastava al., 2022) consists of 1,500 samples. We use the test set following Pan et al. 2023) which consists of 300 samples.
Deduction.
ProofWriter. We use the test set following Pan et al. (202)), which is a set of randomly sampled 600 examples from the most challenging depth-5 subset.
Table 4: Number of few-shot examples, test examples, and options, and license of the logical rea- soning tasks used in the paper.
Dataset
Shot
Test
Options
License
AR-LSAT Zhong et al. 2022
231
MIT license
AR-LSAT--amottted
N/A
305
N/A
MIT license
Zebral.ogic (Lin et al. 2025
240
N/A
Apache 2.0
Puzzle (Srivastava al. 2022
200
2,3,4.5
Apache 2.0
Symbol (Srivastava et al. 2022
99
5
Apache 2.0
Deduction (Srivastava al.
2022
2
300
3,5,7
Apache 2.0
FOLIO (Han al. 2022)
2
203
CC-BY-SA-4.0 license
ProofWriter [Tafjord et al. 2021
600
CC BY 4.0
19

---

Published as a conference paper at ICLR 2025
G PERFORMANCE ON DIFFERENT LANGUAGE MODELS
Table 5 compares the performance of CLOVER and the neurosymbolic approach baselines on dif- ferent languange models. We include three additional language models including 4o too-mini, gpt-3. 3. Sturbo, and models and the other one is an caaruction-follwingg model. We evaluate these models on the Puz- zle 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. S-turroo-nnnssst.. ruct since the prompt including few-shot examples exceeds the context window of the language model. The results show that CLOVER clearly outperforms the baselines across different language models.
3.5 3-tuutto----- cooooinnttre ruct, which the first two are chat-focused
Table 5: Performance with different language models using CLOVER and neurosymbolic approach baselines.
Puzzle SymbCoT
Symbol SymbCoT
Logic-IM
CLOVER
Logic-IM
CLOVER
gpt-4o-mini 42.5
60.0
60.5
38.4
46.5
71.7
gpt-3.5-turbo
42.5
35.0
63.5
24.2
27.3
iot-3.--turho-instrrct
46.0
N/A
59.0
50.5
N/A
70.7
H INFERENCE TIME COSTS
It difficult to measure inference time costs for methods that use LLMSs with API calls. Specifically, inference time significantly depends on the current network traffic of an API, and the number of parameters are unknown. Despite this limitation, we compare CLOVER and the baselines by their API usage costs, which a reliable way to measure inference time costs.
For comparison, we use gpt-4o- 4o--44-mini LSAT annotated subset. We report the results in Table 6 CLOVER requires larger amount of inference costs compared to the baselines since the compositional first-order logic translation gen- crates formulas for each logical dependency structure of a target sentence. However, the increased inference time cost is worth for the significant performance gain in Table T
language model and measure the costs on the AR-
Table 6: Comparison of inference time costs using CLOVER and the baselines with gpt 4o do-mini.
Costs (USD)
Standard
0.02
CoT
0.02
Logic-LM
0.08
SymbCoT
0.15
CLOVER
0.30
20

---

Published as a conference paper at ICLR 2025
I IMPACT OF SAT-BASED FIRST-ORDER LOGIC VERIFICATION
To further analyze an impact of using satisfiability in the verification algorithms, we compare those baselines: syntax consistency and LLM with instruction. First, 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 based first-order logic verification is inspired by the previous works (Pan al.)
2023 Kirtania et al. 2024 Xu et al. 2024 Chen et al. 2024 Madaan et al. 2024 Ni et al. 2023).
We report the results Table 7 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 7: Comparison of different first-order logic verification approaches AR-LSAT and Ze- bral.gic..
Verification
AR-LSAT
ZebraLogic
Random
55.0
70.0
Syntax consistency
59.7
70.8
LLM w/ instruction
53.3
70.0
Logical consistency
61.9
74.2
Disproving
62.8
75.4
21

---

Published as a conference paper at ICLR 2025
J FEW-SHOT PROMPT EXAMPLES
Prompt Logical Dependency Parsing
###
Definition
(Explain definition of logical dependency structures)
### Instruction
Given declarations and a sentence, generate different possible logical dependency structures of the sen- tence. When generating logical dependency structure, first declare each component and indicate the dependency and another. The followings rules must be satisfied:
All components except for one should be dependent another component.
Conjunctions could be included in logic units or logic dependents, while not being allocated as logic couplers.
3. No logic coupler can be head of logic dependent.
If logic coupler logic dependent includes sets of words that not adjacent, then separate them with
5. Any logic dependent cannot be conjunction itself.
### Declarations
rechnicians ZaumSort (IStacy, Urma, Wim, Xena, Yolanda, Zane machines EnumSort ([radios, televisicns, VCRs]) repairs Function ( (technicians, machines] -> [bool])
### Sentence
Xena and exactly three other technicians repair radios
Structures
### 1:
Ul="Xena repairs radios", U2="exactly three technicians repair radios", DI="other", Cl="and"
D1 U2: U1 CI; U2 + C1
### 2:
Ul="Xena repairs radios", DI="and other technicians", D2="exactly"
D1 + U1; D2 - D1
### 3:
Ul="Some technicians repair radios", De="Xena and exactly three other technicians"
DI
### Declarations
technicians EnumSort ([Stacy, Urma, wim, Xena, Yolanda, Zane]) machines EnumSort ([radios, televisiens, VCRs]) repairs Function (technicians, machines] -> [bool]]
### Sentence
Stacy does not repair any type of machine that Yolanda repairs
### Structures
### 1:
Ul="Stacy repairs any type machine", U2="Yolanda repairs any type of machine", DI="does not",
C1="that"
D1 + U1; U1 CI; U2 + C1
### 2:
Ul="Stacy repairs any type machine", DI="does not", D2="that Yolanda repairs"
DI > U1: -
Figure 7: Prompt used for logical dependency parsing on AR-LSAT.
22

---

Published as a conference paper at ICLR 2025
Prompt for Component Accumulation
### Definition
(Explain definition of logical dependency structures)
### Instruction
Given sentence and its logical dependency structure, accumulate each component of the logical de- pendeney structure finally reach the original sentence. The followings are rules accumulation:
Start with copying logic units.
2. If logic dependent D is the only dependent of logic unit U, then integrate D into U and accumu- late the updated U.
If logic dependent DI depends another logic dependent D2, then integrate DI into logic unit that includes D2 and accumulate the updated If more than one logic dependents DI, D2, Dk depend on a logic unit U. then accumulate k se- tences that include U and cach logic dependent Di (i=l, 2, k). After that, integrate all logic depen- dents into U and accumulate the updated U.
If more than one components XI, X2, Xk depend logic coupler C, then integrate compo- nents into and accumulate the updated C.
### Sentence
Xena and exactly three other technicians repair radios
### Structure
Ul="Xena repairs radios". U2="exactly three technicians repair radios", DI="other", Cl="and" DI + U2; UI > CI; U2 + C1
### Accumulation Xena repairs radios
exactly three technicians repair radios
exactly three other technicians repair radios
Xena and exactly three other technicians repair radios
### Sentence
Stacy does not repair any type of machine that Yolanda repairs
### Structure
Ul="Stacy repairs any type of machine", U2=aYolanda repairs any type of machine", D1="does not",
Cl="that"
DI UI: UI + CI: U2 C1
### Accumulation
Stacy repairs any type of machine
Yolanda repairs any type of machine
Stacy does repair any type of machine
Stacy does not repair any type of machine that Yolanda repairs
### Sentence each candidate must speak either first second least of the meetings
### Structure
Ul="cach candidate must speak first at one the meetings", U2="cach candidate must speak second at one of the meetings", DI="at least", Cl="cither... or" DI + U1; DI U2: UI + C1; U2 C1 ### Accumulation
each candidate must speak each candidate must speak second at one the meetings
one of the meetings
each candidate must speak first at at least one of the meetings
each candidate must speak second at at least of the meetings
each candidate must speak either first or second least one of the meetings
Figure 8: Prompt used for component accumulation on AR-LSAT.
23

---

Published as a conference paper at ICLR 2025
Prompt for Sequential Translation
### Instruction
Given declarations, the task is to translate sentence into first order logic program. In order to do that, translate the given accumulation of components step by step finally translate the original tence.
### Declarations
technicial RnumSort ([Stacy, Urma, Wim, Xena, Yolanda, Zane])
machines EnumSort (Iradios, televisicns, VCRs])
repairs Function (1 (/techiicinss, machines] -> [boo1])
### Sentence
Stacy does not repair any type of machine that Yolanda repairs
### Accumulation
Stacy repairs any type of machine
Stacy does not repair any type of machine
Stacy does not repair any type of machine that Yolanda repairs ### Translation
FerAll ( lm:maciness, repairs (Stacy, m)
ForAll ( machineess) Not (repairs (Stacy, m
ForAll ( (m:chnnnees Implies (repairs (Yolanda, m), Not (repairs (Stacy, )
### Declarations
people EnunSort (Viadimir, Wendyl)
meals = EnunSort ( (bbreakfast, lunch, dinner, snack)
fcods = EnunSort ( [[fish, hot_cakes, macaroni, omelet, poached.eggs)
eats Function ([people, meals] -> [foods]]
### Sentence
At no meal does Vladimir cat the same kind of food as Wendy
### Accumulation
At no meal does Vladimir eat the same kind of food as Wendy ### Translation
ForAll [m: meals), , eats (Vladimir, m) != eats (Meddy, m)
### Declarations
candi dates KnumSort ( [[Q, R, 8, T, U]}
meetings KnumSort ([1, 2, 31)
speaks = Function [meetings, candi dateis -> [intl]
dates]
ForAll /mmmmmtingg, c:candidates], And (1 <= speaks (m, c), speaks (m, c) <=
5))
### Sentence
speaks fourth and fifth at meeting ### Accumulation
speaks fourth at meeting
speaks fifth at meeting I speaks fourth and fifth meeting
### Translation
speaks (1, R) --
speaks (1, R.) ==
(speassss (1,
speaks ==
Figure 9: Prompt used for sequential translation AR-LSAT.
24

---

Published as a conference paper at ICLR 2025
Prompt for Disproving by Counter-Interppetation
### Instruction
Your task is to determine whether given solution can be included any of the possible scenarios that arise when the given sentence is set as condition. First, you need to calculate all possible scenar- ios that occur under the given sentence interpreting the solution through the given declarations falls into various examples below, you should provide your answer along with a logical explanation for reasoning behind it. Keep in mind that you should focus on logical conditions rather than relying on commonsense when performing the task.
condition, and then check if the situation obtained by
those scenarios. As shown in
### Input
Declarations:
people RnumSort ( [Vladimir, Wendyl)
mea 1s RnumSort (Ibreakfast, lunch, dinner, snack])
fcods EnunSort [iiish hot cakes, macaroni, omelet, poached eggs
eats Function (eeiiio((ppoppe (ppeople, meals] -> [foods]]
Solution:
eats: Vladimir, breakfast -> fish
eats: Vladinir, lunch -> poached egggs
eats: Vladimir, dinner macaroni
eats: Vladimir, snack -> cakes
eats: Wendy, breakfast -> fish
eats: Wendy, lunch -> poached.eggs
cats: Wendy, dinner -> omelet
cats: Wendy, snack fish
Sentence:
Neither of them eats the same kind of food more than once during the day
### Response
Analysis:
cakes on a single day. Vladimir does not eat the same kind of food more than once during the day. Wendy eats fish, poached eggs, omelet, and fish on single day. Wendy eats fish more than once during the day. Therefore, the solution does not logically satisfy the sentence, "Neither of them cats the same kind of food more than once during the day". Answer:
Vladimir eats fish, poached eggs, macaroni,
No
### Input
Declarations:
candidates EnumSort ( (1,, R, S, I, U]}
meetings = EnumSort (11, , 2, 3])
speaks Function ( (meetings, candidates] -> [intl]
FcrA1l [[m:eetinga c:candidates], And (1 <- speaks (m, c), speaks (m, c)
5))
Solution:
speaks: 1, 0->
speaks: 1, R->
speaks: S->
speaks: 1, T->
speaks: 1, U
Sentence:
candidates will speak in the time slot each other any meeting
### Response
Analysis:
At meeting 1, each candidate speaks 1st, 3rd, 2nd, 4th, and 5th. No two candidates speak in the same time slot each other meeting 1. At meeting each candidate speaks 2nd, 5th, 3rd, 4th, and Ist. two candidates speak in the same time slot as each other meeting 2. At meeting 3, each candi- date speaks 5th, 1st, 2nd, 4th, and 3rd. No two candidates speak the same time slot as each other at meeting 3. Therefore, the solution logically satisfies the sentence, "no two candidates will speak in the same time slot as each other any meeting". Answer:
Yes
Figure 10: Prompt used for disproving by coumter-ineeppeettion on AR-LSAT.
25

---

Published as a conference paper at ICLR 2025
K EXTENSIVE ERROR ANALYSIS OF LOGIC-LM
We present in-depth error analysis of Logic-IM (Pan et al. 2023 for first-order logic translation and the corresponding results of CLOVER on the AR-LSAT annotated subset. We follow Pan al. (023) and Ye et al. (2024) for the specification of declarations and formulas of first-order logic. We colorize incorrect translations as red and describe the reason in the following.
Input
Target sentence:
Each locker must be assigned to either one or two children, and each child must be assigned to exactly locker.
Declarations:
children EnumSort ( [[reed Juan, Marc, Paul, Nita, Rachel, Trishal) leckers EnumSort ([1, 2, 3, 4, 5]) assigned= Function ([children] [lockers])
Output
CLOVER:
And (ForA11 :ockers) Or (Count [[c:children]] (c) 1) ass assigned (c) =- 1) =- 2)), ForAll ([e:chi ceeecchhideeee idren], (xi:ts([1:1ockk)) assi gned (c) 1)))
1, Count
Logic-LM:
ForAll [1: lockers], or (Count (drech)ldren), assigred == == 1, (Count
assigned (c) == 1) == 2, Exists ( [b:boys, gigirls), And (assigned (b) == assigned (g) 1))))
Error Analysis of Logic-LM
contains additional constraint that the locker assigned children should contain hoy and one girl.
Figure 11: Example #1 of error analysis of Logic-LM.
Input
Target sentence:
Juan must share a locker.
Declarations:
children EnumSort (IFred, Juan, Marc, Paul, Nita, Rachel, Trishal) lockers EnumSort (11, 2, 3, 4, 51)
assigned Function ([children] -> [lockers])
Output
CLOVER:
Exists ( [e: cdren))) And (c != Juan, assigned (c) == assigned (Juan)
Logic-LM:
Exists (l:chhidreee) assigned (Juan) == assigned (c))
Error Analysis of Logic-LM
The formula is always true. The variable e should not be equal to Juan.
Figure 12: Example #2 of enror analysis of Logic-LM.
26

---

Published as a conference paper at ICLR 2025
Input
Target sentence:
Nita's locker cannot be adjacent to Trisha's locker.
Declarations:
children EnumSort ([Fred, Juan, Marc, Paul, Kita, Rachel, Trisha])
leckers EnumSort ([1, 2, 3, 4, 5])
assigned Function ([children) -> [lockers])
Output
CLOVER:
FCrA11 ( locker,,,,, 12:lockers], Impl ies (And (assigned (Ni 11, assigned(Trisha) == 12), Abs (11 - 12) != 1
Logic-LM:
ForAll ( [1: lockers]), Implies (assigned (Nita) 1, And (assi gned (Trisha) 1, assigned (Trisha) != 1+1, assigned (Trisha) !- 1-1)))
Error Analysis of Logic-LM
means Nita's locker cannot be adjacent and the same to Trisha's locker. The additional constraint should be eliminated.
Figure 13: Example error analysis of Logic-LM.
Input
Target sentence:
Each division toured at least once.
Declarations:
days EnumSort ([Mndayy, Tuesday, Wednesday, Thursday, Friday])
divisions EnumSort ([peratiios,, Production, Sales])
toured = Function ( [days] -> [divisions]
Output
CLOVER:
FcrA11 ([:Al1((::iiiisionn Exists (dya); toured (day) -- d)
Logic-LM:
ForAll ( [d:divisionss Exists ( (Idrdays] toured == d))
Error Analysis of Logic-LM
Variable d simultaneously assigned to two sorts.
Figure 14: Example #4 of emoo analysis of Logic-LM.
27

---

Published as a conference paper at ICLR 2025
Input
Target sentence:
Each building was owned by exactly one of the families.
Declarations:
families = EnumSort ( ([Trents, Williamses, Yandells])
buildings = EnumSort ( (forre,, granary, inn, mill, stable))
owned Function ([families, buildings] -> [bool])
Output
CLOVER:
ForAl1 ( (b: 1di ngs], Exists ( [f: fami ies], And (owned (f, b), ForA11 ([m2 liss, Impl ies (f2 !- f, Not (owned (f2, b) )))))
Logic-LM:
ForAll ( (b:buildings) Exists famimie)]]] owned b))
Error Analysis of Logic-LM
means each building was owned by least one of the families, not exactly one of the families.
Figure 15: Example #5 of error analysis of Logic-LM.
Input
Target sentence:
Neither the inn nor the mill belonged to the owner of the forge.
Declarations:
families EnumSort ([Trents, Williamses, Yandells]) buildings = EnumSort ( [forge, granary, inn, mill, stablel)
owned = Function (1 (Ifamilies, suildings] -> [bool])
Output
CLOVER:
ForAll [ families) Implies (owned (f, forge), And (Not (owned inn) Not (owned (f, mill))))
Logic-LM:
EcrAll (b:buildings) Implics ies (owned (forge, b) Not (Or (owned (inn, b)
(mill, b))))
Error Analysis of Logic-LM
The domain of the function does match with the declarations.
Figure 16: Example #6 of emoo analysis of Logic-LM.
28

---

Published as a conference paper at ICLR 2025
Input
Target sentence:
Reigel's bowl can be displayed only in either position position 6.
Declarations:
petters EnumSort ([Larsen, Mills, Neiman, Olivera, Park, Reigel, Serra,
Vance])
positions EnumSort ( [[1, 2, 4, 6])
displayed = Function [positions -> [potters])
Output
CLOVER:
(orAL[([p:position)) Implies (displayed (p) == Reigel, Or (p == 1, == 6)
Logic-LM:
or (displayed (1) Reigel, displayed Reigel)
Error Analysis of Logic-LM
means Reigel's bowl is displayed in either position or position 6. We note that Reigel's bowl can- not be displayed.
Figure 17: Example #7 of error analysis of Logic-LM.
Input
Target sentence:
Nash is assigned to a committee, Nash must be the leader for that committee.
Declorations:
velunteers KnumSort [Haddad, Josl in, Kwon, na, Nash] committees KnumSort [x, Y, x1)
positions = EnumSort ( [leader, secretary, treasurer))
assigned Function ccmmiiteess, pesitiens] -> [volanteers])
Output
CLOVER:
FerAll conmi ccommittees]] Implies (Exists ((p:positions), assigned (c, p) Nash), assigne assigned (c, leader) Nash)
Logic-LM:
ForAll le: commiittees), Implies (assigned (c, Leader) Nash,
ForAll ( [p:positions] assigned (c, p) Nash) )
Error Analysis of Logic-LM
The formula always false. Variable p should not leader.
Figure 18: Example #8 of error analysis of Logic-LM.
29

---

Published as a conference paper at ICLR 2025
Input
Target sentence:
Nottingham and Sunnyside are hoth visited, but not consecutive days.
Declarations:
days = EnumSort (Monday,, Tuesday, Wednesday, Thursday, Fridayl) neighborhoods = EnunSort ( HlHid, Lakeville, Nottingham, Oldtowr, Park.Plaze Sunnysidel]
visited Function [days] [neighborhoods)
Output
CLOVER:
(Exists ( [d:days], visited == Not Noghingham), Exists ([drdays), visited (d) == Sunnyside), ForAll ([dl days, d2 :d:ys),,
Implies (And (visited (d1) == Nottingham, visited Sunnyside), Abs (dl d2) 1)))
Logic-LM:
And (Exists [d:dayss, , visited == Nottingham), Exists (Id:days),
(d) Sunnyside), Not (Exists ([d:days), And (visited Nottingham, visited((+1) Sunnyside) )
Error Analysis of Logic-LM
means that Nottingham visited the day hefore Sunnyside visited. We note that the opposite should be also possible.
Figure 19: Example #9 of enror analysis of Logic-LM.
30


Reviews:
[{"review_id": "o6kdM9TOlc", "reviewer": "Reviewer_5CZv", "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.", "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?\n2. Can the authors provide more insights into how CLOVER compares with CoT-based methods designed for improving implicit reasoning of LLMs?\n3. Why not test CLOVER on a wider range of language models to assess its generalizability?", "limitations": "", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 2, "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.\n- The experimental results are robust using GPT4-o, showing improvements over other methods across multiple benchmarks.\n- The authors propose two SAT-based first-order logic verification algorithms for selecting a sample from LLMs' logical code generations.", "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.\n- 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.\n- 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.\n- 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.", "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": "yeyZ2RU9pP", "reviewer": "Reviewer_yp79", "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.", "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?\n\n2. Line 149: how to read this formula in natural language? \n\n3. What is the output for the sentence \"A barber shaves all who do not shave themselves.\"? \n\n4. How are \"Declarations\" created? \n\n5. How to decide a sentence not fit for your system? (or how to decide an unintended input sentence?)", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 1, "contribution": 2, "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.", "weaknesses": "Not all natural language sentences can be translated to first-order logic forms. Authors did not discuss what sentences cannot be translated. \n\nAuthors 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. \n\nTheoretically, the meaning of natural language is not logical formula. This work is valued within fixed benchmark datasets. \n \nThe formalism of the paper is not easy to read.", "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": "uUMN9XbEmW", "reviewer": "Reviewer_W7Jx", "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.", "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.  \n\n- 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.\n\n- 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)?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 3, "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).\n\n- 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.", "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.)\n\n- 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.\n\n- (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.\n\n- (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.", "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)