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
Items 101–154 of 154
Differentiating Modalities in an AI System
Bradford, P. G., Orphys, H., Udler, D., et al. (2026) · Smart innovation, systems and technologies · doi:10.1007/978-981-95-1361-1_44
Ontology Modeling of Normative Documents: Analysis of Approaches and Prospects of Automation
Kabzhan, Z., SHAKHNOVICH, A. L., Shogelova, N., et al. (2025) · Trudy Universiteta · doi:10.52209/1609-1825_2025_4_188
REGAL: Extracting Implicit Rules in Text Using LLMs with Logic Program Feedback
Rajasekharan, A., & Gupta, G. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-15981-6_10
Su, P., Xu, R., Huang, J., et al. (2026) · Research Square · doi:10.21203/rs.3.rs-8541175/v1
LoT-Reasoner: Enhancing Model Reasoning with Logic-Check Tool and Multi-Tool Coordination
Qin, K., Du, J., Xue, Z., & Zhang, J. (2025) · International Conference on Artificial Intelligence and Computer Engineering (ICAICE) · doi:10.1109/icaice68195.2025.11382455
“Existing approaches [1], [2] attempt to align natural language reasoning with formal representations or programmatic structures, yet implicit premises and vague reasoning often per-sist—especially in question-answering scenarios.”
Mikriukov, A., Plaksin, Y., Ravveduto, A., Snigireva, M., Succi, G., Tormasov, A. G., & Трофимова, Е. (2025) · International Conference on Data Science and Intelligent Systems (DSIS) · doi:10.1109/dsis67228.2025.11390564
“Notable examples include [35], [36], where LLMs are employed to translate natural language into structured representations that serve as inputs for deterministic solvers.”
A Decentralized Framework for Auditing Large Language Model Reasoning
Huang, M. Y.-C., Tan, Z., Zhang, M., et al. (2025) · IEEE International Conference on Trust, Privacy and Security in Intelligent Systems and Applications (TPS-ISA) · doi:10.1109/tps-isa67132.2025.00074
Yu, X. Y. X., Jiang, L., Zhuang, W., et al. (2026) · International Journal of Computational Intelligence and Applications · doi:10.1142/s1469026826500124
Enhancing Autonomous Vehicle Test Scenario Reasoning in Language Models
Ataei, D., Paranjape, I., & Whitehead, J. (2025) · IEEE International Conference on Intelligent Transportation Systems (ITSC) · doi:10.1109/itsc60802.2025.11423810
“There have been works that have used symbolic solvers to improve the reasoning capabilities of LLMs [9] [10].”
Vladika, J., Fichtl, A. M., & Matthes, F. (2026) · Scientific Reports · doi:10.1038/s41598-026-45245-2
“This highlights the need to augment LLMs with methods that clarify their decision-making process, such as decision trees 38 , symbolic logic reasoning 39 , chain-of-thought mechanism 40 , and other techniques of explainability 41 .”
Shen, W., Liu, H., Yin, J., et al. (2026) · IEEE International Conference on Acoustics Speech and Signal Processing · doi:10.1109/icassp55912.2026.11462516
SoGRE: Boosting Logical Reasoning of LLMs via Solver-Guided Reasoning Enhancement
Wang, Z., Zhang, L., Zhang, M., Li, Q. P., & Zhang, M. (2026) · IEEE International Conference on Acoustics Speech and Signal Processing · doi:10.1109/icassp55912.2026.11463079
LLM-Driven MCTS for Conditional Story Generation via Logic-Guided Evidence Tree Optimization
Wu, H., Tian, Z., Huang, Z., Lin, N., Song, Y., Wen, Z., Lu, M., Liu, F., & Li, D. (2026) · IEEE Transactions on Audio Speech and Language Processing · doi:10.1109/taslpro.2026.3687020
“(cid:2) Inference based on the logical formulas: To verify the logical coherence of evidence nodes within an evidence chain, we perform first-order logic inference via the resolution principle [38].”
Matrix as Plan: Structured Logical Reasoning with Feedback-Driven Replanning
Chen, K., Zeng, J., Peng, Z., Guo, L., Zhang, G., & Wang, T. (2026) · International World Wide Web Conference (WWW) · doi:10.1145/3774904.3792213
A Review of System 2 Reasoning from Cognitive Theories to Algorithmic Innovations
Yu, X., Xia, J., & Yang, C. (2025) · International Conference on Intelligent Education and Intelligent Research (IEIR) · doi:10.1109/ieir67391.2025.11491040
“Integrating symbolic solvers for faithful logical reasoning reduces hallucination and enforces rule consistency—valuable for algebraic transformations and formal proof obligations [12].”
InfluentialChen, W., & Sun, C. (2025) · International Conference on Intelligent Education and Intelligent Research (IEIR) · doi:10.1109/ieir67391.2025.11491556
“The primary advantage of CoK lies in its structured expressiveness [13].”
Autonomous Business System via Neuro-symbolic AI
Pang, C., & Sayama, H. (2026) · IEEE International Systems Conference (SysCon) · doi:10.1109/syscon66367.2026.11503621
“Pan et al. [29] used LLMs to translate logical reasoning problems in natural language into a symbolic representations and then used a symbolic logic solver to solve the problems deterministically.”
Toward Human-Aligned, Modular, and Emotion-Aware Multi-Agent Systems: A Systematic Literature ReviewPreprint
Ghanem, H., Cruz, C., & Cherifi, H. (2026) · Research Square · doi:10.21203/rs.3.rs-9485421/v1
When the Chain Breaks: Interactive Diagnosis of LLM Chain‐of‐Thought Reasoning Errors
Chen, S., Sritharan, N., Wen, X., Zhang, C., Wang, X., & Wang, Y. (2026) · Computer Graphics Forum · doi:10.1111/cgf.70439
“Logical errors can be detected either via external symbolic solvers [Che25, PAWW23] or by prompting LLMs [XFP ∗ 24, MCK ∗ 25].”
Self-citationA Neurosymbolic Prolog Skill for LLM-Driven Service Placement
Massa, J., Bisicchia, G., Dazzi, P., et al. (2026) · IEEE ... International Conference on Cloud Computing · doi:10.1109/cloud72782.2026.00014
A Diagnostic Framework for Compositional Generalization via NL-to-FOL Translation
Deveci, İ. E. (2026) · Journal of Logic Language and Information · doi:10.1007/s10849-026-09480-0
OOWM: Structuring Embodied Reasoning and Planning via Object-Oriented Programmatic World Modeling
Chen, H., Lin, L., & Wang, G. (2026) · International Conference on Multimedia Retrieval · doi:10.1145/3805622.3810797 · Cited by 1
Implicit to Explicit: A Pipeline for Inter-Policy Conflict Detection in Data Ecosystems Governance
Hmimou, A., Jovanović, P., & Romero, O. (2026) · IEEE International Conference on Data Engineering Workshops (ICDEW) · doi:10.1109/icdew71238.2026.00025
“Similarly, Logic-LM [16] translates informal text into symbolic solvers.”
Alkhairy, M., Homer, V., & O'Connor, B. (2026) · Journal of Logic Language and Information · doi:10.1007/s10849-026-09481-z · Cited by 1
Ai, X., Yin, Y., Huang, Y., et al. (2026) · Journal of Engineering and Applied Science · doi:10.1186/s44147-026-01100-9
“Without the formal transition model ( M = ( Q, Σ , δ, q 0 , F ) ), the LLM’s False Positive rate increased by 28%, as it often hallucinated logical constraints [15] that did not exist in the actual code architecture.”
Beyond the Black Box—A New Vector for Explainable AI Through Comparative Analysis of Logical Systems
Gulyamov, S. S., Gulyamov, S. S., Rodionov, A., Rustambekov, I., & Хаётовна, М. М. (2026) · Information · doi:10.3390/info17080809
Neurosymbolic computer vision: a survey and perspective
Nicolau, M., Jung, C. R., & Lamb, L. C. (2026) · Neural Computing and Applications · doi:10.1007/s00521-026-12063-6 · Cited by 2
LLM-COGNICA: Towards Reliable Agent Decision Making
Koumi, A., & Kakas, A. C. (2026) · IFIP advances in information and communication technology · doi:10.1007/978-3-032-30801-6_7
A Survey on Agentic AI Approaches for Unifying Knowledge Graphs and Large Language Models
Tiwari, S., Amara, F. Z., Hammaz, M., Chand, B., Khorashadizadeh, H., Groppe, S., Sahri, S., Mihindukulasooriya, N., Groppe, J., & Benamara, F. (2026) · Lecture notes in computer science · doi:10.1007/978-981-92-2014-4_39
Large Language Models as Tools for Symbolic Discovery and Analysis of Nonlinear Dynamical Systems
VOLOS, C. K., & Li, C. (2026) · International Journal of Bifurcation and Chaos · doi:10.1142/s0218127426501944
Takedato, T., & Kato, T. (2026) · IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW) · doi:10.1109/icstw72326.2026.00030
“Research on universal automatic generation of SMT formulas from DSLs using LLMs includes Logic-LM [10], LLMLift [11], EMUR [12], CloudFix [13], and ARC (Automated Reasoning Checks) [14].”
Pant, Y. R., Adarbah, H. Y., Afzel Noore, B., Che, D., Ahmed, A., & Ayala, R. (2026) · AI · doi:10.3390/ai7080280
Wang, Y., Seggoju, R. H., & Paschke, A. (2026) · Neurosymbolic Artificial Intelligence · doi:10.1177/29498732261469484
From Gameplay Traces to Game Mechanics: Causal Induction with Large Language Models
Jiwatode, M., Dockhorn, A., & Rosenhahn, B. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-31927-2_1
SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification
Cui, W., Zhang, H., Huang, Y., Li, Q., Xu, J. H., Liu, C., Gao, C., Wang, J., & Zhang, B. (2026) · ACM SIGKDD Conference on Knowledge Discovery and Data Mining (KDD) · doi:10.1145/3770855.3818004
A neuro-symbolic approach to translate English to logic and ontology
Pease, A., & Thompson, R. (2026) · Frontiers in Artificial Intelligence · doi:10.3389/frai.2026.1820380
Reconstructing TensorLog for Scalable End-to-End Rule Learning
Qi, K., Du, J., Wan, H., & Wang, W. (2026) · IEEE International Conference on Data Engineering (ICDE) · doi:10.1109/icde65706.2026.00089
“Recently, several studies [16]–[20] have explored leveraging logical rules to enhance the reasoning abilities of LLMs. Specifically, they enhance LLMs with KGs and logical rules by constructing rule-guided prompts [17]– [21] or applying symbolic solvers [16], [21].”
Self-citationPandžić, S., Dijkshoorn, F., & Broersen, J. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-22820-8_6
Wang, Z., Zhang, H., Hou, J., & Zheng, S. (2026) · International Conference on Electronics and Communication, Network and Computer Technology (ECNCT) · doi:10.1109/ecnct70535.2026.11661501
“Pairing a model with a symbolic solver, as Logic-LM [16] does for logical reasoning, recovers much of what the model alone gets wrong.”
Fusion Rush: Enhancing Proficiency in Boolean Logic Algebra through Gamification
Bascug, F. M. F. G., Gemina, R. B., Mendoza, B. X. B., Arellano, C. N., & Laviste, R. P. (2026) · International Conference on Education and Training Technologies (ICETT) · doi:10.1109/icett70124.2026.11665957
“Pan et al. [11] demonstrated that integrating large language models with symbolic solvers can significantly enhance a learner's deductive skills.”
Neurosymbolic Large Language Models: A Survey of Symbolic Integration, Reasoning and Explainability
Rani, M., Mishra, B. K., & Thakker, D. (2026) · Information Systems Frontiers · doi:10.1007/s10796-026-10794-4 · Cited by 2
Vassilis Sioros at Sci-ImageMiner 2026 Tasks 2, 3, and 4
Sioros, V. (2026) · Open Conference Proceedings · doi:10.52825/ocp.v10i.3511
“In language-centric reasoning pipelines, Logic-LM and NL2LOGIC show that coupling LLM generation with symbolic constraints/solvers can improve faithfulness and syntactic validity, with evaluations tied to FOLIO -style logical reasoning settings [7], [8], [9], [10], [11].”
Proof-Carrying Neuro-Symbolic Reasoning for Non-Monotonic Legal Decision Support with LLMs
Ulizko, M., Polevaya, T., Томилов, И. В., et al. (2026) · Big Data and Cognitive Computing · doi:10.3390/bdcc10090295
“Logic-LM and LINC established a modular pattern in which an LLM translates natural-language problems into a symbolic language and an external solver performs inference [19,20].”
Sun, Z., Wang, Z., Wei, S., et al. (2026) · doi:10.1145/3821966.3822043
GarmentoPIA: Generating Garment Pattern Models Using Intelligent Agents
Yeom, M., Shin, R., & Lee, S.-H. (2026) · Computational Visual Media · doi:10.26599/cvm.2026.9450567
Intent-Driven and Constraint-Verified Service Composition via Evolving Verified Experience
Ma, B., Liu, J., Ren, B., Luo, L., Guo, D., & Chen, H. (2026) · IEEE International Conference on Web Services (ICWS) · doi:10.1109/icws72778.2026.00168
“More recently, works such as Logic-LM [9] and [11] have introduced formal verification approaches for planning, translating queries into constraint satisfaction problems (CSPs) solvable by SMT solvers.”
EviGuard: Machine-Verifiable Evidence Grounding for LLM-Based Industrial Incident Reasoning
Zhou, H., Lei, H., & Yang, M. (2026) · Applied Sciences · doi:10.3390/app16188925
Zikas, S., Gkirtzou, K., Panagiotakopoulos, T., & Kiouvrekis, Y. (2026) · Machine Learning and Knowledge Extraction · doi:10.3390/make8090281
“Only Li et al. [133] simultaneously address both safety constraints (D3) and knowledge production (D4), suggesting that designing systems that both enforce safety and produce new symbolic knowledge remains an open challenge.”
Formal Verification of Robust IoT Systems
Quispe-Olmedo, L., Bárcenas, E., Pérez-Gaspar, M., et al. (2026) · Communications in computer and information science · doi:10.1007/978-3-032-37444-8_46
Crocetti, V., Pacioni, E., Dragoni, A. F., Schumacher, M., & Calvaresi, D. (2026) · Lecture notes in computer science · doi:10.1007/978-3-032-40774-0_17
Aksyonov, K. A., Sun, L., & Aksyonova, O. P. (2026) · International Russian Automation Conference (RusAutoCon) · doi:10.1109/rusautocon69876.2026.11707467
“Recent systems operationalize this pattern by translating natural-language problems into symbolic forms that are executed by deterministic solvers, thereby improving faithfulness and verifiability [29-31].”
Guo, M., Chen, C., Wang, T., & Cheng, L. (2026) · IEEE International Conference on Automation Science and Engineering (CASE) · doi:10.1109/case69030.2026.11704166
RefineAct: Automatic Runtime Verification of LLM Agent Actions
Batole, F., Khomh, F., & Rajan, H. (2026) · IEEE/ACM International Conference on Automated Software Engineering (ASE) · doi:10.1145/3832783.3834409
Arithmetic Reasoning with LLM: Prolog Generation & Permutation
Yang, X., Chen, B., & Tam, Y.-C. (2024) · arXiv · doi:10.48550/arxiv.2405.17893
“LLMs are hence adopted to generate symbolic representations from natural language (Lyu et al., 2023; Pan et al., 2023; Yang et al., 2023), where deterministic symbolic solvers will process the query and symbolic representations generated by LLMs to conduct reasoning or proofs.”
Background
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
