Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
Authors: Liangming Pan
Alon Albalak
Xinyi Wang
William Yang Wang
Venue: EMNLP 2023 Findings (2023)
Keywords: Logical Reasoning
Language Model
Symbolic Language
Self-Refinement
TL;DR: This paper introduces a novel framework, Logic-LM, which integrates LLMs with symbolic reasoning to improve logical problem-solving.

Abstract: Large Language Models (LLMs) have shown human-like reasoning abilities but still struggle with complex logical problems. This paper introduces a novel framework, Logic-LM, which integrates LLMs with symbolic solvers to improve logical problem-solving. Our method first utilizes LLMs to translate a natural language problem into a symbolic formulation. Afterward, a deterministic symbolic solver performs inference on the formulated problem. We also introduce a self-refinement module, which utilizes the symbolic solver's error messages to revise symbolic formalizations. We demonstrate Logic-LM's effectiveness on five logical reasoning datasets: ProofWriter, PrOntoQA, FOLIO, LogicalDeduction, and AR-LSAT. On average, Logic-LM achieves a significant performance boost of 39.2% over using LLM alone with standard prompting and 18.4% over LLM with chain-of-thought prompting. Our findings suggest that Logic-LM, by combining LLMs with symbolic logic, offers a promising avenue for faithful logical reasoning.

LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
Liangming Pan
Alon Albalak
Xinyi Wang
William Yang Wang
University of California, Santa Barbara
(liangmingpan, alon_albalak, xinyi_wang, nangwilliamyyangeeusbb.b edu
Abstract
Problem
G
Goal
Large Language Models (LLMs) have shown human-like reasoning abilities but still strug- gle with complex logical problems. This pa- per introduces novel framework, LOGIC- LM, which integrates LLMs with symbolic solvers improve logical problem-solving. Our method first utilizes LLMs to translate a natural language problem into a symbolic formulation. Afterward, a deterministic sym- bolic solver performs inference on the for- mulated problem. We also introduce self- refinement module, which utilizes the symbolic solver's 's error messages to revise symbolic for- malizations. We demonstrate LOGIC-LM ef- fectiveness on five logical reasoning datasets: ProofWriter, PrOntoQA, FOLIO, LogicalDe- duction, and AR-LSAT. On average, LOGIC- LM achieves a significant performance boost 39.2% over using LLM alone with standard prompting and 18.4% over LLM with chain-of- thought prompting. Our findings suggest that LOGIC-LM, by combining LLMs with sym- holic logic, offers promising avenue for faith- ful logical reasoning.
Problem Formulator
Symbolic Formulation
oofis "o
Self- Refine
Symbolic Reasoner
Symbolic
Result
Result
Answer
Interpreter
Figure I: Overview of our LOGIC-LM framework.
Despite the advances of LLMs, they still strug- gle with complex logical reasoning problems (Liu et al., 2023b). Recent studies (Golovneva et al., 2023; Ribeiro al., 2023b; Lyu et al., 2023) found that LLMs occasionally make unfaithful reason- ing, i.e., the derived conclusion does not follow the previously generated reasoning chain. While chain-of-thought may imitate human reasoning pro- cesses, the fundamental nature of LLMs remains that of black-box probabilistic models, lacking mechanism guarantee the faithfulness of reason- ing (Shanahan, 2022). contrast, symbolic infer- ence engines, such as expert systems (Metaxiotis et al., 2002), are faithful and transparent because the reasoning is based on cumbolic-representee knowledge and follows well-defined inference rules that adhere to logical principles. The main obsta- cle is how to accurately translate problem into symbolic representations, considering the inherent ambiguity and flexibility of natural language. This is precisely where LLMs excel, making LLMs a promising complement to symbolic solvers.
1 Introduction
Logical reasoning is cognitive process that in- volves using evidence, arguments, and logic to ar- rive at conclusions or make judgments (Huang and Chang, 2023). It plays a central role in intelligent systems for problem-solving. decision-making and critical thinking. Recently, large language models (LLMs) (Brown et al., 2020; Ouyang et al., 2022a; OpenAl, 2023) have exhibited emergent ability to "reason" like human (Wei al., 2022a). When prompted with step-wise explanations of reasoning ("chain of thoughts"),, or simple prompt "Let's think step by step.", these models are able to an- swer questions with explicit reasoning steps (Wei et al., 2022b; Kojima et al., 2022).
This drives our exploration of neuro-symbolic methods that integrate LLMs with symbolic reason- ing. As illustrated in Figure I, we present LOGIC-
'Code and data are publicly available at https://githhn con/ tom/teaccherpetee seteacchepppttrppaoooii--LLL

---

LM, novel framework that decomposes a logical reasoning problem into three stages: Problem For- mulation, Symbolic Reasoning, and Result Inter- pretation. During problem formulation, an LLM converts the natural language description of the problem into an appropriate symbolic formulation, identifying key entities, facts, and rules present in the problem statement. Subsequently, at the symbolic reasoning stage, a deterministic symbolic solver performs inference on the symbolic formula- tion. Lastly, result interpreter explains the output and maps it to the correct answer. By incorporating LLMs with symbolic solvers, we can exploit the robust natural language understanding capabilities of LLMs to precisely represent the problem using symbolic representations, while also taking advan- tage of the logical faithfulness and transparency offered by symbolic solvers. To improve the accu- racy of the symbolic parsing, we also incorporate the idea of self-refinement to iteratively revise the generated logical form using the error messages from the symbolic solver as feedback.
(8 4.3). Finally, by analyzing the impact of self- refinement, we highlight the effectiveness of incre- mentally revising symbolic formalizations when interacting with the symbolic solver ($ 4.4).
2 Related Work
Language Models for Logical Reasoning. Re- cent works in adapting LLMs for logical reasoning tasks can be broadly categorized into two groups: 1) fine-tuning approaches that optimize LLMs' rea- soning ability through fine-tuning or training spe- cialized modules (Clark et al.. 2020; Tafjord et al., 2022; Yang et al., 2022), and 2) in-context learning approaches that design special prompts to elicit LLMs' step-by-step reasoning capabilities. Typical methods include fhaiinof-tthughhe prompting (Wei et al., 2022b; Wang al., 2023) that generates ex- planations before the final answer and the least-to- most prompting (Zhou et al., 2023) that breaks the problem down into simpler components that can be solved individually. Both the above approaches perform reasoning directly over natural language (NL), providing greater flexibility than symbolic- based reasoning. However, the intrinsic complexity and ambiguity of NL also bring undesired issues such as unfaithful reasoning and hallucinations. Different from prior works, we use symbolic language as the basic unit of reasoning. This effec- tively transfers the burden of executing complex, precise reasoning from LLMs to more reliable, in- terpretable external symbolic solvers. Simultane- ously, leverage the strong in-context learning ability of LLMs formulate the NL-based prob- lem into suitable symbolic representations, thus maintaining the benefit of flexibility.
We showcase the adaptability and effective- ness of LOGIC-LM on five logical reasoning datasets: ProofWriter (Tafjord et al., 2021), PrOn- toQA (Saparov and He, 2023), FOLIO (Han et al., 2022), AR-LSAT (Zhong et al., 2022), and the Log- icalDeduction dataset from BigBench (Srivastava et al., 2022). These datasets cover wide range of logical reasoning problems, including:
Deductive Reasoning problems
First-Order Logic (FOL) reasoning problems
Constraint Satisfaction Problems (CSP)
Analytical Reasoning (AR) problems
We integrate four types of symbolic inference tools tailored these problems: 1) logic programmiing engine that supports deductive reasoning through forward/backwward chaining; 2) FOL inference en- gine that derives new conclusions based on FOL rules and facts, 3) constraint optimization engine that provides solvers for CSP over finite domains, and 4) boolean satisfiability problem (SAT) solver that solves analytical reasoning problems.
Although prior works (Mao et al., 2019; Gupta et al., 2020; Manhaeve et al., 2021; Cai et al., 2021; Tian et al., 2022; Pryor et al., 2023) also propose neuro-symbolic methods to combine neural net- works with symbolic reasoning, these methods suf- fer from limitations such as hand-crafted spe- cialized module designs that are not easily gen- eralizable, or brittleness due to the difficulty of optimization. In contrast, we propose a more gen- eralizable framework that integrates modern LLMs with symbolic logic without the need for training or designing complex problem-specific modules.
Our evaluations show that the strategy of inte- grating LLMs with symbolic solvers performs sig- nificantly better than purely relying LLMs for logical reasoning, with an average improvement of 39.2% over the standard prompting and 18.4% over the chain-of-thougee prompting ($ 4.1.. We also find that LOGIC-LM becomes increasingly ef- fective as the required reasoning depth increases
Tool- lug--uugeetedd Language Models. Language models have inherent limitations such as the inabil- ity to access up-to-date information, take actions, or perform precise mathematical reasoning. To

---

Nogg pirt language mode cou hoee sas performanee
In anaiz e car stons there those verirde timetce
boutoons condur neenkiyy Esomatherg oo,, then metal hall nade ron.
bangzage model hos good per memos used by some resorrhern
narwer Life and mirton The tratton the secrnds- nowest The mition is newo than tonvent be
work ued some ressorcho the shout pop
goen bong age mode then the same
garttang
The tovertts dites
th followng re statement trve.
fele,
el the somee di the skiua.
Cf the minsan cheeklest
Problem Formulator
Rules:
Facts:
Dossin:
Veriab les:
Monalo, Truc) - Conductflkttttpy.. Thur)
Earllanggeeeedeeii GiantO (oo.Fecfhrrancccee))
I: slreer
insturd (3.2.3
MastoCCrsnts, Trae) - Motalix, Trus)
3: aewwsssi
mithon e 11,2
(MaddlrSarrallee heuaarts)
ouzvertiike
Expprapraade Slant(bert) Langaggtooeeggrrr A (eengggr)) (aart(
Constraints:
Condurtheerittyyhooll hates)
Qvery:
méntoon conventble
Query: Pakstorggec)
MlltiisentCCmdaanniiimi mitikan, commertible)
Symbolic Reasoner
Logic Programming
First-order Logic Prover
Constraiint Optimitation
SMT Solver
Result
Clnductllecticctyyaaallll True)
Entailment
(convertble: 1, tractor: minttnn:) 3)
Interpreter
Answer
The statement "Nalls cannot electricity" is false.
The statement 'SPPTS popular" true.
A) The convertible is the oldest.
Figure 2: Overview of LOGIC-LM model, which consists of three modules: (J) Problem Formulator generates symbolic representation for the input problem with LLMs via in-context learning (2) Symbolic Reasoner performs logical inference on the formulated problem, and (3) Result Interpreter interprets the symbolic answer.
address this, recent work has begun to augment lan- guage models with access to external tools and re- sources, such as the information retriever (Nakano et al., 2021: Shi et al., 2023; Lazaridou et al., 2022), calculator (Cobbe et al., 2021), code in- terpreter (Wang et al., 2022), planner (Liu et al., 2023a), and other pre-trained models (Shen et al., 2023), Recent works (Gao et al., 2023; Chen et al.. 2022) have achieved improved performance arithmetic reasoning tasks by generating Python programs that specify the reasoning procedure as chained commands in the order of execution. How- ever, this idea has not been extended to logical reasoning problems, primarily due to the challenge of representing their highly "non-lincar" reasoning procedure (e.g., hypothesizing, case-by-case analy- sis. and the process of elimination) with functional programming. Our work provides novel way solve this within the framework of augmented LLMs. Instead of parsing the moblem-solvinn pro- cedure as programs, we only describe the problem with symbolic language using LLMSs and then of- fload the reasoning to external symbolic solvers.
et al., 2022; He- He-Yueya al., 2023; Jiang et al., 2023). These works demonstrate the proficiency of LLMs in translating a considerable fraction of mathematical problems into formal specifications defined in tools like SymPy (Meurer et al., 2017), IsabelleHHOL (Paulson, 1994), and Lean (de Moura et al., 2015). Mathematical reasoming can be con- sidered a specialized subset of logical reasoning. primarily focused on numeric deductions. Due this numeric specificity, mathematical problems are often more readily translatable to symbolic forms. In contrast, logical reasoning covers a wider array of problem types, often requiring a deeper under- standing of world knowledge and commonsense for effective parsing into symbolic forms. Despite plenty of works studying mathematical reasoning, our work pioneers in extending the concept of auto- formalization
broader range of logical reason- ing tasks with modern LLMs.
3 LOGIC-LM
As shown in Figure 2, the inputs of our model are logical reasoning problem P described in natural language, along with goal G in the form of multiple-choice or free-form question. LOGIC-LM then follows a problem formulation soaud-easoninn paradigm to solve the problem.
fotooFoommaliztioo. The concept of convert- ing natural language into symbolic representations has been widely adopted in nuto-formalization for mathematical reasoning (Wu et al., 2022; Drori

---

In the Problem Formulation stage, we prompt an LLM translate the problem and the goal into a task-specific symbolic language. In the Symbolic Reasoning stage, we call a deterministic symbolic solver, e.g., a logic programming engine, to ob- tain a symbolii-representeed answer. Finally, an LLM- or rule-based Resuli Interpreter is respon- sible for translating the answer back to natural language. Using this approach, the reasoning is guaranteed to be faithful as long as the problem formulation is correct since the answer A is the result of exccuting deterministic algorithms (e.g., wwwpa//bbawwwrd-hhhhiii
Logic Programming (LP) Language. Deduc- tive reasoning typically starts from known facts and rules, and iteratively makes new inferences until the goal statement can be proved or disproved (Poole and Mackworth, 2010). The Prolog logic pro- gramming language (Clocksin and Mellish, 2003; Körner et al., 2022) is arguably the most prominent symbolic language to describe deductive reasoning problems. We adopt its grammar represent problem as facts, rules, and queries.
Facts: a fact F is simple statement with a predicate and a set of arguments, formulated as P(al..... ;0n. an), where P is the predicate name and each argument ag can be a variable, entity, num- ber, or bool. For example, Age(Peter, 31) means "Peter's 's age is 31", and MadeOf (Nails, True) represents the fact "Nails are made of iron".
embedded within the symbolic reasoner. Compared to previous methods based on chain-of -fttouhhhthhtt,,..o our framework reduces the burden of LLMs by shifting their focus from "solving the problem by reasoning step-by-step" to "representing the problem in symbolic language".
Rules: rules are written in the form of clauses: AA Fm+1A A- - Fn, where cach Fj is fact and the rule means "if the facts Fi,... Fm.. are true, then the facts Fm+1 ... F, are also true."
3.1 Problem Formulator
Intuitively, LLMs may struggle with directly solv- ing complex reasoning problems. However, they have demonstrated a notable ability to comprehend textual inputs and translate them into formal pro- grams, such as mathematical equations (He- Yueya al., 2023) Python codes (Gao et al., 2023). We posit that this capability to formulate problems into different languages can be extended to symbolic languages as well. We leverage the few-shot gener- alization ability of LLMs to achieve this. By pro- viding the LLM with detailed instructions about the grammar of the symbolic language, alongside few demonstrations as in-context examples, we observe that LLMs, like InstructGPT (Ouyang et al., 2022b) and GPT-4 (OpenAI, 2023), can effectively follow the instructions to identify key entities, facts, and rules present in the problem statement, and then translate these elements into symbolic language following our defined grammar.
Queries: a query Q is simply another fact re- quired to be proved based on known facts and rules.
First-Order Logic (FOL). While the logic pro- gramming language efficiently represents common deductive reasoning problems, it may fail to rep- resent more complex first-order logic (FOL) prob- lems. To address this, also include the FOL grammar (Enderton, 2001) in Appendix A. A prob- lem is then parsed into a list of FOL formulas, which are divided into Premises (the known in- formation from the problem) and Conclusion (the unknown formula to be proved). An example sen- tence and its FOL formula are given in Table 1.
Constraint Satisfaction (CSP). Constraint sat- isfaction problems (CSPs) (Kumar, 1992) aims to find the value assignment of set of objects that satisfy number of constraints. A CSP is often defined as triple DX, where X = {æ1.... .. Φn} a set of variables, D = [DI, ... "P.,...,D)) ,D) is a set of their respective domains of values, and C == (CI, ,Cm} is a set of con- straints. Each variable x; can take on the values in the nonempty domain D, Every constraint Cj is pair (yy,R)), where ty C X is a subset of k variables and R2 is k-ary relation on the corre- sponding subset of domains D,. We use the above syntax to define a CSP problem as variables, do- mains, and constraints. An example is given in both Figure and Table 1.
Specifically, we use four different symbolic for- mulations to cover four common types of logical reasoning problems: deductive reasoning, first- order logic reasoning, constraint satisfaction prob- lem, and analytical reasoning. These formula- tions provide foundation for translating natu- ral language-based problem statements. By defin- ing additional problem-specific formulations, our framework retains the flexibility to accommodate a wider range of reasoning tasks. Next, we will delve into the grammar of each symbolic formulation. Examples of each problem type are in Figure 2.

---

Example
Problem
Formulation
Solver
Dataset
NL Sentence
Symbolic Formulation
If the circuit complete
Complete(Circuit, True)
Deductive
Pro
LP
circuit has the light bulb
Has LightBulb)
Pyke
Reasoning
ProofWriter
then the light bull is glowing.
clowing(LightBull, True)
First-Onler
A Czech person write a book
Fuy Ar((Czec((rn)) Author(z2, ABook(zz) A Publish(z2: 1946))
FOL
Prover9
POLIO
Logic
in 1946.
On shelf, there five books,
blue_ book 2,3,4444
Constraint
python-
CSP
The blue book the right of the yellow book.
yellow_ book (1, 4,5,)
LogicalDeduetion
Satisfaction
constraint
blue_book yellow_oook
repairs(Xena, radios) A
Analytical
Xema and exactly three other technicians repair radios
SAT
Count (I:::ttcccchiiiins]] + Xena
Z3
AR-LSAT
Reasoning
A repairs(t, radios))) = 3)
Table A summary of the symbolic formulations (with examples) and symbolic solvers we use for the five datasets in our study, representing four different types of logical reasoning problems.
Boolean Satisfiability (SAT) Formulation. SAT
FOL Prover. We use Prover9* as the FOL in- ference engine. Prover9 is an automated theorem prover that supports first-order logic and equational logic. It initially converts FOL statements to con- junctive normal form (CNF) and then performs resolution (Robinson, 1965) the CNF deduce whether a conclusion true, false, or unknown.
is the problem of deciding if there is an assignment to the variables of Boolean formula such that the formula is satisfied. Many analytical reasoning problems can be formulated as SAT problems. We adopt the grammar defined in Ye al. (2023) to formulate an SAT problem as (0, T, 2), where @ is a set of constraints defined under the theory? T.
CSP Solver. Solving a CSP is to find value as- signments for all variables that satisfy all given constraints. Commonly used algorithms for this task include backtracking, constraint propagation, and local search variants. To this end, incor- porate the python-constren traintt package which offers solvers for CSPs over finite domains.
and Q is the query of interest.
Table I summarizes the four types of logical reasoning problems, their typical datasets, and the symbolic formulation used represent each type of problem. We also give an example of natural lan- guage statement with its corresponding symbolic formulation for each type. Appendix shows the full prompts we use for the problem formulator. To teach LLMs to better align each statement with its corresponding symbolic form, we use the for- mat #TMBOLIC_FORMULA FORMULA ::: NL_STATSTI STATEMEETT in in-context examples to enable better grounding.
SAT Solver. For solving SAT problems, we use the Z3 theorem prover (de Moura and Bjørner, 2008), a satisfiability modulo theories (SMT) solver developed by Microsoft'. The SMT solver provides algorithms determine whether set of mathematical formulas satisfiable. generalizes the SAT problems to more complex formulas in- volving real numbers, integers, and various data structures such as lists, arrays, bit vectors, and strings. A lot of real-world analytical reasoning problems can be represented as problems of solv- ing system of equations.
3.2 Symbolic Reasoner
After the problem formulator parses the problem P and the goal G into symbolic representations P and G. we call a deterministic external solver depending on the task, to obtain the answer A. Ta- ble summarizes the symbolic solvers we use for each type of logical reasoning problem.
3.3 Self-Refiner
LP System. For deductive reasoning, we incor- porate the Pyke expert system (Frederiksen, 2008), which makes inferences based on the logic pro- gramming language. In response a query, Pyke first creates knowledge base, populating with known facts and rules. Subsequently, it applies forward- and backward-chaining algorithms to in- fer new facts and substantiate the goal.
For complex problems, generating the correct log- ical form may become challenging for LLMs. To address this, introduce self-refinement mod- ule that learns to modify inaccurate logical for-
hhttps://www.c unm. cttp///mccceee//reerrr////////// python-constraint wtwpttuhw..cmmyyyyooooootrrrrraa pettps://githann htttss///githu...om///eevvrrr/

