The DOI matches its DataCite record; 62 of the 62 references it cites were found in a registry or an index; 7 of the 13 sources its claims cite were checked for support.
Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
Open accessAbstract
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. Code and data are publicly available at https://github.com/teacherpeterpan/Logic-LLM.
Overview
AI snapshot
Written from the paper’s full text.
TL;DR
LOGIC-LM combines LLMs with deterministic symbolic solvers by having the LLM translate natural-language logical problems into symbolic formulations, then offloading inference to solvers and interpreting results back into answers. Across five logical reasoning datasets, it improves over standard prompting by 39.2% on average and over chain-of-thought by 18.4% on average.
Key findings
- LOGIC-LM outperforms standard LLMs and CoT across all five datasets; with GPT-3.5, average improvement is 39.2% over standard prompting and 18.4% over CoT.
- With GPT-4, LOGIC-LM further improves over standard prompting by an average of 24.98% and over CoT by 10.44%.
- Performance gains grow with reasoning depth on ProofWriter: 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, respectively.
- Self-refinement increases executable symbolic formulations by 5.01% on average, but accuracy tends to stagnate in later rounds even as executability continues to rise.
Methods
- Design: three-stage framework — Problem Formulator (LLM translates NL into symbolic language), Symbolic Reasoner (deterministic solver performs inference), and Result Interpreter (maps solver output to natural-language answer). A self-refinement module revises symbolic formulations using solver error messages.
- Data: five logical reasoning datasets — PrOntoQA, ProofWriter, FOLIO, LogicalDeduction, and AR-LSAT — covering deductive reasoning, first-order logic, constraint satisfaction, and analytical reasoning. Test sizes reported in the paper’s table are PrOntoQA 500, ProofWriter 600, FOLIO 204, LogicalDeduction 300, and AR-LSAT 230; the text separately says AR-LSAT has 231 multiple-choice questions.
- Analysis: compares LOGIC-LM against standard in-context prompting and chain-of-thought prompting using ChatGPT (gpt-3.5-turbo), GPT-3.5 (text-davinci-003), and GPT-4 (gpt-4), with temperature 0 and accuracy as the metric. Symbolic solvers include Pyke, Prover9, python-constraint, and Z3.
Limitations
- Stated: LOGIC-LM’s applicability is bounded by the expressiveness of the symbolic solver, since not all problems can be easily encoded in formalisms such as first-order logic.
- Stated: it depends on in-context learning plus self-refinement to convert NL into symbolic representations, which may struggle with intricate grammar structures such as probabilistic soft logic due to limited demonstrations and context size.
- Evident from the paper’s analysis: self-refinement mainly fixes invalid symbolic forms using solver error messages, but a valid symbolic representation is not necessarily a correct problem formulation; the paper notes accuracy can stagnate even as executable rate increases. Error cases also show GPT-4 struggles with predicate consistency, interpreting expressions like “below” vs. “above,” and FOL grammar.
Model-written summary. Check it against the paper before relying on it.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
24 Own interpretation · 20 Own result · 5 Partly supported · 5 Own method · 3 No basis given · 1 Supported · 1 Sources not found · accuracy not yet measured
Every source the paper cites for this claim was checked and supports it.
In the paper
“Despite the advances of LLMs, they still struggle with complex logical reasoning problems (Liu et al., 2023b).”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Problem Goal Answer
What the sources say
- Supportedcites Liu et al., 2023b source
The Conclusion reports that ChatGPT and GPT-4 face challenges on new and out-of-distribution logical-reasoning data and do not perform especially well on natural-language inference requiring logical reasoning. This supports the citing sentence’s broad claim that advanced language models still struggle with difficult logical-reasoning problems. (LLM, conf=0.90)
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
- Supported
The cited sources support only part of this claim — read each source’s verdict below.
In the paper
“Recent studies (Golovneva et al., 2023;Ribeiro et al., 2023b;Lyu et al., 2023) found that LLMs occasionally make unfaithful reasoning, i.e., the derived conclusion does not follow the previously generated reasoning chain.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Problem Goal Answer
What the sources say
- Not matchedcites Golovneva et al., 2023
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- Not matchedcites Ribeiro et al., 2023b
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- Supportedcites Lyu et al., 2023 source
The Input section states that in standard chain-of-thought prompting, the final answer does not necessarily follow from the generated reasoning chain. Its Figure 1 example shows an answer that does not follow from the chain, matching the cited claim. (LLM, conf=0.94)
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
- Not matched
The cited sources support only part of this claim — read each source’s verdict below.
In the paper
“However, they have demonstrated a notable ability to comprehend textual inputs and translate them into formal programs, such as mathematical equations (He-Yueya et al., 2023) or Python codes (Gao et al., 2023).”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 3.1 Problem Formulator
What the sources say
- Supportedcites He-Yueya et al., 2023 source
Section 3.1 says the LLM formalizes math word problems as variables and equations. The Conclusion reports that this approach was effective, supporting the claim as applied to mathematical equations; the separate Python-code example is attributed to another source. (LLM, conf=0.93)
- Not matchedcites Gao et al., 2023
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
boosted- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
- Supported
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We also find that LOGIC-LM becomes increasingly effective as the required reasoning depth increases ( § 4.3).”
- Also stated in: § 4.3 Robustness of Reasoning · hedged
“The results, shown in Figure 3, indicate that LOGIC-LM becomes increasingly effective as the required reasoning depth increases.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Problem Goal Answer
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
- Also stated in: § 4.3 Robustness of Reasoning · hedged
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Example 4 exemplifies GPT-4's challenge with fully grasping the rules of FOL grammar, evidenced by the invalid generated formula: Rating(subway, y) ∧ y > 9.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.5 Case Study
plaindirectSingle case- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“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.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.4 Impact of Self-Refinement
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Finally, by analyzing the impact of selfrefinement, we highlight the effectiveness of incrementally revising symbolic formalizations when interacting with the symbolic solver ( § 4.4).”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Problem Goal Answer
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“GPT-4 outperforms GPT-3.5 by a large margin of 48.46% on average for the standard prompting.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: unclear — It is unclear whether the paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The performance of Standard and CoT declines precipitously with the escalation of problem complexity.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.3 Robustness of Reasoning
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Generally, LLM demonstrates high proficiency in transcribing problems into symbolic formats, evidenced by its near 100% Exe_Rate on ProntoQA, ProofWriter, and Logi-calDeduction.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.2 Effectiveness of Problem Formulator
boosted- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
- It may state two separate claims as one. 17
- Probably not a substantial claim. 13
The cited sources support only part of this claim — read each source’s verdict below.
In the paper
“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 networks with symbolic reasoning, these methods suffer from limitations such as hand-crafted or specialized module designs that are not easily generalizable, or brittleness due to the difficulty of optimization.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 2 Related Work
What the sources say
- Partly supportedcites Mao et al., 2019 sourceExperimental — accuracy not yet measured
The Training Paradigm (p. 6) says curriculum learning is essential to joint optimization, and Appendix E (p. 19) reports that training can fail to converge without it. But the paper describes NS-CL as robust and demonstrates several forms of generalization (p. 2); it does not support the unqualified claim that its module design is not easily generalizable or that the trained method is brittle. (LLM, conf=0.86)
- Not matchedcites Gupta et al., 2020
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
- Partly supportedcites Manhaeve et al., 2021 sourceExperimental — accuracy not yet measured
The Related Work section describes limitations of some prior neuro-symbolic methods, including restricted expressivity, and §7.3 identifies an approach specialized for NLP tasks. It does not establish that prior methods generally rely on hand-crafted modules that are hard to generalize or are brittle because optimization is difficult. Page numbers were not available in our copy. (LLM, conf=0.78)
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
- Partly supported
The cited sources support only part of this claim — read each source’s verdict below.
In the paper
“This aligns with the assertion that the main enhancement of GPT-4 lies in its ability to carry out complex reasoning (OpenAI, 2023).”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
What the sources say
- Partly supportedcites OpenAI, 2023 sourceExperimental — accuracy not yet measured
The Observed Safety Challenges section (p. 44) says GPT-4 improves on earlier models in reasoning, but also names knowledge retention and coding. The report does not identify complex reasoning as GPT-4’s main enhancement. (LLM, conf=0.86)
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim. The paper’s conclusions may not depend on it.
- Partly supported
The cited sources support only part of this claim — read each source’s verdict below.
In the paper
“AR-LSAT is particularly challenging, with state-of-the-art models only achieving performance slightly better than random guessing (Liang et al., 2022;Ribeiro et al., 2023a).”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4 Experiments
What the sources say
- Partly supportedcites Liang et al., 2022 sourceExperimental — accuracy not yet measured
The Reasoning section (page unavailable) says most evaluated models scored around the 20% chance level on LSAT questions, supporting the claim that the task is challenging. It does not establish that the best-performing models scored slightly above chance; it also reports 0% accuracy for the code models evaluated on LSAT. (LLM, conf=0.84)
- Not matchedcites Ribeiro et al., 2023a
Couldn’t be matched to a paper in Crossref, so it can’t be checked.
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim. The paper’s conclusions may not depend on it.
- Partly supported
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“While integrating CoT generally enhances LLM performance, we find its benefits comparatively less substantial or even negative on FOLIO, LogicalDeduction, and AR-LSAT, with a modest improvement of 11.75%, 9.41%, and -3.2%, respectively.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“When it comes to datasets comprising real-world, expertly crafted problems, such as FOLIO and AR-LSAT, GPT-4's performance is notably less promising, with Exe_Rate scores of 79.9% and 32.6% respectively.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.2 Effectiveness of Problem Formulator
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“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-ofthought prompting.”
- Also stated in: § Problem Goal Answer · boosted
“Our evaluations show that the strategy of integrating LLMs with symbolic solvers performs significantly better than purely relying on LLMs for logical reasoning, with an average improvement of 39.2% over the standard prompting and 18.4% over the chain-of-thought prompting ( § 4.1).”
- Also stated in: § 4.1 Main Results · plain
“With GPT-3.5, our method outperforms standard LLM on all datasets, with an average improvement of 39.2%.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Abstract
boosteddirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
- Also stated in: § Problem Goal Answer · boosted
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Logic-LM significantly outperforms standard LLMs and CoT across all datasets.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“We find that as the rounds of self-refinement increase, the percentage of executable formulations consistently increases, leading to an enhancement in the final performance.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.4 Impact of Self-Refinement
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“Nonetheless, there remain certain difficulties in accurately understanding the semantics of the problem.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.5 Case Study
plain- Asserted: passes — The authors put it forward as true.
- Checkable: fails — It may be too vague to check against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably not a substantial claim. It may be too vague to check against evidence. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“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, respectively.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.3 Robustness of Reasoning
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“By delegating the reasoning to symbolic solvers, our method can further improve GPT-4 by an average of 24.98% and 10.44% for standard prompting and CoT prompting, respectively.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
A result the paper reports from its own data — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“On the contrary, the benefits of CoT on ProntoQA and ProofWriter are 51.59% and 33.82%, respectively.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
The paper states this without a source or data behind it here, so there is nothing to check it against. The quote shows it is in the paper.
In the paper
“However, the accuracy tends to stagnate in subsequent rounds, even though the Exe_Rate continues to increase.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.4 Impact of Self-Refinement
plaincorrelational- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“Compared to CoT, the integration of symbolic solvers is better suited to these reasoning styles, hence yielding a more marked improvement on FO-LIO (+21.85%),LogicalDeduction (+45.67%), and AR-LSAT (+24.14%).”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“In LOGIC-LM, multi-step logical reasoning is delegated to external symbolic solvers, thereby transitioning the challenge of LLM from problemsolving to problem representation.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.3 Robustness of Reasoning
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
What the paper did — it cites no source for this, so there is none to check. The quote shows it is in the paper.
In the paper
“For reproducible results, we set the temperature to 0 and select the response with the highest probability from LLMs.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4 Experiments
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
What the paper did — it cites no source for this, so there is none to check. The quote shows it is in the paper.
In the paper
“We randomly selected 300 examples from each subset of ProofWriter, ensuring a balanced label distribution.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.3 Robustness of Reasoning
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim. The paper’s conclusions may not depend on it. It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“As a consequence, the model's applicability is inherently bounded by the expressiveness of the symbolic solver, for example, not all problems can be easily encoded in first-order logic.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Limitations
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
What the paper did — it cites no source for this, so there is none to check. The quote shows it is in the paper.
In the paper
“For these un-executable cases, we fall back on using chain-of-thought to predict the answer.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim. The paper’s conclusions may not depend on it.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“that CoT emulates human forward-chain reasoning: beginning with known facts and sequentially deriving new conclusions until the goal is met.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
hedgedconditional- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“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 advantage of the logical faithfulness and transparency offered by symbolic solvers.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Problem Goal Answer
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“By defining additional problem-specific formulations, our framework retains the flexibility to accommodate a wider range of reasoning tasks.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 3.1 Problem Formulator
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim.
What the paper did — it cites no source for this, so there is none to check. The quote shows it is in the paper.
In the paper
“Since all examples are formed as multiple-choice questions, we evaluate model performance based on the accuracy of selecting the correct answer.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4 Experiments
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“This inconsistency is a 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.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.5 Case Study
hedgedconditionalSingle case- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
It may state two separate claims as one.
What the paper did — it cites no source for this, so there is none to check. The quote shows it is in the paper.
In the paper
“To ensure fair comparisons, we use the same in-context examples for all models.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4 Experiments
plain- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The flexible design of LOGIC-LM facilitates this integration.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Limitations
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim. The paper’s conclusions may not depend on it.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“This arises from the difficulty in conveying complex grammatical rules to the language model through a limited number of demonstrations within a constrained context size.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Limitations
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: passes — The paper’s conclusions depend on it.
- Based: passes — The paper gives a reason why it holds.
Probably not a substantial claim.
A conclusion the paper draws from its own results — it cites no other source for it, so there is none to check. The quote shows it is in the paper.
In the paper
“The wide range of reasoning tasks that we can instantiate our LOGIC-LM framework on shows its general applicability.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Limitations
plaindirect- Asserted: passes — The authors put it forward as true.
- Checkable: passes — It can be checked against evidence.
- Load-bearing: fails — The paper’s conclusions may not depend on it.
- Based: fails — The paper may give no reason why it holds.
Probably not a substantial claim. The paper’s conclusions may not depend on it. The paper may give no reason why it holds.
The paper relies on this without support.
The main obstacle in using symbolic solvers for logical reasoning is accurately translating natural language problems into symbolic representations.
“The main obstacle is how to accurately translate a problem into symbolic representations, considering the inherent ambiguity and flexibility of natural language.”
The paper relies on this without support.
Language models have inherent limitations such as the inability to access up-to-date information, take actions, or perform precise mathematical reasoning.
“Language models have inherent limitations such as the inability to access up-to-date information, take actions, or perform precise mathematical reasoning.”
The paper relies on this without support.
Many analytical reasoning problems can be formulated as SAT problems.
“Many analytical reasoning problems can be formulated as SAT problems.”
The paper relies on this without support.
A lot of real-world analytical reasoning problems can be represented as problems of solving a system of equations.
“A lot of real-world analytical reasoning problems can be represented as problems of solving a system of equations.”
The paper relies on this without support.
For complex problems, generating the correct logical form may become challenging for LLMs.
“For complex problems, generating the correct logical form may become challenging for LLMs.”
The paper relies on this without support.
While logic programming efficiently represents common deductive reasoning problems, it may fail to represent more complex first-order logic problems.
“While the logic programming language efficiently represents common deductive reasoning problems, it may fail to represent more complex first-order logic (FOL) problems.”
The authors state this as an assumption.
The complexity of formally representing a problem statement in logical form should remain relatively constant, regardless of whether the questions require simple or complex reasoning.
“Ideally, the complexity of formally representing a problem statement in logical form should remain relatively constant, regardless of whether the questions require simple or complex reasoning.”
The paper relies on this without support.
The problems in ProntoQA, ProofWriter, and LogicalDeduction are mostly synthetically generated, limiting language variability.
“given that their problems are mostly synthetically generated, limiting language variability.”
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The source backs part of the claim, not all of it — or backs it for a different population, condition or comparison.
In the citing paper
“but they typically operate at the level of the full problem or the full reasoning trace.”
From Reason Popper-ly: Patching In-Context Reasoning with Inductive Logic Programming (2026) · cites this paper as Pan et al. [2023]
Experimental — accuracy not yet measuredThe source backs part of the claim, not all of it — or backs it for a different population, condition or comparison.
In the citing paper
“LOGIC-LM [15] creates a deterministic symbolic solver that expresses reasoning in a specific symbolic format to obtain actual results.”
From ChatLogic: Integrating Logic Programming with Large Language Models for Multi-Step Reasoning (2024) · cites this paper as [15]
Experimental — accuracy not yet measuredThe cited source says what the claim attributes to it.
In the citing paper
“This aligns with recent research integrating LLMs with symbolic reasoners for various reasoning tasks (Olausson et al., 2023;Pan et al., 2023).”
From TReMu: Towards Neuro-Symbolic Temporal Reasoning for LLM-Agents with Memory in Multi-Session Dialogues (2025) · cites this paper as Pan et al., 2023
The cited source says what the claim attributes to it.
In the citing paper
“Logic-LM Pan et al. [2023] partially addresses this issue by using LLMs as translators from natural language to formal logic, but the translation stage itself introduces an additional failure mode.”
From Reason Popper-ly: Patching In-Context Reasoning with Inductive Logic Programming (2026) · cites this paper as Pan et al. [2023]
The cited source says what the claim attributes to it.
In the citing paper
“Existing neurosymbolic approaches either internalize rules through retraining with logic-informed objectives de Souza et al. [2025], or rely on hand-crafted formal grammars specified per domain Pan et al. [2023], Chen et al. [2022, 2023].”
From Reason Popper-ly: Patching In-Context Reasoning with Inductive Logic Programming (2026) · cites this paper as Pan et al. [2023]
The cited source says what the claim attributes to it.
In the citing paper
“Recent neurosymbolic approaches either translate natural-language problems into formal representations and delegate reasoning to external solvers Pan et al. [2023], Olausson et al. [2023], or inject symbolic structure into the reasoning process to improve faithfulness and controllability Xu et al. [2024], Lyu et al. [2023].”
From Reason Popper-ly: Patching In-Context Reasoning with Inductive Logic Programming (2026) · cites this paper as Pan et al. [2023]
The cited source says what the claim attributes to it.
In the citing paper
“These approaches show that symbolic constraints can improve reasoning reliability”
From Reason Popper-ly: Patching In-Context Reasoning with Inductive Logic Programming (2026) · cites this paper as Pan et al. [2023]
The cited source says what the claim attributes to it.
In the citing paper
“Neither [11] nor [13] pose a viable approach in this current work, however, due to the complexity of questions expected for a KBQA system, and our subsequent interest in leveraging the generative power of an LLM to answer inputted queries.”
From ProSLM: A Prolog Synergized Language Model for explainable Domain Specific Knowledge Based Question Answering (2024) · cites this paper as [13]
The cited source says what the claim attributes to it.
In the citing paper
“While LLMs can generate logic programs, their outputs in formal domains remain prone to errors [15].”
From ADVENT: LLM-Driven Automatic Predicate Invention for ILP (2026) · cites this paper as [15]
The cited source says what the claim attributes to it.
In the citing paper
“External tools used for self- correction include code interpreters for code generation tasks (Chen et al., 2024e;Gou et al., 2024) and symbolic reasoners for logical reasoning tasks (Pan et al., 2023).”
From When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs (2024) · cites this paper as Pan et al., 2023
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
Each contradiction between two passages listed here was confirmed by an independent check.
Rated major: it would touch a result — a value a result rests on, reported and recomputed p-values on opposite sides of the significance level, two passages that conflict with no sign which is right, or a cited work retracted before this paper was published.
In the paper
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.1 Main Results
“1. Logic-LM significantly outperforms standard LLMs and CoT across all datasets.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Query:
“| PrOntoQA | 47.40 | 67.80 | 61.00 | 51.80 | 83.00 | 85.00 | 77.40 | 98.79 | 83.20 |”
Rated minor: it would not touch a result — a value no result rests on, a p-value that stays on the same side of the significance level, or a conflict that is clerical, resolved elsewhere in the paper, or outside its own findings.
In the paper
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4 Experiments
“We use the test set which has 231 multiplechoice questions.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Query:
“| AR-LSAT | AR | 230 | 5 |”
Rated minor: it would not touch a result — a value no result rests on, a p-value that stays on the same side of the significance level, or a conflict that is clerical, resolved elsewhere in the paper, or outside its own findings.
In the paper
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.3 Robustness of Reasoning
“depth-0, depth-1, depth-2, depth-4, and depth-5 problems, respectively.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > 4.3 Robustness of Reasoning
“The problems in these subsets require 0, <=1, <=2, <=3, and <=5 hops of reasoning, respectively.”
Rated minor: it would not touch a result — a value no result rests on, a p-value that stays on the same side of the significance level, or a conflict that is clerical, resolved elsewhere in the paper, or outside its own findings.
In the paper
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Answer
“A) The convertible is the oldest.”
§ LOGIC-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning > Which of the following is true?
“A) The tractor is the oldest.B) The convertible is the oldest.C) The minivan is the oldest.”
Citations
Cites
Language Models are Few-Shot Learners
Brown, T. B., Mann, B., Ryder, N., Subbiah, M., Kaplan, J., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al. (2020) · arXiv · doi:10.48550/arxiv.2005.14165 · Cited by 23,372
de Moura, L., & Bjørner, N. (2008) · Lecture Notes in Computer Science · doi:10.1007/978-3-540-78800-3_24 · Cited by 6,595 · cited 2×
“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 4 .”
BackgroundMethodChain-of-Thought Prompting Elicits Reasoning in Large Language Models
Wei, J., Wang, X., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, E., Le, Q., & Zhou, D. (2022) · arXiv · doi:10.48550/arxiv.2201.11903 · Cited by 4,263 · cited 7×
“”, these models are able to answer questions with explicit reasoning steps (Wei et al., 2022b; Kojima et al., 2022).”
BackgroundMethodInfluentialSelf-citationTraining language models to follow instructions with human feedback
Ouyang, L., Wu, J., Jiang, X., Almeida, D., Wainwright, C. L., Mishkin, P., Zhang, C., Agarwal, S., Slama, K., Ray, A., et al. (2022) · arXiv · doi:10.48550/arxiv.2203.02155 · Cited by 4,208
A Machine-Oriented Logic Based on the Resolution Principle
Robinson, J. A. (1965) · Journal of the ACM · doi:10.1145/321250.321253 · Cited by 4,011 · cited 2×
“It initially converts FOL statements to conjunctive normal form (CNF) and then performs resolution (Robinson, 1965) on the CNF to deduce whether a conclusion is true, false, or unknown.”
BackgroundMethodEnergy and Policy Considerations for Deep Learning in NLP
Strubell, E., Ganesh, A., & McCallum, A. (2019) · Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics · doi:10.18653/v1/p19-1355 · Cited by 3,684
Training Language Models to Follow Instructions with Human Feedback
Ouyang, L., Wu, J., Jiang, X., Almeida, D., Wainwright, C., Mishkin, P., Zhang, C., Agarwal, S., Slama, K., Ray, A., et al. (2022) · Advances in Neural Information Processing Systems 35 · doi:10.52202/068431-2011 · Cited by 3,117
Richardson, M., & Domingos, P. (2006) · Machine Learning · doi:10.1007/s10994-006-5833-1 · Cited by 2,676 · cited 2×
“For example, 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…”
BackgroundA Mathematical Introduction to Logic
(2001) · Elsevier eBooks · doi:10.1016/c2009-0-22107-6 · Cited by 2,398 · cited 1×
“To address this, we also include the FOL grammar (Enderton, 2001) in Appendix A.”
MethodSelf-Refine: Iterative Refinement with Self-Feedback
Madaan, A., Tandon, N., Gupta, P., Hallinan, S., Gao, L., Wiegreffe, S., Alon, U., Dziri, N., Prabhumoye, S., Yang, Y., et al. (2023) · arXiv · doi:10.48550/arxiv.2303.17651 · Cited by 2,314
Research works printed but not linked: 3
- Stephen Bach, Matthias Broecheler, Bert Huang, and Lise Getoor. 2017. Hinge-loss markov random fields and probabilistic soft logic. Journal of Machine Learning Research (JMLR), 18(1):1-67.
- Kostas S. Metaxiotis, Dimitris Askounis, and John E. Psarras. 2002. Expert systems in production planning and scheduling: A state-of-the-art survey. Journal of Intelligent Manufacturing, 13(4):253-260. · DOI
- 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 reasoning and ex- planation benchmark. In Proceedings of the 11th International Conference on Learning Representa- tions (ICLR). · DOI
Cited by
Sorted by citations
Hadi, M. U., Al-Tashi, Q., Qureshi, R., Shah, A., Muneer, A., Irfan, M., Zafar, A., Shaikh, M. B., Akhtar, N., Hassan, S. Z., et al. (2023) · doi:10.36227/techrxiv.23589741.v4 · Cited by 193
Ma, Y., Cao, Y., Hong, Y. S., & Sun, A. (2023) · Findings of the Association for Computational Linguistics: EMNLP (Findings of EMNLP) · doi:10.18653/v1/2023.findings-emnlp.710 · Cited by 193
“…Chowdhery et al. 2022; Touvron et al. 2023) have shown remarkable abilities on various NLP applications such as factual question answering (Yu et al., 2023; Sun et al., 2023), arithmetic reasoning (Chen et al., 2022a; Qian et al., 2023) and logical reasoning (Jung et al., 2022; Pan et al., 2023).”
BackgroundEnhancing emergency decision-making with knowledge graphs and large language models
Chen, M., Tao, Z., Tang, W., Qin, T., Yang, R. C., & Zhu, C. (2024) · International Journal of Disaster Risk Reduction · doi:10.1016/j.ijdrr.2024.104804 · Cited by 112
Pan, L., Saxon, M., Xu, W., Nathani, D., Wang, X., & Wang, W. Y. (2024) · Transactions of the Association for Computational Linguistics · doi:10.1162/tacl_a_00660 · Cited by 86
Self-citationWhen Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs
Kamoi, R., Zhang, Y., Zhang, N., Han, J., & Zhang, R. (2024) · Transactions of the Association for Computational Linguistics · doi:10.1162/tacl_a_00713 · Cited by 200
Metadata
- Authors
- Pan, L., Albalak, A., Wang, X., & Wang, W. Y.
- Affiliations
- University of California, Santa Barbara (US)
- Venue
- arXiv
- Publisher
- arXiv
- Published
- 2023
- Pages
- 3806-3824
- arXiv
- 2305.12295
- OpenAlex
- W4389519818
- Semantic Scholar
- 9e9e4df2996bac794c4f04cb887df3e553bae4fd
- Cited by
- 144
- References
- 56
- Citations by year
- 2026: 59 · 2025: 54 · 2024: 25 · 2023: 6
- FWCI
- 25.82
- Type
- conference paper
- Language
- en
- Open access
- gold
- doi.org
- Licence
- Locations
- arXiv (Cornell University) (submittedVersion, cc-by)
- arXiv (Cornell University) (cc-by)
- Funders
- National Science Foundation (2048122)
- Topics
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
- Physical Sciences › Computer Science › Artificial Intelligence › Topic Modeling
- Physical Sciences › Computer Science › Artificial Intelligence › Natural Language Processing Techniques
- Keywords
- large language models, symbolic solvers, logical reasoning, self-refinement, chain-of-thought prompting, proof writing, first-order logic, logical deduction
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
A language model drew the claims from the paper on 2026-10-19, under version 3 of the claim definition (model deepseek-v4.1-flash, prompt extract-v3).
A second model labelled each claim on 2026-10-19 (model jev-1.13-20260917, definition revision gold-guideline-v0.2).
Cited sources are checked with a language model’s help (gpt-6-sol).
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