---

mulations using the error messages from the sym- bolic reasoner as feedback. Recent works (Chen et al., 2023; Madaan et al., 2023) have adopted sim- ilar ideas to improve code generation, by teaching LLMs to debug their predicted programs via few- shot demonstrations. Here we extend this idea to refine generated logic representations. If the sym- bolic solver returns an execution error, we instruct the LLM to refine the incorrect logical form, by prompting with the erroneous logic form, the solver's error message, and a set of demonstrations showing common error cases (c.g., a free variable is not bounded to any quantifier in FOL) and their remedies. We run this process iteratively until ei- ther no error messages are returned, or the maxi- mum number of allowable revisions is reached.
each part requiring 0, -, 2, S 3, and S 5 hops of reasoning, respectively. We evaluate the hardest depth-5 subset. To reduce overall experimentation costs, we randomly sample 600 examples in the test set and ensure a balanced label distribution.
FOLIO (Han et al., 2022) is challenging expert written dataset for logical reasoning. The problems are mostly aligned with real-world knowl- edge and use highly natural wordings, and the ques- tions require complex first-order logic reasoning solve. We use the entire FOLIO test set for evalua- tion, consisting of 204 examples.
LogicalDeduction is a challenging logical rea- soning task from the BigBench (Srivastava et al., 2022) collaborative benchmark. The problems are mostly about deducing the order of sequence of objects from a minimal set of conditions. We use the full test set consisting of 300 examples.
3.4 Result Interpreter
Finally, the result interpreter translates the results returned from the symbolic solver back to a natural language answer. For certain problems, this can be achieved through predefined rules; for example, mapping Entailment to true. However, this pro- cess can be more complex for CSPs, e.g., translat- ing /comvertible: 1, tractor: 2, minivan: 3/ to "the convertible is the oldest.". To handle these varying levels of complexity, designed both based and LLM-bbsed result interpreters. Details of the result interpreter are given in Appendix D.
A AR-LSAT (Zhong et al., 2022) a dataset that collects all analytical logic reasoning questions from the Law School Admission Test from 1991 to 2016. We use the test set which has 231 multiple- choice questions. AR-LSAT is particularly chal- lenging, with state-of-the- tof-the-art models only achiev- ing performance slightly better than random guess- ing (Liang al., 2022; Ribeiro et al., 2023a).
We convert all examples into standard multiple- choice format, comprising a problem statement, a question, and potential answers, as shown in Fig- ure 2. We also select 1-5 examples from the train- ing set of each dataset as in-context examples. De- tailed data statistics are in Appendix B.
4 Experiments
Datasets. We evaluate LOGIC-LM on five com- mon logical reasoning datasets, as follows.
Baselines. We compare our model against two baselines that depend solely on LLMs for logical reasoning: 1) Standard LLMs, which leverage in- context learning to directly answer the question; and 2) Chuin--ofThouugh (CoT) (Wei et al., 2022b). which adopts step-by-step problem-solving ap- proach, generating explanations before providing the final answer. We separately evaluate the set- tings that ChatGPT (text-davinci-003)) (Ouyang et al., 2022a) and GPT-4 (gpt-4) (OpenAl, 2023) serve as the under- lying LLMs for all models. To ensure fair com- parisons, we use the same in-context examples for all models. For reproducible results, we set the temperature to 0 and select the response with the highest probability from LLMs. Since all examples are formed as multiple-choice questions, we eval- uate model performance based on the accuracy of selecting the correct answer.
PrOntoQA (Saparov and He, 2023) is a recent synthetic datasct created to analyze the capacity of LLMS for deductive reasoning. We use the hardest fictional characters version of the dataset, based on the results in Saparov and He (2023). Each version is divided into different subsets depending on the number of reasoning hops required. We use the hardest 5-hop subset for evaluation. Each question in PrOntoQA aims to validate a new fact's veracity, such as "True or false: Alex is not shy.".
GPT-3.5
ProofWriter (Tafjord et al., 2021) is another commonly used dataset for deductive logical rea- soning. Compared with PrOntoQA, the problems are expressed in more naturalistic language form. We use the open-world world assumption (OWA) subset in which each example is a (problem, goal) pair and the label is one of (PROVED, DISPROVED, UNKNOWN). The dataset is divided into five parts,

---

ChatGPT (gpt-3.5-turbo)
GPT-3.5
((ext-davinci-003)
GPT-4 (gpt-4)
Dataset
Standard
CoT
Logic-LM
Standard
Co'I
Logic-LM
Standard
Co'I
Logic-L.
PrOntoQA
47.40
67.80
61.00
51.80
83.00
85.00
77.40
98.79
83.20
ProofWriter
35.50
49.17
58.33
36.16
48.33
71.45
52.67
68.11
79.66
FOLIO
45.09
57.35
62.74
54.60
57.84
61.27
69.11
70.58
78.92
LogicalDedductin
40.00
42.33
65.67
41.33
48.33
62.00
71.33
75.25
87.63
AR-LSAT
20.34
17.31
26.41
22.51
22.51
25.54
33.33
35.06
43.04
Table 2: Accuracy of standard promoting (Standard), chain-of-thoughee promoting (CoT), and method (LOGIC- LM, without self-refinement) on five reasoning datasets. The best results within each base L.M are highlighted.
4.1 Main Results
GPT-3.5
GPT-4
Dataset
SR
EateRate
Rate
Ese_Ace
Exe Rale
Exc_Acc
We report the results of LOGIC-LM (without self- refinement) and baselines in Table For LOGIC- LM, a symbolic solver does not return an answer when there are grammar errors in the symbolic formulation. For these un-executable cases, we fall back using chain-of-thought to predict the answer. We have three major observations.
99.4%
84.9
100.0%
83.2
ProntoQA
100.0% 10.6
85.0
100.0%
83.2
87.3%
99.0%
79.6
ProofWriter
95
74.1
99.0%
79.6
66.7%
61.8
79.9%
TOLIO
84.3% 117.6
64.3 f25
85.8% fs.
79.9 Ja.5
Logical
100.0%
62.0
100.0%
87.6
Deduction
100.0%
100.0%
1. Logic-LM significantly outperforms stan- dard LLMs and CoT across all datasets. With GPT- 3.5, our method outperforms standard LLM all datasets, with an average improvement of 39.2%. This highlights the benefit of combining LLMs with external symbolic solvers for logical reason- ing. LOGIC-LM also improves CoT by a large mar- gin of 18.4% on average, showing that offloading the reasoning to symbolic solvers greatly improves faithfulness compared with pure language-based reasoning with COT.
11.3%
$7.7
32.6%
60.0
AR-LSAT
21.8% 110.5
60.3
f2.6
39.8%
17.2
58.8 J1.2
Table Analysis of accuracy and execution status of LOGIC-LM. We present the percentage of executable logical formulations (Exe_Rate)) together with the accu- racy of the execution (Exe_Acc). SR represents before (-) and after (+) self-refinement.
that CoT emulates human forward-chain reasoning: beginning with known facts and sequentially de- riving new conclusions until the goal is met. This reasoning style aligns well with problems the PrOntoQA and ProofWriter datasets. However, FOL and CSP problems often necessitate more sophisticated reasoning strategies that are "non- linear" compared to standard forward-chain rea- soning. These include hypothesizing, conditioning, recursive inference, and the process of elimina- tion. Compared to CoT, the integration of symbolic solvers is better suited to these reasoning styles, hence yiclding a more marked improvement on FO- LIO (+21.85%) LogicalDeduction (+45.67%) and AR-LSAT (424.14%).
2. GPT-4 outperforms GPT-3.5 by a large margin of 48.46% on average for the standard prompting. This aligns with the assertion that the main hancement of GPT-4 lies in its ability carry out complex reasoning (OpenAI, 2023). Although this may indicate that the logical reasoning capability can be boosted by scaling up the LLM, we observe that GPT-4 still makes numerous unfaithful reason- ing errors. By delegating the reasoning to symbolic solvers, our method can further improve GPT-4 by average of 24.98% and 10.44% for standard prompting and CoT prompting, respectively.
3. While integrating CoT generally enhances LLM performance, we find its benefits compara- tively less substantial or even negative FOLIO, LogicalDeddutton, and AR-LSAT, with a modest improvement of 11.75%, 9.41% %, and -3.2%, re- spectively. On the contrary, the benefits of CoT on ProntoQA and ProofWriter are 51.59% and 33.82%, respectively. A plausible explanation is
4.2 Effectiveness of Problem Formulator
We then evaluate how well LLM can translate given problem into the symbolic formulation used by each symbolic solver. In Table 3, we report the percentage symbolic formulations that are exe- cutable by the corresponding symbolic solver for

---

Accuracy
Standard
CoT
Logic-LM
CoT (GPT-3.5)
Logic-LM (GPT-3.5)
90
Accuracy
CoT (GPT-4)
Logic-LM (GPT-4)
81.7
80
73.6
71.3
80
78.43
79.9
79.41
70 76.3
73.5
75
60
57.7
52.6
70.58
50
-8-
47.3
59.4
64,56
63.84
51
65
62.25
38.3
40
33.5
60
30
$7.87
Rounds
2
Reasoning Depth
79.4%
Figure 3: Accuracy of different models for increasing size of reasoning depth on the ProofWriter dataset.
GPT-4
79.3%
85.3%
85.3%
85,8%
Figure 4: The accuracy for different rounds of self- refinement, with the corresponding executable rates.
each dataset EExe_Rate), Generally, LLM demon- strates high proficiency in transcribing problems into symbolic formats, evidenced by its near 100% Exe_Rate on ProntoQA, ProofWriter, and Logi- calDeduction. However, the high performance on these datasets is somewhat anticipated, given that their problems mostly synthetically generated, limiting language variability. When it comes to datasets comprising real-world, expertly crafted problems, such as FOLIO and AR-LSAT, GPT- 4's performance notably less promising, with Exe_Rate scores of 79.9% and 32.6% respectively. This discrepancy underscores the inherent chal- lenges associated with converting roal-world prob- lems into their logical equivalents.
ple, LOGIC-LM outperforms CoT by 7.1%, 5.0%, 12.7%, 20.0%, and 39.4% on depth-0, depth-1, depth-2, depth-4, and depth-5 problems, respec- tively. In LOGIC-LM, multi-step logical reasoning is delegated external symbolic solvers, thereby transitioning the challenge of LLM from problem- solving to problem representation. Ideally, the com- plexity formally representing a problem state- ment in logical form should remain relatively con- stant, regardless of whether the questions require simple or complex reasoning. The trends in Fig- ure 3 validate this assumption. The performance of Standard and CoT declines precipitously with the escalation of problem complexity. However, this trend is less prominent for LOGIC-LM, indicating that the robust reasoning capabilities provided by external solvers substantially mitigate performance degradation for complex reasoning problems.
Rate only reflects the grammar correctness the logical form. We also report the accuracy of the executable samples (Exe_Acc) to measure the semantic correctness. We find that logical forms generated by GPT-4 generally achieve high Exe_Acc, even for the most challenging AR-LSAT dataset. Such performance accentuates the poten- tial of symbolic solvers in bolstering the model's logical reasoning prowess, contingent on the pre- cise translation of problems into symbolic forms.
4.4 Impact Self-Refinement
In Table 3, we find that self-refinement is effective in fixing the in-executable symbolic formulations, increasing the Exe_Rate by 5.01 on average. For in-depth analysis, then evaluate the accu- racy and Exe_ across different rounds of self- refinement on FOLIO, namely, 0 (no refinement), 1, 2, and rounds. The results are Figure 4. We find that as the rounds of self-refinement in- crease, the percentage of executable formulations consistently increases, leading to an enhancement in the final performance. This suggests that self- refinement serves as effective tool in aiding the LLM to accurately frame the problem. However, the accuracy tends to stagnate in subsequent rounds. even though the Exe_ Rate continues to increase. This can be attributed to the type of feedback re- ceived by the self-refiner, which is the error mes-
4.3 Robustness of Reasoning
Incorporating symbolic solvers also leads to more robust reasoning. To illustrate this, we report the performance of LOGIC-LM and baselines for questions of varying complexity levels. We ran- domly selected 300 examples from each subset of ProofWriter, ensuring a balanced label distri- bution. The problems in these subsets require <=1, <=3, and <=5 hops of reasoning, respec- tively. The results, shown in Figure 3, indicate that LOGIC-LM becomes inereasingly effective as the required reasoning depth increases. For exam-

---

Problen: "Stnanger Things" is populan Netflix show. If Netflix show is popular, faren will binge-watch it. downloed it.
only if binge-watches Netflix show, "Black Kirror" is Netflix show. Karen binge-watches a Netflix show, she will share it to Lisa.
not download "Black Märror",
Question: the following statenent true, false, uncertain? "Black Mirror" is popular. (C) Uncertain
(A) True
(B)
Generated symbolic Formulation::
Predicates:
NetflikShow(K) x 1s Netflik show.
Popular(x) # x is popular.
Bingowatch(x,
binge-watches y-
Dounload(x, y) # x downloads y.
Share(X,
shares to
Premises:
A Popular(strange-Thinns) "Stranger Things" is popular Netflix show. (NetFLixShow(x) Popular(x) BingeNatch(karen, x)) If Netflix show is popular, Karen will binge-watch it. vx (NetfLixshow(x) A Bingeketch(kareen x) * Download(karen, x)) If and only if Karen au she will download it. betfinnchww(taaactterree -Download(karen, blackttrrrr) # Karen does not "Black Mirrur" is a Netflix show. share it Lisa.
ketfflishoo(straageehhhie
(NetfLiiShow(x) 6ingekatch((eeee,, x) Share(karen, X, lisa))
Conclusion:
Popular (blalkk(aa)M
"Black Mirror" is popular.
Predicted answer:
Figure 5: An example of the generated symbolic representation and the predicted answer by LOGIC-LM.
sage from the symbolic solver. This feedback aids in converting "invalid" symbolic representations into valid ones. However, valid symbolic repre- sentation does not necessarily equate to "correct" problem formulation that accurately represents the problem. This issue could be tackled by enhanc- ing the self-refiner to incorporate feedback beyond the eгror message. e.g., a reward signal from an additional module evaluating the accuracy of gen- erated symbolic form. We leave this as promising direction for future exploration.
expressions accurately. In this case, the model fails to distinguish between the meanings of "below" and "above", resulting in an incorrect constraint Dan > Eve. Example 4 exemplifies GPT-4's chal- lenge with fully grasping the rules of FOL gram- mar, evidenced by the invalid generated formula: Mating(subwayy y) A 9. These eтrоr cases underscore that transforming problems into logi- cal forms remains challenging task for modern LLMs, due to the intricacies of FOL formulation, the innate flexibility of natural language, and the complexity of global problem comprehension.
4.5
Case Study
In Figure 5, we show an example of the symbolic representations generated by GPT-4, together with the predicted answer. In general, LOGIC-LM has demonstrated a potent capacity to interpret com- plex problems into symbolic forms. Nonetheless, there remain certain difficulties in accurately un- derstanding the semantics of the problem.
Conclusion and Future Work
In this work, we propose a novel approach to ad- dress logical reasoning problems by combining large language models with symbolic solvers. We introduce Logic-LM,, one instantiation of such framework, and demonstrate how significantly improves performance over pure LLMs and chain- of of-thought prompting techniques.
We further analyze some error cases in Fig- ure 6 of Appendix E. Example 1 shows case where GPT-4 generates an incorrect FOL represen- tation, stemming from its inability define ap- propriate predicates. Here, instead of creating the predicate EasternwiidTurrky, the model gener- ates a constant, Wi (elldTurre((eaater)) in which wildTurkey is the predicate and eastern is the constant. While this representation is valid in iso- lation, it does not interact well with subsequent constants. This inconsistency is recurring issue in GPT-4's symbolic form generation, illustrating that the model sometimes struggles to maintain an overarching understanding of the problem when forming logical symbols. Example 3 highlights a case where GPT-4 struggles to interpret specific
While Logic-LM has proven to be capable sys- tem, can be further improved with extension more flexible and powerful logic systems. For ex- ample, statistical relational learning (SRL) systems such as Markov logic networks (Richardson and Domingos, 2006) and probabilistic soft logic (Bach et al., 2017) have demonstrated great promise in reasoning under uncertainty and integration with our framework would enable even more adaptive problem-solving capabilities. Additionally, our method can be extended reasoning problems requiring commonsense, which remains signifi- cant challenge as they often require reasoning over complex and ambiguous rules.

---

Limitations
and probabilistic soft logic. Journal of Machine Learning Research (JMLR), 18(1):1667.
We identify two main limitations of LOGIC-LM. First, LOGIC-LM relies on translating reasoning problems into logical formats that can be tackled by symbolic solvers. As a consequence, the model's applicability is inherently bounded by the expres- siveness of the symbolic solver, for example, not all problems can be easily encoded in first-order logic. Nevertheless, this limitation can be mitigated by integrating a more diverse set of symbolic solvers. The flexible design of LOGIC-LM facilitates this integration. The wide range of reasoning tasks that we can instantiate our LOGIC-LM framework on shows its general applicability.
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert- Voss. Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz. Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. 2020. Language models few-shot learners. In Proceedings of the Annual Conference on Neural Information Processing Systems (NeurIPS).
Le-Wen Cai, Wang-Zhou Dai, Yu-Xuan Huang, Yu- Feng Li, Stephen H. Muggleton, and Yuan Jiang. 2021. Abductive learning with ground knowledge base. In Proceedings the 30th International Joint Conference on Artificial Intelligence (IJCAI), pages 1315-1821.
Second, LOGIC-LM depends on in-context learning coupled with self-refinement to convert a natural language (NL) problem into the symbolic representation. While this method has proven to be effective, it may face difficulties when dealing with logical representations with intricate grammar structures, such as probabilistic soft logic. This arises from the difficulty in conveying complex grammatical rules to the language model through a limited number of demonstrations within con- strained context size. As a potential solution, future works could explore the development of specialized modules enhance the mapping between NL and symbolic language, e,g. fine-tuning LLMs with synthetic data generated via symbolic solvers.
Wenhu Chen, Xueguang Ma. Xinyi Wang, and William W. Cohen. 2022. Program of thoughts prompting:
Disentangling computation from rea- soning for numerical reasoning tasks. CoRR.
abs/2211.12588.
Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. 2023, Teaching large language models to self-debug. CoRR, Abs/2304.05128.
Peter Clark, Oyvind Tafjord, and Kyle Richardson. 2020. Transformers as soft reasoners over language. In Pro- ceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI), pages 3882-3890.
Ethics Statement
William F Clocksin and Christopher S Mellish. 2003. Programming in PROLOG. Springer Science & Busi- ness Media.
The use of large language models requires signifi- cant amount of energy for computation for training, which contributes to global warming (Strubell et al., 2019). Our work performs few-shot in in-context learning instead of training models from scratch, so the energy footprint of our work is less. The large language models whose API we use for inference, especially GPT-4, consume significant energy.
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian. Jacob Hilton, Retichiro Nakano, Christopher Hesse, and John Schulman. 2021. Training verifiers to solve math word problems. CoRR, 1bs/2110.14168.
Leonardo Mendonça de Moura and Nikolaj S. Bjömer. 2008. 73: an efficient SMT solver. Proceedings of the 14th International Conference of Tools and Algo- rithms for the Construction and Analysis Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pages 337-340.
Ackmowledgements
This work was supported by the National Science Foundation Award #2048122 The views expressed are those of the authors and do not reflect the offi- cial policy or position of the US government.
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer, 2015. The lean theorem prover (system description). In Proceedings of the 25th International Conference on Automated Deduction (ICAD), volume 9195 of Lecture Notes in Computer Science, pages 378-388.
References
Iddo Drori, Sarah Zhang, Reece Shuttleworth, Leonard Tang, Albert Lu, Elizabeth Ke, Kevin Liu, Linda Chen, Sunny Tran, Newman Cheng, et al. 2022. A
Stephen Bach, Matthias Broecheler, Bert Huang, and Lise Getoor. 2017. Hinge-loss markov random fields

---

neural network solves, explains, and generates uni- versity math problems by program synthesis and few- shot learning at human level. Proceedings of the Na- tional Academy of Sciences, 119(32)e2212333)) 19.
Philipp Körner, Michael Leuschel, João Barbosa, Vitor Santos Costa, Verónica Dahl, Manuel V. Hermenegildo, José F. Morales, Jan Wielemaker, Daniel Diaz, and Salvador Abreu. 2022. Fifty years of prolog and beyond. Theory Pract. Log. Progrum., 22(6))776-855 -588..
Herbert B Enderton. 2001. mathematical introduction to logic. Elsevier.
Vipin Kumar. 1992.
Algorithms for constraint- satisfaction problems: survey, Mag.. 13(1)322- 44.
Bruce Frederiksen. 2008. Applying expert system tech- nology to code reuse with pyke. PyCon: Chicago.
Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Gra- ham Neubig. 2023. PAL:: program-aided language models. In Proceedings of the International Con- ference Machine Learning (ICML), volume 202, pages 10764-10799,
Angeliki Lazaridou, Elena Gribovskaya, Wojeiech Stokowiec, and Nikolai Grigorev. 2022. Internet- augmented language models through few-shot prompting for open-domain question answering. CoRR, abs/2203.051 155.
Olga Golovneva, Moya Chen, Spencer Poff. Martin Corredor, Luke Zeu, Maryam Fazel-Zarandi, and Asli Celikyilmaz. 2023, ROSCOE: A suite of metrics for scoring step-by-step reasoning. In Pro- ceedings of the 11th International Conference on Learning Representations (ICLR).
Percy Liang. Rishi Bommasani, Tony Lee, Dimitris Tsipras, Dilara Soylu, Michihiro Yasunaga, Yian Zhang, Deepak Narayanan, Yuhuai Wu, Ananya Ku- mar, Benjamin Newman, Binhang Yuan, Bobby Yan, Ce Zhang, Christian Cosgrove. Christopher D. Man- ning, Christopher Ré, Diana Acosta-Navas, Drew A. Hudson, Eric 7elikman, Esin Durmus, Faisal Ladhak, Frieda Rong. Hongyu Ren, Huaxiu Yao, Jue Wang. Keshav Santhanam, Laurel J. Orr, Lucia Zheng, Mert Yüksekgönül, Mirac Suzgun, Nathan Kim, Neel Guha, Niladri S. Chatterji. Omar Khattab, Peter Henderson, Qian Huang. Ryan Chi, Sang Michael Xie, Shibani Santurkar, Surya Ganguli, Tatsunori Hashimoto, Thomas Icard, Tianyi Zhang, Vishrav Chaudhary, William Wang. Xuechen Li, Yifan Mai, Yuhui Zhang, and Yuta Koreeda. 2022. Holistic eval- uation of language models. CoRR, abs/2211.00 1001100.
Nitish Gupta, Kevin Lin, Dan Roth, Sameer Singh, and Matt Gardner. 2020. Neural module networks for reasoning over text. In Proceedings of the 8th In- termational Conference on Learning Representations (ICLR).
Simeng Han, Hailey Schoelkopf. Yilun Zhao, Zhenting Qi. Martin Riddell, Luke Benson, Lucy Sun, Eka- terina Zubova, Yujie Qiao, Matthew Burtell, David Peng, Jonathan Fan, Yixin Liu, Brian Wong, Mal- colm Sailor, Ansong Ni, Linyong Nan, Jungo Kasai, Tao Yu, Rui Zhang. Shafiq R. Joty, Alexander R. Fab- bri. Wojeiech Kryscinski, Xi Victoria Lin, Caiming Xiong, and Dragomir Radev. 2022. FOLIO: natu- ral language reasoning with first-order logic. CoRR, hts/2209.008400
Bo Liu, Yuqian Jiang, Xiaohan Zhang, Qiang Liu, Shiqi Zhang. Joydeep Biswas, and Peter Stone. 2023a. LLM+P: empowering large language models with op- timal planning proficiency. CORR, abs/2304.11477
Joy He- Yueya, Gabriel Poesia, Rose E Wang, and Noah D Goodman. 2023. Solving math word prob- lems by combining language models with symbolic solvers. CoRR, abs/2304.09110
Hammeng Liu, Ruoxi Ning, Zhiyang Teng, Jian Liu, Qiji Zhou, and Yue Zhang. 2023b. Evaluating the logi- cal reasoning ability of chatgpt and GPT-4. CoRR, abs/2304.03439.
Jie Huang and Kevin Chen-Chuan Chang. 2023. To-
Qing Lyu, Shreya Havaldar, Adam Stein, Li Zhang. Delip Rao, Eric Wong, Marianna Apidianaki, and Chris Callison-Burchh 2023. Faithful chain-of- thought reasoning. CORR, abs/2301.13379.
wards reasoning in large language models: A survey. In Findings of the 61st Anmual Meeting of the Asso- ciation for Computational Linguistics (ACL), pages 1049-1065.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In Proceedings of the 11th International Conference on Learning Represen- lations (ICLR).
Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Sean Welleck, Bodhisattwa Prasad Majumder. Shashank Gupta, Amir Yazdanbakhsh, and Peter Clark. 2023. Self-refine: Iterative refinement with self feedbace... CORR, abs/2303.17651.
Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yu- taka Matsuo, and Yusuke Iwasawa. 2022. Large lan- guage models are zero-shot reasoners. In Proceed- ings of the Annual Conference on Neural Information Processing Systems (NeurIPS).
Robin Manhaeve, Sebastijan Dumancic, Angelika Kim- mig, Thomas Demeester, and Lue De Raedt. 2021. Neural probabilistic logic programming in deep- problog. The Journal of Artificial Intelligence (AIJ). 298: 103504.

---

Jiayuan Mao, Chuang Gan, Pushmeet Kohli, Joshua Tenenbaum, and Jiajun Wu. 2019. The neuro- symbolic concept learner: Interpreting scenes, words, and sentences from natural supervision. In Proceed- ings of the 7th International Conference on Learning Representations (ICLR).
Connor Pryor, Charles Dickens, Eriq Augustine, Alon Albalak, William Yang Wang, and Lise Getoor. 2023, Neupsl: Neural probabilistic soft logic. In Proceed- ings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI), pages 4145-4153.
Danilo Neves Ribeiro. Shen Wang, Xiaofei Ma. Henghui Zhu, Rui Dong, Deguang Kong, Juli- ette Burger, Anjelica Ramos, Zhiheng Huang, William Yang Wang. George Karypis, Bing Xiang, and Dan Roth. 2023a. STREET: A multi-task struc- tured reasoning and explanation benchmark. In Pro- ceedings of the Eleventh International Conference on Learning Representations (ICLR).
Kostas S. Metaxiotis, Dimitris Askounis, and John E. Psarras. 2002. Expert systems in production planning and scheduling: A state-of-the atrt survey. Journal of Intelligent Manufacturing, 1 13(4)2553-26..
Aaron Meurer, Christopher P. Smith, Mateusz. Pa- procki, Ondrej Certík, Sergey B. Kirpichev, Matthew Rocklin, Amit Kumar, Sergiu Ivanov, Jason Keith Moore, Sartaj Singh, Thilina Rathnayake, Sean Vig, Brian E. Granger, Richard P. Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, Fredrik Johans- son, Fabian Pedregosa, Matthew J. Curry, Andy R. Terrel, Stepán Roucka, Ashutosh Saboo, Isuru Fer- nando, Sumith Kulal, Robert Cimrman, and An- thony M. Scopatz. 2017. Sympy: symbolic com- puting in python. PeerJ Computer Science, 103.
Danilo Neves Ribeiro, Shen Wang. Xiaofei Ma, Henry Zhu, Rui Dong, Deguang Kong, Juliette Burger, An- jelica Ramos, William Yang Wang. Zhiheng Huang. George Karypis, Bing Xiang, and Dan Roth. 2023b. STREET: A multi-task structured reasoming and ex- planation benchmark. In Proceedings of the I 11th International Conference on Learning Representa- tions (ICLR).
Reichhrro Nakamo, Jacob Hilton, Suchir Balaji, Jeff Wu. Long Ouyang, Christina Kim, Christopher Hesse, Shantanu Jain, Vineet Kosaraju, William Saunders, Xu Jiang, Karl Cobbe, Tyna Eloundou, Gretchen Krueger, Kevin Button, Matthew Knight, Benjamin Chess, and John Schulman. 2021. Webgpt: Browser- assisted
Matthew Richardson and Pedro M. Domingos. 2006. Markov logic networks. Machine Learning, 62(1- 2):107-136.
John Alan Robinson. 1965. A machine-oriented logic based on the resolution principle. The Journal of the ACM (JACM), 12(1):23 ):23441.
with human feedback.
CoRR, abs/2112.09332.
Abulhair Saparov and Hc He. 2023. Language models are greedy reasoners: A systematic formal analysis of chain-of-thouugt. Proceedings of the 11th In- ternational Conference on Learning Representations (ICLR).
OpenAI. 2023. GPT-4 technical report. CoRR, abs/2303.08774.
Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida. Carroll L. Wainwright, Pamela Mishkin, Chong Zhang. Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welin- der, Paul F. Christiano, Jan Leike, and Ryan Lowe. 2022a. Training language models to follow instruc- tions with human feedback. In Proceedings of the Annual Conference on Neural Information Process- ing Systems (NeurIPS).
Murray Shanahan. 2022. Talking about large language models. CoRR, abs/2212.033511.
Yongliang Shen, Kaitao Song, Xu Tan, Dongsheng Li, Weiming Lu, and Yueting Zhuang. 2023. Hugging- gpt: Solving Al tasks with chatgpt and its friends in huggingface. CoRR, abs/2303. 17580.
Weijia Shi, Sewon Min, Michihiro Yasunaga, Minjoon Seo, Rich James, Mike Lewis, Luke Zettlemoyer, and Wen-tau Yih. 2023. REPLUG: vetrivaal-augmenne black-box language models. CoRR, abs/2301.
Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll L. Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welin- der, Paul F. Christiano, Jan Leike, and Ryan Lowe. 2022b. Training language models to follow instruc- tions with human feedback. In Proceedings of the Annual Conference on Neural Information Process- ing Systems (NeurIPS.
Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao. Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R. Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, Agnieszka Kluska, Aitor Lewkowyzz, Akshat Agarwal, Alethea Power, Alex Ray, Alex Warstadt, Alexander W. Kocurek. Ali Safaya, Ali Tazarv, Alice Xiang, Alicia Par- rish, Allen Nie, Aman Hussain, Amanda Askell, Amanda Dsouza, Ameet Rahane, Anantharaman S. Iyer, Anders Andreassen, Andrea Santilli, Andreas Stuhlmüller, Andrew M. Dai, Andrew La, Andrew K. Lampinen, Andy Zou, Angela Jiang, Angelica Chen, Anh Vuong, Animesh Gupta, Anna Gottardi, Anto- nio Norelli, Anu Venkatesh, Arash Gholamidavoodi,
Lawrence C. Paulson. 1994. Isabelle- A Generic The- orem Prover (with a contribution by T. Nipkow), volume 828 of Lecture Notes in Computer Science. Springer.
David Poole and Alan K. Mackworth. 2010. Artificial Intelligence- - Foundations of Computational Agents. Cambridge University Press.

---

Arfa Tabassum, Arul Menezes, Arun Kirubarajan, Asher Mullokandov, Ashish Sabharwal, Austin Her- rick, Avia Efrat, Aykut Erdem, Ayla Karakas, and al. 2022. Beyond the imitation game: Quantifying and extrapolating the capabilities of language models. CoRR, abs/2206.04411.)
Empirical Methods in Natural Language Processing (EMNLP), pages 89-105.
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. Satisfiability-aides language models using declarative prompting. In Proceedings of the An- nual Conference on Neural Information Processing Systems (NeurIPS).
Emma Strubell, Ananya Ganesh, and Andrew McCal- lum. 2019. Energy and policy considerations for deep learning in NLP. In Proceedings of the 57th
Wanjun Zhong, Siyuan Wang. Duyu Tang, Zenan Xu, Daya Guo, Yining Chen, Jiahai Wang, Jian Yin, Ming Zhou, and Nan Duan. 2022. Analytical reasoning of text. In Findings of the 2022 Conference of the North American Chapter of the Association for Computa- tional Linguistics: Human Language Technologies (NAACI-HLTT), pages 2306-2319.
Annual Meeting of the Association for Computational Linguistics (ACL), pages 3645-3650.
Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021. Proofwriter: Generating implications, proofs, and abductive statements over natural language. In Find- ings of the 59th Annual Meeting the Association for Computational Linguistics (ACL.,, pages 3621-3634.
Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang. Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoe V. Le, and Ed H. Chi. 2023. Least-to-most prompting enables complex reasoning large language models. In Proceedings of the 1 11th International Conference on Learning Representations (ICLR).
Oyvind DafoodT Bhavana Dalvi Mishra, and Peter Clark. 2022. Entailer: Answering questions with faithful and truthful chains of reasoning. In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 2078- 2093.
Jidong Tian, Yitian Li. Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. 2022. Weakly supervised neural symbolic learning for cognitive tasks. In Pro- ceedings of 36th Conference on Artificial Intelligence (AAAI), pages 0896.
Xingyao Wang, Sha Li. and Heng Ji. 2022. Code4struct: Code generation for few-shot structured prediction from natural language. CoRR, abs/2210.12811
Xuezhi Wang. Jason Wei, Dale Schuurmans, Quoc V. Le, Ed H. Chi. Sharan Narang, Aakanksha Chowd- hery, and Denny Zhou. 2023. Self-consistency im- proves chain of thought reasoning in language mod- cls. In Proceedings of the 11th International Confer- ence on Learning Representations (ICLR).
Jason Wei, Yi Tay, Rishi Bommasani, Colin Raffel, Barret Zoph, Sebastian Borgeaud, Dani Yogatama, Maarten Bosma, Denny Zhou, Donald Metzler, Ed H. Chi, Tatsunori Hashimoto, Oriol Vinyals, Percy Liang. Jeff Dean, and William Fedus. 2022a. Emer- gent abilities of large language models. Transactions on Machine Learning Research, 2022.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Ed H. Chi, Quoc Lc, and Denny Zhou, 2022b. Chain of thought prompting elicits reasoning in large language models. CoRR, abs/2201. 1903..
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large lan- guage models. Proceedings of the Annual Con- ference on Neural Information Processing Systems (NeurlPS).
Kaiyu Yang, Jia Deng, and Danqi Chen. 2022. Gen- erating natural language proofs with verifier-guided search. In Proceedings of the 2022 Conference on

---

A
Syntax for First-order Logic (FOL)
C.1 PrOntoQA Prompts
Standard In-Context Learning
Name
FOL Notation
Context:
Jonpuses are not shy. Jonpuses are yunpuses. (+ context here ...) Zumpuses are rompuses. Max is yumpus.
Constant
lowercase letters
Question: following statement false? Max is sour.
Variable
2, y, 2,
Atom
P ,an)
Options:
True B) False
Negation
-P
Pi A P2 PAA," ,PP
correct
Conjunction
Chain-of-Thought Prompting
PVV P2 PVV,,,,VR,
Disjunction
Task Description: Given problen staterent contexts, the task is answer logical reasoning question.
Implication
Ps
Context:
Jonpuses are not shy, Jonpuses are yumpuses. (- more context here m.)) are ronpuses.
Equivalence
Pi ++ Ps
уumpus.
Existential Quantifier
3xP(I,....)
Question: Is the following statement false? Max is sour.
Universal Quantifier
Vr VxP(,....)
Options:
A) True
Table 4: First-Order Logic Grammar.
Reasoning:
is yumpus. Each is dumpus. (-. sore reasoning here ..)
Tunpuses not So Max is not
B Dataset Statistics
The correct option is:
Logic-LM
Dataset
Reasoning
Test Size
#Opts
PrOntoQA
Deductive
500
2
Task Description: You are given problen description and question. The task is to:
ProofWriter
Deductive
600
3
define all the predicates the problen
2) parse the problen into lagic rules based on the defined predicates
FOLIO
FOL
204
LogicalDeduction
CSP
300
3,5,7
3)
the facts mentioned 4) parse the question into the logic forn
problan
AR-LSAT
AR
230
Context: Fach jompus is fruity.
(-.. context here ...)
Table 5: Statistics of the logical reasoning datasets.
Rompuses are zunpuses. Alex is tumpus.
Question:
not shy.
Predicates:
Prompt Examples
Jompus (XSx, bool) :1: Does belong to Janpus? (-. sore predicates here ...).
In this section we provide examples of the prompts used for each dataset and method. Prompts for stan- dard in-context learning contain demonstrations consisting of parts each: context, question, and options. Prompts for chain-of-thought prompt- ing contain demonstrations consisting of parts each: a task description, a context, a question, op- tions, and chain of reasoning. Prompts for Logic- LM contain 2 demonstrations with 5 parts each: task description, context, question, options, and domain-specific symbolic program. For brevity, we show only a single demonstration for each ting the following sections.
Cumpus(V5:) bool) 2:: Does balang zumpus?
Tunpuses (Alex, True)
Rules:
Jompus True) 222 (Fx, True) ( more rules here o.))
Dumpus (15x, True) >>> Rompus (1Sx, True)
Query (Alex, False)

---

C.2 Frier Prompts Standard In-Context Learning
Logic-LM
Description: are given problem description
and question. The task is to:
The соm is blue. The cow 16 round. ( context here -..)
Context:
1) define all the predicates the problen
2) parse the problen into logic rules based on
the cow is cold and the cow visits the 1ion then
the defined predicates
the lion sees the squirrel.
3) write all the facts nentioned in the problen
4) parse the question into the logic forn
Question: Based on the above Infornation, is the fallowing
false, unknown?
Context: Anne is quiet. Erin 1s furry. (+. context here ...)
The tiger is not young.
All red people are young.
options: A) True
Question:
above information,
following statement true, false, or unknown? is
C) Unknawn
The correct option is: B
Predicates:
(5x, bool) 111 Is quiet?
Chain-of-Thought Prompting
Furry($x, bool) Is furry? (- more predicates
..)
White bool] ::: Is white? Young(Sx, bool)
Task Description: Given problen statement contexts, the task answer logical reasoning question.
young?
Facts:
(unne True) 112 Anne qutet. (-.. more facts hare ..1)
Context:
The соm is blue. The con is round. ...)
(-.-
White(Harry, True) Harry white.
the cau is cold and the сaи visits the lion then the lion the squirrel.
Rules:
(5x, True) 355 Furry True) s:: Young people are Turry.
Question: Based en the above information, is the Following statenent true,
unknown?
(-.. rules here ...)
The tigar is not young.
Red($x. True) >>> (Sung(Sx, True) and All red people are young.
Options: True
Whi Le (Anne, True) ::: Anne is white
C) Unknown
Reasoning:
The tiger likes the cow.
The tiger likes the squirrel.
(... more reasoning here ...)
If sonething is nice and it sees the tiger then young.
tiger young.
The option 1s:

---

C.3 FOLIO Prompts
Logic-LM
Standard In-Context Learning
Description:
problen description question. The task is to parse the problen and into first-arder logic forrulas.
Context: All peopla who regularly drink coffee are dependent caffeine.
The gremeer of the first-order logic fornuls is defined follows:
(... nore context here ...)
If Bina is not person dapendent caffeine and
1) legical conjunction: expr1 expr2
person dependent on caffeine and student, or neither a person dependent caffeins nor student.
student,
is
2) lagical disjunction: expr1 expr2
3) lugical exclusive disjunction: expri expr2
4) logical negation: maxpr1
implies expr2: expri exar2
information. is the rollowing statement true, ralse, or uncertain? Rina
Question: Based the
6) exprl and only if expr2: expri + expr2
7) legical universal quantification: V
is person who jakes about being addicted to caffeine unaware that caffeine drug.
8) logical existencial quantification:
Output fornat: logic form ::: description
Options: True
Context: All people who regularly drink coffee are dependent caffeine.
A)
B) False
(-.. more context here ...)
C)
If Rina is not person dependent on caffeine and student,
person dependent on caffeine and student, or neither person dapendent caffaine
is
option
Chain-of-Thought Prompting
Question: Based the above information, the following statement true, false, uncartain? Rina is either person who jokas about being unaware caffeine
Task Description: Given a problen statement as logical reasoning
contexts, the task question.
is a drug.
company Building comnercial warehouse listed on the National Register Historic (-.. more context here ...)
Context:
The Blake
Predicates:
Dependent(1) x 1s person dependent on caffeine (- predicates ...)
Student(x) 11: is student
John works the Ennet Building.
Prenises:
Question: Based en the above information, is the fallowing statement true, The Blake Hcfall Company building is located in Portland, Oregon.
Yx (Drinks(x) Dependent All people who regularly drink coffee are dependent on caffeine.
unsertain?
(-.. premises here ...).
VX (Jokes + -Unaware s:: No one who lokes addicted caffeine that caffeine 1s a drug.
Options:
A) True
8) False
C)
Conclusion:
Jokes (rina) @ Unoware(rina) t:: Rina is either
Reasoning:
The Blake NcFall Company But Buinding another name for the Ennet Building.
person jokes being addicted caffeine or 1s unaware that caffeine is drug.
(-.. reasoning here ...)
Therefore,
Company Building
located in Portland, Oregon.
The correct option Is: A

---

C.4 LogicalDeduction Prompts
Logic-LM
Standard In-Context Learning
Description: You are given problem description. The task is to parse the problen as constraint satisfaction problen, defining the domain, variebles, and contruints.
Context:
The nolloxing paragraphs each describe objects arranged fixed order. (-.- more context here ...)
set
Eve. finished balow Ada. Rob finished below Joe.
Context: The following paragraphs each describe set of three abjects arranged in fixed order. (---
Question: Which of the Following is true?
here ...) The minivan is newer than the convertible.
Options:
finished third.
Question: Which the Folloning is true?
Eve rintshed third.
C) Ada finished third.
Options:
finished third.
A) The station wagon is the recond-newest is C) The ninivan is the second -newest.
F) 8ob finished third.
() finished third.
6) loe finished third.
Donain:
correct option
1: oldest
newest
Chain-of-Thought Prompting
Variables: station' _agen [IN] [1, 2, 3] convertible [IN] [1,
Task Description: Given a problen statement as contexts. the
logical reasoning
minivan [IN] [1, 3]
question.
Constraints:
Context:
The fallaxing paragraphs each describe a set five objects orranged in fixed order. (-.. more context ...)
station'..wgoo =* ::: The station wagon is the aldest. ninivan convertible ::: The minivan is newer than the convertible.
The raven is the third from the left.
convertible, minivan]) ::: All vehicles have diffarent values.
Question: Which of the fallowing is true?
Options:
The quall is the rightmost.
the rightnost.
A) station', wagon Maagon
2 ::: The station wagon is the
() The raven is the rightnost.
sacona newwstt.
rightnost.
tible ::: convertible
E) The robin is the rightnost.
second newest. ninivan
The ninivan second
Reasoning:
The oel is the leftmost. This neans uwl not the rightmost.
(-.- reasoning .er)
This neans raven is alse not the rightnost.. So, The quail is rightmost.
the
The correct option 1s:

---

C.5 AR-LSAT Prompts
Logic-LM
Standard In-Context Learning
Description: You are given problem description. The task is to parse the problen as constraint satisfaction problen, defining the domain, variebles, and contreints.
Context:
During strgle week, from Monday through Friday, tours will conducted of company three divisions; Operations, Production, and
Salas. Exactly five tours will be conducted one
Context:
travel nagazine has hired six Interns Farber, Gombarick, Hall, Jackson, Kanze, and assist covering Romanta, Spain, and Tuscany. (- more context here ..)) Jackson is assigned to Tuscany. Kanze is not assigned Spain.
day. (-.- ...) If the Operations division toured on Thursday, then the Production division is toured Friday.
stories:
Question:
Which one of the follewing CANNOT be true s schedule?
Question: Which one of the following interns CANNOT be assigned Tuscany?
Options:
A) The division that is toured on Honday alse
Options:
toured on Tuesday.
(A) Farber
division that
Nonday
(B) Gonbarick
toured on Friday.
division that is
Tuesday
(D) Kanze
toured on Thursday.
The division that is toured Wednesday also
toured on Friday.
Declarations: stories Enunsort (L Spain, Tuscany
E) The division that is toured on Thursday is also toured Friday.
assistants Enumsart ([phhtorrrphtt writer]] (--- declarations ...).
option
trainad Funstton([interns]] +> [assistants])
Constraints:
Chain-of-Thought Prompting
trained the same Conbarick and trained(Farber) != trained ::: farber and will trained in different fields ( sore contraints here ..))
(rained(Gombarrrt -* trained(Lhs)
Lha
Task Description: Given a problen statement as contexts, the task
logical reasoning Salas. Exactly fiva tours will be conducted that week, each (-.. context here
question.
(Jackson)))
Tuscany Jackson is assigned
During single week, Monday through. Friday, tours will be conducted of comрany s three divisions: Operations, Production,
to Tuscany
assigned (Kanze) Spain
Kanze is not assigned
to Spain
Options:
Thursday. Operations division toured Production division is
..-)
is_unsat (assigned == Tuscany) ::: (A)
is_unsat [d_uunat (GennbeiiG н* Tuscany)
toured on Friday.
is_unsat (aansaatassiganna (aes)
Tuscany) 11: (E)
is_unsat (assigned (Kanze))) == Tuscany) (B)
Question: Which one of the follewing CANNOT be true of the week's 's tour schedule?
is_unsat (asiingnsgg Tuseany) ::: (E)
Options:
The division
Honday The division that toured Honday also
is
D Result Interpreter Implementation
toured on Tuesday.
toured on Friday.
For PrOntoQA and ProofWriter, the Pyke logic programming engine returns the inferred value of the variable in the query or Unknown if the variable cannot be determined. For example, for the query ConductÉlectricityy (Nail,,, x), Pyke may return x =True. By comparing with the goal statement ConductElectrictt (Nail, False), we can know that goal to be proved is False. For FOLIO, the FOL inference engine directly turns the veracity label of the goal ENTAILMENT, CONTRADICTION, and CONTINGENT, which can be mapped to True, False, and Unknown, respectively. For LogicalDeductton, the solver returns all the possible value assignments an array. We write rules to parse cach option into the corresponding value and check it is in the generated array. For AR- LSAT, we attempt to separately prove each option to find the correct answer.
C) The division that is taured on Tuesday is also toured Thursday.
D) The division that is toured on Wednesday is also toured Friday.
F) The division that is taured on Thursday is also toured Friday.
Since Thursday and Friday already have planned, only Honday, Tuesday and Rednesday tours need to be determined.
Reasoning:
reasoning ...)
A different division is taured on Thursday. Therefore, the final
is
The correct option is:
E Example Generations of LOGIC-LM

---

Example 1
There are six types wild turkeys: Eastern wild turkey, osceola wild turkey, Gould's wild turkey, Herrias's wild turkey, Rie Grande Mild turkey, and Ocollated kild turkey. Toe is not an Easten: wild turkey. Tor is not an Osceola wild turkey, Tox is also not Gould's wild turkey, or Narric Lan't wild turkey, on sio orande wlld tursey, Tan is a wild turkey. Question: Based on the above information, is the following statement true, false, on uncertain? Ton is an Ocellated wild turkey.
Probles:
(A] True
(8) False
(C) Uncertain
Predicted logic prograns:
Premises:
hoyfeore weweeeetrttteeeeeee -n det hoydeeolddddd Vx (0 (collatsohilafukkey(3 v EsttemMllouunee(e) @ccoolaMildfurloy(ss) Gouldsndld (1) Nerriansdiddarkkyyy
Rlotinandwwi lsturkey(ss))
wildfurkaytten #astsmmiillurrryytee (arc x -doullsii1d/uuraayttee wwwrriaassaldduureeyye
okloGramdeel (sTurkeytoo))
Conclusion:
Dcellatedkiloffrkeytte
Predicted answer:
Example
Probles: Japanese gane company created the gase the Legend Zelds, All gawes in the Top 18 List are mode by Jopanese game compantes. game sells nore than one ailllion coples, then will be selected into the Top 18 1ist. The Logend of Zelda sold nora than one millloon copies. Question: Based on the above information, is the Following statement true, faise, on uncertain? The Lagend of Zelca is In the Top 18 1ist. (A) True
(8) False
(C) Uncertain
Predicted logic programs::
Premises: IaganeseSavetoeppryytt Conpreerreereppyeeeeeeee. zelda)
vv. (Top18L1st(0) Iggaesstaaecooomn(ee)
vi tael (onnopptttt) (op1oList((H)
Sel innertannnelllleeoooooeee _eeeed)
Conclusion:
Tool@List(legemdddoo
Predicted answer:
Example 3
lowing paragraphs
onjectss arranged
logically
paragraph. golf tountavent,
five golfers: Rob, Eve, El1, Any,
Dan finished second, Any finished Eve. Dan
Question: Which followiing true?
(A) Finished third
(B) Eve Finished third
(D) Any Finished third
(E) Don Finished third
Predicted logic prograns:
Domsin:
Variables:
Constroints:
1: first
Rob [TM] [1, 2, 4, 5]
Dan
Eve
E11 [DN]
[1, 2, 3, 4, 5]
Sua Dan < Eve
[10]
5]
8li
Gan [1M]
[3,
2,
4,
allliffeeetiontrriin((eeee Eve, E15, Any, Dan))
Rob
Eve
E11
(E)
Predicted answer:
Example 4
Problem: If the restaurant is Histed in velp's recomendation, then the restaurant does not receive man negetive revimus. All restaurents with a rating greater than are listed in velp's reconmentationss Sone restaurants that do not provide take-out service receivv nany negative reviews. all restaurants that are popular anong local residents have ratings greater than Subway has rating greater than or 15 popular asong local residents.
Question: Based the above information, is the rollowing statenent true, false, on uncertain? Subway provides take-out service and does not receive eany negative reviows.
(b) True
False
(C) Uncertain
Predicted logit programs:
Premises:
(Listed(s) -Nopttiooevieesss)
wM-(Aacingixx Listodings
(SreaterTanttie(()) Listed(x))
(=Takedutt>) Neputiveetvvenn(()))
(Popular(x) (Ratingss, y) y 9)) (Pogular(x) Gresterthanttne(())
Rating(sumayy y) >->-- Popular(sumway) GreaterThantinesuuaon Popular(subary)
Conclusion:
(subwa)) (Nopstiveeecttocsssuaa))
Predicted answer: C
Figure 6: Examples of generated symbolic representations and predicted answers. The incorrect segment(s) and their correspondence the problem are marked in red, and the correct revisions are marked green.


Reviews:
[{"review_id": "uhW4JBZHxc", "reviewer": "Reviewer_TXB8", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": 4, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the valuable insights behind the comments and also want to clarify a few points. \n\n> *The experiments can be further improved by adding necessary compared methods. Are there no few-shot methods/approaches for logical reasoning tasks? What if using some off-the-shelf text-to-symbolic formulator? Or what would be the performance of trained small models on these datasets?*\n\nThanks for the reviewer's suggestions. In the Related Work section (Lines 144-155), we clarified why traditional neuro-symbolic methods were not included for comparison. These methods: 1) rely on hand-crafted or specialized module designs which are hardly generalizable to other datasets, and 2) they often require large numbers of training data, making them unsuitable for few-shot settings, which is our focus. For this reason, we chose to compare Logic-LM with modern LLMs, such as GPT-4 and GPT-4 + CoT, which are more generalizable and powerful baselines. \n\nRegarding off-the-shelf text-to-symbolic formulators, existing models mainly target SQL or SPASQL formats, which are not applicable to the logical reasoning tasks we study. As far as we're aware, no pre-trained formulators exist for the symbolic languages like FOL, logical programming, or CSP that we employ. This led us to define our own symbolic grammar and use in-context learning for formulation. \n\nWe appreciate the reviewer's suggestion on comparing with trained small models. In response to this, we conduct additional experiments on fine-tuning FLAN-T5-XL model to compare with Logic-LM. For a fair comparison, we fine-tune FLAN-T5 on the same $N$ few-shot examples we used in the Logic-LM prompt. The results are shown in the table below. \n\n| Method / Dataset      | ProntoQA | ProofWriter | FOLIO | LogicalDeduction |\n| --------------------- | -------- | ----------- | ----- | ---------------- |\n| FLAN-T5-XL (N=2)      | 49.80    | 34.17       | 34.31 | 28.33            |\n| FLAN-T5-XL (N=50)     | 50.80    | 35.33       | 36.76 | 31.67            |\n| Logic-LM (w. GPT-3.5) | 93.20    | 70.11       | 61.76 | 67.66            |\n\nWhen trained with the same number of few-shot examples (N=2), it's hard for FLAN-T5 to learn anything useful, with performance close to random guessing across all datasets. Therefore, we relax the constraint by using $N=50$ in-domain examples for training. While this led to some performance improvement, FLAN-T5-XL still lagged significantly behind Logic-LM. These results demonstrate the superior data efficiency and effectiveness of applying in-context learning for problem formulation.  We will include these additional results and findings in the camera-ready version. \n\n---\n\n> *I appreciate the authors' efforts on curating specific symbolic language grammar for specific type of reasoning task. When conducting experiments, will Logic-LM be prompted with the correct few-shot examples using the most effective grammar? Would that be considered as a data leakage, as in the real-world setting models can never know the exact type of reasoning task and prepare the best few-shot example with best grammars?*\n\nThanks for asking this question. In our experiments, the grammar for each dataset was predetermined, since we primary focus on accurate problem-to-symbolic-form translation. As an experimental setting, we don't think this is data leakage because it aligns with the premises of few-shot learning where some domain-specific information is assumed to be known. This is analogous to the Chain-of-Thought method, where LLMs are prompted with a few in-domain examples, together with human annotated correct reasoning chains. In Logic-LM, we provide a few correct symbolic formulations, which can be regarded as correct reasoning chains written in symbolic language. \n\n**Additional Experiments**. However, we agree with the reviewer's point that automatically selecting an appropriate symbolic system is an important practical concern. To address this, we conducted an additional experiment to evaluate the potential of using LLMs as grammar designators. We prompted GPT-4 with 8 demonstrations, each consisting of a problem and its corresponding symbolic language, such as `(Problem from FOLIO, \"FOL representation\")`. These demonstrations were randomly drawn from each of the four datasets we used (two examples per dataset).  Subsequently, we evaluated GPT-4's performance on the grammar designation task to assign new examples to the appropriate symbolic grammar (3-class classification since we have defined three different grammars). Out of 400 randomly sampled test cases (100 from each dataset), GPT-4 achieved a high F1 score of 96.5%. However, we note that this high performance may partially due to the fact that the problems of the four datasets we used are easy to differentiate. In real-world applications, determining the most fitting symbolic system could be more challenging. We will include these new findings and discussions in a discussion section of the camera-ready version. We thank the reviewer for raising this interesting and valuable question. \n\n---\n\n> *I suggest to put Sec 3.2 as a subsection of Sec 3.1. Also Section 3.4 can be aggregate into Sec 3.1. Then Section 3 will have three subsection, each corresponding to one technical component of the propose approach. Now, it is a bit confused to have Symbolic Language Grammar and Self-Refiner, parallel to the three components.*\n\nWe agree with the reviewer's suggestion to reorganize Section 3 into three sub-sections—Problem Formulator, Symbolic Reasoner, and Self-Refiner—which align more coherently with the general framework illustrated in Figure 1. This restructuring will provide a clearer presentation of each technical component of our proposed approach, thereby improving the paper's readability and logical flow. We appreciate this insightful recommendation and will implement it in the final version.", "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": "- The idea of utilizing symbolic reasoner to help LLM resolver logical reasoning is making sense, to achieve both accuracy in terms of reasoning results and generality of understanding various logical queries. \n- The motivation to design three stages or technical components for the overall approach is well explained. LLM is mainly serve as a interpreter to translate text into symbolic formulas, and translate the symbolic results into textual answer.", "reasons_to_reject": "- The experiments can be further improved by adding necessary compared methods. Are there no few-shot methods/approaches for logical reasoning tasks? What if using some off-the-shelf text-to-symbolic formulator? Or what would be the performance of trained small models on these datasets?\n- I appreciate the authors' efforts on curating specific symbolic language grammar for specific type of reasoning task. When conducting experiments, will Logic-LM be prompted with the correct few-shot examples using the most effective grammar? Would that be considered as a data leakage, as in the real-world setting models can never know the exact type of reasoning task and prepare the best few-shot example with best grammars?", "questions_to_authors": "", "paper_topic_and_main_contributions": "The paper studies logical reasoning task problems. The proposed approach is a tool-augmented LLM. \nLLM struggles in making correct reasoning. With the help of specialized symbolic reasoners, LLM can deliver more faithful results on logical reasoning tasks.", "excitement": 3, "reproducibility": 4, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {"Typos_Grammar_Style_and_Presentation_Improvements": "- I suggest to put Sec 3.2 as a subsection of Sec 3.1. Also Section 3.4 can be aggregate into Sec 3.1. Then Section 3 will have three subsection, each corresponding to one technical component of the propose approach. Now, it is a bit confused to have Symbolic Language Grammar and Self-Refiner, parallel to the three components."}}, {"review_id": "bMPR2FEPrM", "reviewer": "Reviewer_Yhix", "summary": "", "questions": "1. what is the performance of proposed Logic-LM on Entailmentbank dataset? How is it compared to \"Standard\" and \"COT\"?\n2. what if \"Standard\" and \"COT\" use self-refinement to directly solve the original problems?\n3. what can I learn from this paper given my previous analysis of this paper?", "limitations": "", "rating": 3, "confidence": 4, "soundness": 3, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "> *The adopted datasets are not persuading to be used by this paper to form its conclusions. Because every data in the four datasets is generated from symbolic reasoner and tranfered to synthetic natural language.* \n\nWe want to clarify that FOLIO is not a dataset automatically generated with symbolic reasoner. FOLIO is an expert-written dataset for FOL reasoning equipped with parallel FOL formulas. The examples are aligned with real-world knowledge and use highly natural wordings. They asked the annotators to create new FOL problems from scratch, using Wikipedia articles to develop ideas for topics (please refer to Section 3.1 of the FOLIO paper). They also use a hybrid of automatic generation and manual annotation. In this case, only the problem template is automatically generated. Human annotators are asked to create problems based on the template. Therefore, FOLIO is clearly not a \"synthetic dataset automatically generated with symbolic reasoner\". \n\n---\n\n> *However, if the method of this paper can work on any dataset that is not automatically generated with symbolic reasoner, I probably would agree that it is a good work.*\n\nAlthough we don't agree that all datasets used in this paper are automatically generated with symbolic reasoner, we appreciate the reviewer's point that evaluating on more real-world datasets could make our work more convincing. Therefore, we present additional experimental results on two realistic human-created datasets: GSM8K and AR-LSAT.\n\n**Datasets**\n\n- GSM8K [1] contains 8.5K high-quality mathematical logic reasoning problems, crafted by human experts. For our evaluation, we use the test set, containing 1,319 questions. \n- AR-LSAT [2] collected all analytical logic reasoning questions from the Law School Admission Test from 1991 to 2016. We use the test set which has 231 multiple-choice questions. \n\n**Symbolic Language and Reasoners.**  For GSM8K, we employ *SymPy*, a Python library specialized in symbolic mathematics, to serve as the symbolic reasoner. For AR-LSAT, we utilize the *Z3 theorem prover* as the symbolic reasoner. Below, we provide examples of questions from each dataset, along with their corresponding symbolic representations. \n\n**GSM8K: Problem**\n\n```\nQuestion: Olivia has $23. She bought five bagels for $3 each. How much money does she have left?\n```\n\n**GSM8K: symbolic formulation**\n\n```python\n# Variables\nMoney_of_Olivia = 23 # Olivia has $23\nEach_Bagel_Price = 3 # Each bagel is $3\nNum_Bagel_Olivia_Bought = 5 # Olivia bought five bagels\n\n# Query\nMoney_of_Olivia - Each_Bagel_Price * Num_Bagel_Olivia_Bought # How much money does she have left?\n```\n\n**AR-LSAT: Problem**\n\n```\nAs part of an open house at a crafts studio, three teachers—Jiang, Kudrow, and Lanning—will give six consecutive presentations on six different subjects. Jiang will present on needlework and origami; Kudrow on pottery, stenciling, and textile making; and Lanning on woodworking. The order of their presentations will meet the following conditions: Kudrow cannot give two presentations in a row. The presentation on stenciling must be given earlier than the one on origami. The presentation on textile making must be given earlier than the one on woodworking.\n\nIf textile making is presented fifth, which one of the following could be true?\nA) Needlework is presented sixth.\nB) Pottery is presented fourth.\nC) Stenciling is presented second.\nD) Stenciling is presented third.\nE) Woodworking is presented second.\n```\n\n**AR-LSAT: symbolic formulation**\n\n```python\n# Variables and functions\nSubjects = [needlework, origami, pottery, stenciling, textile_making, woodworking]\nTeachers = [Jiang, Kudrow, Lanning]\nPosition = Function(Subjects -> bool)\n\n# Constraints\nForAll([sub IN Subjects], And(position(sub) >= 1, position(sub) <= 6)) # each position should be from 1 to 6\nForAll([s_1, s_2], Implies(s_1 != s_2, position(s_1) != position(s_2))) # each subject should be assigned a different order\nteach(needlework) == Jiang # Jiang will present on needlework\nteach(origami) == Jiang # Jiang will present on origami\nteach(pottery) == Kudrow # Kudrow will present on pottery\nteach(stenciling) == Kudrow # Kudrow will present on stenciling\nteach(textile_making) == Kudrow # Kudrow will present on textile making\nteach(woodworking) == Lanning # Lanning will present on woodworking.\nposition(textile_making) == 5 # textile making is presented fifth.\nposition(stenciling) < position(origami) # The presentation on stenciling must be given earlier than the one on origami.\nposition(textile_making) < position(woodworking) # The presentation on textile making must be given earlier than the one on woodworking.\nForAll([s_1, s_2], Implies(And(teach(s_1) == Kudrow, teach(s_2) == Kudrow, s_1 != s_2), And(Not(position(s_1) == position(s_2) - 1), Not(position(s_2) == position(s_1) - 1)))) # Kudrow cannot give two presentations in a row.\n\n# Query\nposition(needlework) == 6 # A) Needlework is presented sixth.\nposition(pottery) == 4 # B) Pottery is presented fourth.\nposition(stenciling) == 2 # Stenciling is presented second.\nposition(stenciling) == 3 # Stenciling is presented third.\nposition(woodworking) == 2 # Woodworking is presented second.\n```\n\n**Main Results.** The results of Logic-LM (without self-refinement) and the baselines are given in the table below. Consistent with Table 3 in our paper, *Exe_Rate* means the percentage of executable symbolic representations, and *Exe_Acc* means the accuracy of the executable samples. We use the same set of in-context examples for Standard, CoT, and Logic-LM for fair comparison. \n\n|          |           | GSM8K     |           |           | AR-LSAT   |           |\n| -------- | --------- | --------- | --------- | --------- | --------- | --------- |\n|          | GPT-3.5   | ChatGPT   | GPT-4     | GPT-3.5   | ChatGPT   | GPT-4     |\n| Standard | 23.95     | 15.77     | 43.32     | 20.34     | 22.51     | 33.33     |\n| CoT      | 65.04     | 60.72     | 90.36     | 17.31     | 22.51     | 35.06     |\n| Logic-LM | **69.59** | **64.44** | **91.04** | **21.64** | **30.73** | **45.45** |\n| Exe_Rate | 90.9%     | 95.22%    | 99.7%     | 24.24%    | 21.21%    | 31.17%    |\n| Exe_Acc  | 71.33     | 66.16     | 91.01     | 33.93     | 46.93     | 65.28     |\n\nWe find that Logic-LM without self-refinement surpasses both Standard and CoT prompting on both datasets across all tested models, including GPT-3.5, ChatGPT, and GPT-4. In the case of the GSM8K dataset, a high *Exe_Rate* is observed, suggesting that the majority of problems within this dataset can be represented as SymPy programs — even though the questions were not originally generated using symbolic reasoners. Conversely, while the *Exe_Rate* for AR-LSAT is somewhat lower, we find that the *Exe_Acc* is significantly greater than that achieved using CoT. This implies that the integration of a symbolic solver, such as Z3 in this case, considerably enhances the model's logical reasoning capabilities when problems can be translated into symbolic language. We argue that these findings, when considered in conjunction with real-world datasets like GSM8K and AR-LSAT, compellingly demonstrate the efficacy of augmenting LLMs with symbolic solvers. \n\n- [1] Zhong et al., AR-LSAT: Investigating Analytical Reasoning of Text. NAACL, 2022.\n- [2] Cobbe et al., Training Verifiers to Solve Math Word Problems. 2021. \n\n---\n\n> *It is very improper to use these four datasets, and transfer their data back to symbolic language to be solved by symbolic reasoner to illustrate the power of symbolic reasoner.*\n\nIn general, we believe studying whether LLMs can transfer these real-world problems into appropriate logical forms is an intriguing direction to explore. There are many related areas for this such as NL-FOL translation, NL-SQL translation, and semantic parsing. In this work, we explore in-context learning as the NL to Logic language translator. \n\nHowever, we understand the reviewer's concern that transferring a synthetically created dataset back to the symbolic language does not show the effectiveness of our method. Therefore, in the previous replies, we have: 1) clarified that FOLIO is not an automatically created logical reasoning dataset, and 2) demonstrated the effectiveness of LogicLM on two real-world datasets purely created by human experts (GSM8K and AR-LSAT). We hope these could address the reviewer's concern. \n\n---\n\n> *The performance comparison is established in an unfair experiment --- Logic-LM can use self-refinement to refine the transferred symbolic language, then why \"Standard\" and \"COT\" can't use self-refinement as well to directly solve the original problem? What if \"Standard\" and \"COT\" use self-refinement to directly solve the original problems?*\n\nWe are afraid that this is a misunderstanding. In our Logic-LM model, self-refinement is possible because the symbolic reasoner serves as a feedback mechanism, allowing the model to self-correct based on error messages. This enables the model to refine its generated logic formulations iteratively. \n\nConversely, \"Standard\" and \"CoT\" models lack an analogous feedback mechanism during the inference stage. Once these models produce an answer, there's no clear way to validate its correctness, leaving us without a clear path for correction. Differently, in Logic-LM, the error message from symbolic solver provides a clear feedback signal for whether the symbolic form is correct and what error it contains. This demonstrates another advantage of incorporating a symbolic solver into Logic-LM: it not only enhances reasoning but also facilitates self-refinement through automated feedback. \n\nOne way we could implement self-correction for \"Standard\" and \"COT\" is to use an external model as the feedback model. Existing methods like Self-Refine [3] and Reflexion [4] use the LLM itself for feedback. After generating an answer, the model is prompted with a question such as, \"Is this answer/reasoning correct?\" If the model replies \"no,\" it attempts to generate a new answer. However, this is inherently limited by the model's own capabilities. If the LLM cannot solve a particular problem, it is unlikely to accurately assess the correctness of its own answers or reasoning for that problem. \n\nIt is also feasible to use an external model to verify the plausibility of each reasoning step, but this introduces a new set of challenges. Verifying the correctness of language-based reasoning is a complex and as-of-yet unresolved research issue. In contrast, the logic language enables more straightforward and reliable validation. \n\nGiven the discussions above, incorporating self-refinement is inherently more applicable to Logic-LM than to the \"Standard\" and \"CoT\" models. Nonetheless, in response to the reviewer's suggestion, we conducted an additional experiment where the LLM itself serves as the feedback model. Consistent with our expectations, this approach resulted in only marginal performance changes on the FOLIO dataset, as detailed in the table below. \n\n| Language Model | Without Self-refinement | With Self-refinement |\n| -------------- | ----------------------- | -------------------- |\n| GPT-3.5        | 57.84                   | 58.33                |\n| ChatGPT        | 57.35                   | 57.84                |\n| GPT-4          | 70.58                   | 70.09                |\n\nMoreover, even without self-refinement, Logic-LM outperforms \"Standard\" and \"COT\" by an obvious margin on GSM8K and AR-LSAT, as shown by our additional results in the previous reply. \n\n- [3] Madaan et al., 2023. Self-refine: Iterative refinement with self-feedback. \n\n- [4] Shinn et al., 2023. Reflexion: Language agents with verbal reinforcement learning. \n\n---\n\n> *What is the performance of proposed Logic-LM on Entailmentbank dataset? How is it compared to \"Standard\" and \"COT\"?*\n\nEntailmentbank is a question-answering dataset that focuses on multi-hop, commonsense reasoning and explanation generation.   However, our paper is focusing on enhancing LLM's ability in solving logical reasoning problems. Therefore, evaluating on Entailmentbank seems out of the scope of this paper. As we admitted in the limitation section, Logic-LM relies on translating reasoning problems into logical formats that can be tackled by symbolic solvers. As a consequence, the model’s applicability is inherently bounded by the expressiveness of the symbolic solver. There are certainly problems that cannot be encoded as logical forms, such as the questions in Entailmentbank. Despite this limitation, the value of integrating symbolic solvers with LLMs should not be discounted. We have already showcased the efficacy of Logic-LM across three real-world datasets: FOLIO, GSM8K, and AR-LSAT. Furthermore, the diversity of existing symbolic solvers—including tools for symbolic mathematics, theorem proving, and logic programming—provides a broad range of utilities that significantly enhance the logical reasoning capabilities of LLMs. \n\n---\n\n> *What can I learn from this paper given my previous analysis of this paper?*\n\nWhile we can't determine what the reviewer has learned from our paper, we believe that addressing the reviewer's concerns with our previous replies should clarify the significance of our contributions. To succinctly outline these: 1) We pioneered the integration of symbolic solvers with LLMs using in-context learning for tackling logical reasoning tasks, 2) We developed Logic-LM, a flexible and effective framework for harmonizing various types of symbolic solvers with LLMs, thereby augmenting their logical reasoning capabilities, 3) We explored the self-refinement mechanisms within LLMs for improving logical forms, and 4) We established a foundation with Logic-LM that we anticipate will inspire future neuro-symbolic research, bridging modern LLMs with traditional symbolic logic.", "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": "1. A through analysis on the performance of transfering synthetic natural language back to logic language and solve it with symbolic solver.", "reasons_to_reject": "1. The adopted datasets are not persuading to be used by this paper to form its conclusions. Because every data in the four datasets is generated from symbolic reasoner and tranfered to synthetic natural language. The goal the the four datasets is to analyze the existing LMs' ability on logical reasoning on natural language. It is very improper to use these four datasets, and transfer their data back to symbolic language to be solved by symbolic reasoner to illustrate the power of symbolic reasoner. However, if the method of this paper can work on any dataset that is not automatically generated with symbolic reasoner, I probably would agree that it is a good work. An example is Entailmentbank [1]. However, I have not seen this paper working on similar datasets.\n2. The performance comparision is established in an unfair experienment --- Logic-LM can use self-refinement to refine the transfered symbolic language, then why \"Standard\" and \"COT\" can't use self-refinement as well to directly solve the original problem? I don't think any number in table 2 is persuading. \n3. It is hard to learn anything from this paper because of my previous reaons.\n\n\n[1] Dalvi, B., Jansen, P., Tafjord, O., Xie, Z., Smith, H., Pipatanangkura, L., & Clark, P. (2021). Explaining answers with entailment trees. arXiv preprint arXiv:2104.08661.", "questions_to_authors": "1. what is the performance of proposed Logic-LM on Entailmentbank dataset? How is it compared to \"Standard\" and \"COT\"?\n2. what if \"Standard\" and \"COT\" use self-refinement to directly solve the original problems?\n3. what can I learn from this paper given my previous analysis of this paper?", "paper_topic_and_main_contributions": "This paper takles logical reasoning problems by transfer four existing synthetic natural language datasets (where each data in the datasets is generated automatically by transfering symbolic reasoner generated symbolic sentences to synthetic natural language sentences) back to symbolic sentences and solve it with symbolic reasoner. This paper tries to indicate that in this situation using a symbolic reasoner can achieve better performance than using LM to directly solve the synthetic natural language tasks.", "excitement": 3, "reproducibility": 4, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "2EODHykfww", "reviewer": "Reviewer_udfF", "summary": "", "questions": "1. The benefit of Logic-LM over CoT is clear for the highest reasoning depths, but when reasoning depth is lower, to what extent does Logic-LM improve over CoT? Is it possible that the failure rate of the translation (as shown in Fig. 6) ends up being worse than the failure rate of CoT logical errors (as ther is only one step of reasoning)?\n\n2. The four datasets you test on are still rather synthetic datasets. How do you envision your Logic-LM approach to apply in more complex and real-world applications? ", "limitations": "", "rating": 4, "confidence": 4, "soundness": 4, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the valuable insights behind the comments and also want to clarify a few points.\n\n> *The first order logic representation used may be somewhat complex and difficult for someone to understand if they need to go in and debug the full pipeline, compared to the explanation generated by chain of thought.*\n\nWe appreciate the reviewer's concern regarding the explainability of our neuro-symbolic approach in Logic-LM. While it's true that methods like chain-of-thought offer better natural language explainability, our primary focus in this paper is on enhancing the **faithfulness** of LLMs in logical reasoning. The use of symbolic language, although less interpretable, provides a more precise and verifiable form of reasoning. \n\nTo strike a balance between faithfulness and explainability, we have made some initial efforts. Specifically, we prompt Logic-LM to generate both the symbolic formula and its corresponding natural language explanation (as mentioned in Line 297). This not only helps in better grounding of the symbolic language but also offers users a level of explainability. Looking ahead, we see ample opportunity to further improve Logic-LM's explainability. One promising direction could involve introducing a *Reasoning Explanation* module designed to translate the symbolic solver's reasoning path into easily understandable natural language. We will add this discussion into the future work section. We appreciate the reviewer highlighting this important aspect.\n\n> *The four datasets you test on are still rather synthetic datasets. How do you envision your Logic-LM approach to apply in more complex and real-world applications?*\n\nThanks for pointing this out. We agree with the reviewer's point that we should evaluate on more real-world datasets. Therefore, we present additional experimental results on two realistic human-created datasets: GSM8K and AR-LSAT.\n\n- GSM8K [1] contains 8.5K high-quality mathematical logic reasoning problems, crafted by human experts. For our evaluation, we use the test set, containing 1,319 questions. \n- AR-LSAT [2] collected all analytical logic reasoning questions from the Law School Admission Test from 1991 to 2016. We use the test set which has 231 multiple-choice questions. \n\nFor GSM8K, we employ *SymPy*, a Python library specialized in symbolic mathematics, to serve as the symbolic reasoner. For AR-LSAT, we utilize the *Z3 theorem prover* as the symbolic reasoner. The results of Logic-LM (without self-refinement) and the baselines are given in the table below. \n\n|          |           | GSM8K     |           |           | AR-LSAT   |           |\n| -------- | --------- | --------- | --------- | --------- | --------- | --------- |\n|          | GPT-3.5   | ChatGPT   | GPT-4     | GPT-3.5   | ChatGPT   | GPT-4     |\n| Standard | 23.95     | 15.77     | 43.32     | 20.34     | 22.51     | 33.33     |\n| CoT      | 65.04     | 60.72     | 90.36     | 17.31     | 22.51     | 35.06     |\n| Logic-LM | **69.59** | **64.44** | **91.04** | **21.64** | **30.73** | **45.45** |\n\nWe find that Logic-LM without self-refinement surpasses both Standard and CoT prompting on both datasets across all tested models, including GPT-3.5, ChatGPT, and GPT-4. This shows that Logic-LM can also be applied in more complex and real-world applications. The integration of a symbolic solver, such as Z3 in this case, considerably enhances the model's logical reasoning capabilities by translating real-world problems into symbolic language. We will add these additional results to the final version. \n\n- [1] Zhong et al., AR-LSAT: Investigating Analytical Reasoning of Text. NAACL, 2022.\n- [2] Cobbe et al., Training Verifiers to Solve Math Word Problems. 2021. \n\n> *This approach works well if the premises can be cleanly converted into FOL representations, but this leads to a rather restricted set of possible applications for the Logic-LM framework.*\n\nThanks for pointing this out. First, we want to clarify that Logic-LM is not solely tied to FOL representations. Instead, it is a versatile framework that integrates LLMs with various symbolic solvers, and FOL is only one of the symbolic formulations. Together with the additional results shown in the previous reply, we already demonstrated the applicability of Logic-LM on six different logical reasoning datasets, and we have integrated a diverse set of symbolic solvers, including tools for symbolic mathematics (SymPy), theorem proving (Z3), first-order logic (FOL), constraint satisfaction problem (CSP solver), and logic programming (Pyke). This adaptability of a wide range of tasks and symbolic solvers underlines the general utility of Logic-LM.\n\nSecond, we acknowledge in our limitations section that Logic-LM is confined by the expressiveness of the symbolic solvers it employs. While certain problems may not be represented as logical form, this limitation should not diminish the inherent value of integrating symbolic solvers with LLMs. Looking ahead, an intriguing direction for extending Logic-LM's applicability would be to explore a hybrid approach that combines language-based reasoning (e.g., CoT) with symbolic-based reasoning. \n\n> *The work does provide a few examples of incorrect first-order logic representations, but does not go in depth to analyze if CoT failures are systematic and can be recovered by Logic-LM.*\n\nWe appreciate the reviewer's emphasis on the need for a more rigorous analysis of CoT's failure modes. In Section 4.1 (Lines 454 - 475), we have touched upon CoT's limitations in \"non-linear\" reasoning that include hypothesizing, conditioning, recursive inference, and the process of elimination. We argued that the integration of symbolic solvers is better suited to these reasoning styles, hence yielding a more marked improvement on the FOLIO (+15.67%) and the LogicalDeduction (+56.85%) datasets. In the camera-ready version, we plan to enrich this part with a more comprehensive quantitative analysis. This involves categorizing and reporting the proportion of each prevalent failure mode in CoT and discussing how Logic-LM effectively addresses these issues. We thank the reviewer for highlighting this point. \n\n> *The benefit of Logic-LM over CoT is clear for the highest reasoning depths, but when reasoning depth is lower, to what extent does Logic-LM improve over CoT? Is it possible that the failure rate of the translation (as shown in Fig. 6) ends up being worse than the failure rate of CoT logical errors (as ther is only one step of reasoning)?*\n\nAs shown in Figure 3, when the reasoning depth is 0, the Logic-LM and CoT achieve 81.7 and 76.3 accuracy on ProofWriter, respectively. Although the benefit of Logic-LM is less obvious than that in higher reasoning depths, Logic-LM still achieved an improvement of 7.1%. As shown in Table 3, Logic-LM generally show a very low failure rate in symbolic translation. For problems with low reasoning depth, the failure rate is even lower. For example, in ProofWriter depth-1, we find that GPT-3.5 produces 100% executable programs, 77.3% of which yielded correct answers, outperforming CoT's 73.6% accuracy. Unfortunately, we could only do the analysis on ProofWriter because the other datasets do not annotate the reasoning depth for their problems.", "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": "1. One of the biggest failure modes of language models is their inability to perform faithful logical reasoning, and Logic-LM no longer requires the language model to perform the logical reasoning. In a sense, there is a clean separation of concerns here between the language model and the symbolic solver. This neurosymbolic approach to logical reasoning is likely to inspire future work that doesn't rely solely on the LM.\n\n2. The symbolic solver in Logic-LM will never fault on performing logical reasoning. Errors when using the Logic-LM framework would be much easier to debug.\n\n3. Table 2 shows reasonable gains by using Logic-LM compared to CoT and standard prompting on three different models across four different datasets, highlighting that the technique is widely applicable. \n\n", "reasons_to_reject": "1. The first order logic representation used may be somewhat complex and difficult for someone to understand if they need to go in and debug the full pipeline, compared to the explanation generated by chain of thought.\n\n2. This approach works well if the premises can be cleanly converted into FOL representations, but this leads to a rather restricted set of possible applications for the Logic-LM framework. \n\n3. Sometimes, CoT performance is very similar to Logic-LM performance, highlighting that CoT is perhaps already able to perform some degree of logical reasoning. The work does provide a few examples of incorrect first-order logic representations, but does not go in depth to analyze if CoT failures are systematic and can be recovered by Logic-LM. ", "questions_to_authors": "1. The benefit of Logic-LM over CoT is clear for the highest reasoning depths, but when reasoning depth is lower, to what extent does Logic-LM improve over CoT? Is it possible that the failure rate of the translation (as shown in Fig. 6) ends up being worse than the failure rate of CoT logical errors (as ther is only one step of reasoning)?\n\n2. The four datasets you test on are still rather synthetic datasets. How do you envision your Logic-LM approach to apply in more complex and real-world applications? ", "paper_topic_and_main_contributions": "This paper proposes a new two-stage framework addressing the task of performing logical reasoning from a set of premises: first, it converts the premises and conclusion into an intermediate first-order logical representation called Pyke. Then, it applies an inference engine (one from the Stanford CS221 course) to deduce the truthness of the resulting conclusion.", "excitement": 4, "reproducibility": 5, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"Missing_References": "N/A", "Typos_Grammar_Style_and_Presentation_Improvements": "- It might be of interest to include a brief idea of how the CS221 solver works\n- Including a few examples of the benefit of self-refine would be instructive"}, "extra_text": {}}, {"review_id": "wK3RuEI15x", "reviewer": "Reviewer_sDiS", "summary": "", "questions": "Question A: The framework integrates three sets of grammar: deductive reasoning, first-order logic, and constraint optimization. In practice, how to choose and designate from the three grammars for a specific reasoning question? \nQuestion B: How does this framework deals with error propagation?\n", "limitations": "", "rating": 3, "confidence": 4, "soundness": 3, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We appreciate the valuable insights behind the comments and also want to clarify a few points.\n\n> *The idea of parsing natural language into symbolic forms might not be original considering the autoformalization task in mathematical reasoning.*\n\nWe appreciate the reviewer's insight regarding the similarities between Logic-LM and the autoformalization tasks common in mathematical reasoning. While the core idea of translating natural language into symbolic forms might be similar, the two areas differ in scope and complexity. Logical reasoning encompasses a broad scope of making and justifying arguments. As such, mathematical reasoning can be considered a specialized subset of logical reasoning, primarily focused on numeric deductions. Due to this numeric specificity, mathematical problems are often more readily translatable to symbolic forms. In contrast, logical reasoning covers a wider array of problem types, often requiring a deeper understanding of world knowledge and commonsense for effective parsing into symbolic forms. \n\nDespite plenty of works studying mathematical reasoning, our work pioneers in extending the concept of \"autoformalization\" to a broader range of logical reasoning tasks with LLMs. Nonetheless, we acknowledge the relevance of existing works on autoformalization in mathematical reasoning and will include the suggested references in the related work section of our paper. \n\n> *Question A: The framework integrates three sets of grammar: deductive reasoning, first-order logic, and constraint optimization. In practice, how to choose and designate from the three grammars for a specific reasoning question?*\n\nAs an initial exploration of integrating symbolic solvers with LLMs, our work primary focus on how to correctly translate the problem into the specific symbolic formulation used by the chosen symbolic solver. Therefore, in our experiments, the grammar for each dataset was predetermined. However, we agree with the reviewer's point that automatically selecting an appropriate symbolic system is an important practical concern. \n\n**Additional Experiments**. To address this, we conducted an additional experiment to evaluate the potential of using LLMs as grammar designators. We prompted GPT-4 with 8 demonstrations, each consisting of a problem and its corresponding symbolic language, such as `(Problem from FOLIO, \"FOL representation\")`. These demonstrations were randomly drawn from each of the four datasets we used (two examples per dataset).  Subsequently, we evaluated GPT-4's performance on the grammar designation task to assign new examples to the appropriate symbolic grammar (3-class classification since we have defined three different grammars). Out of 400 randomly sampled test cases (100 from each dataset), GPT-4 achieved a high F1 score of 96.5%. However, we note that this high performance may partially due to the fact that the problems of the four datasets we used are easy to differentiate. In real-world applications, determining the most fitting symbolic system could be more challenging. We will include these new findings and discussions in a discussion section of the camera-ready version. We thank the reviewer for raising this interesting and valuable question. \n\n> *Question B: How does this framework deals with error propagation?*\n\nFirst, we want to clarify that Logic-LM actually has less error propagation problems than chain-of-thought.  CoT sequentially generates the reasoning chain step-by-step until it reaches the final answer. Therefore, error propagation is easy to happen where an error in early reasoning steps can readily affect all subsequent steps. Logic-LM mitigates this by refocusing the language model's task from \"step-by-step problem-solving\" to \"symbolic problem representation\" (Line 203 - 207). When the problem is accurately formulated, symbolic solvers can guarantee the correctness of the reasoning. By offloading the burden of logical reasoning to external symbolic solvers, it minimizes the risk of error propagation for CoT during complex reasoning processes. \n\nSecond, we admit that Logic-LM is not entirely immune to error propagation. Errors can occur when the LLM generates incorrect symbolic formulations that affect the solver's reasoning. To address this, we have integrated the self-refinement mechanism that uses feedback from the symbolic solver's error messages to correct faulty formulations (Section 3.4). Self-refinement can effectively alleviate error propagation, as evidenced by the results in Table 3 and Figure 5. However, as mentioned in Lines 543-550, there still exist cases where incorrect formulations go undetected by the symbolic solver. To tackle this limitation, future work could involve extending the self-refinement module to incorporate additional forms of feedback, such as a reward signal from a module specifically designed to assess the accuracy of generated symbolic forms. We leave this for future exploration.", "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": "The experimental results show the effectiveness of the method. The paper is clearly written and easy to follow. ", "reasons_to_reject": "The idea of parsing natural language into symbolic forms might not be original considering the autoformalization task in mathematical reasoning. Please see the details in “Missing References”.", "questions_to_authors": "Question A: The framework integrates three sets of grammar: deductive reasoning, first-order logic, and constraint optimization. In practice, how to choose and designate from the three grammars for a specific reasoning question? \nQuestion B: How does this framework deals with error propagation?\n", "paper_topic_and_main_contributions": "This paper proposes integrating LLMs with symbolic solvers to improve logical problem-solving. A self-refiner is incorporated in the reasoning process to iteratively refine the generate valid logic forms. The final answer is then obtained by a result interpreter. The method is evaluated on 4 datasets. ", "excitement": 3, "reproducibility": 3, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {"Missing_References": "What the “Problem Formulator” module does is similar to the autoformalization task in mathematical reasoning, for instance:\n[1] Wu Y, Jiang A Q, Li W, et al. Autoformalization with large language models[J]. Advances in Neural Information Processing Systems, 2022, 35: 32353-32368.\n[2] Wang Q, Brown C, Kaliszyk C, et al. Exploration of neural machine translation in autoformalization of mathematics in Mizar[C]//Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2020: 85-98.\n"}}]

Author rebuttal:

Meta-review: This paper proposed to improve the reasoning capability of LLMs by giving them the access to a symbolic reasoner. A self-refinement mechanism instructs the LLM to refine the incorrect logical form, by prompting it with the erroneous logic form, the solver’s error message, and a set of demonstrations showing common error cases and their remedies. 
Experiment is conducted by transferring four existing synthetic natural language datasets back to symbolic sentences and solving it with a symbolic reasoner. The result shows significant improvement over standard and CoT settings for 3 GPT models.

Strength:
1. The three stage design and self-refinement are reasonable and effective, even though not completely novel.
2. A thorough analysis on the performance of 4 tasks and 3 GPT models.

Weakness:
1. The datasets are synthetic and it is not clear how much impact the proposed approach has on more natural tasks such as Entailmentbank. 
2. It is not clear what possible applications can the FOL representation be applied to.
Decision: Accept-Findings