LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers

Theo OlaussonAlex GuBenjamin LipkinCedegao E. ZhangArmando Solar-LezamaJoshua B. TenenbaumRoger Levy

article2023EMNLP224 citationsOutstanding Paper Award

Proposes LINC, a neurosymbolic method that uses language models to translate natural language into first-order logic for external theorem provers, enabling a 15.5-billion-parameter model to outperform GPT-4 with chain-of-thought prompting on deductive reasoning benchmarks.

Listen

Large language models frequently struggle with sound deductive reasoning, often failing when handling negation, out-of-domain problems, and long deduction chains. When deployed in critical downstream applications such as automated theorem proving, knowledge discovery, and factual retrieval, these failures can cause severe hallucinations and logical errors. Existing prompting techniques, including Chain-of-Thought prompting, encourage models to verbalize reasoning steps but still suffer from unreliable deductive leaps.

The article evaluates a modular neurosymbolic framework named LINC (Logical Inference via Neurosymbolic Computation) to determine whether offloading deductive logic to an external symbolic engine improves natural language reasoning accuracy and robustness across diverse model scales.

The authors implemented a three-step neurosymbolic pipeline where a language model first acts as a semantic parser to translate natural language premises and conclusions into first-order logic. Second, an automated theorem prover executes symbolic deduction to determine if the conclusion is True, False, or Uncertain given the premises. Third, a 10-way majority voting sieve filters syntax errors and selects the most consistent outcome. The approach was evaluated against three standard in-context baselines (Naïve, Scratchpad, and Chain-of-Thought) across three models—StarCoder+ (15.5 billion parameters), GPT-3.5, and GPT-4—on both a naturalistic benchmark (FOLIO) and a synthetic benchmark (ProofWriter).

The evaluation revealed substantial performance advantages for neurosymbolic execution. On the synthetic ProofWriter dataset, LINC achieved near-perfect performance, reaching 96.4% with GPT-3.5 and 98.3% with GPT-4. Augmenting the smaller, open-source StarCoder+ with LINC yielded an accuracy of 82.5%, outperforming GPT-3.5 and GPT-4 using Chain-of-Thought by 38 and 10 percentage points, respectively. Unlike standard prompting baselines whose performance degraded toward random chance as proof depth increased, LINC maintained near-ceiling accuracy across all proof depths. On the naturalistic FOLIO dataset, LINC improved StarCoder+ accuracy from 41.8% to 56.0% and GPT-3.5 from 54.9% to 62.6%, while performing comparably to Chain-of-Thought on GPT-4 (72.5% versus 75.3%, a difference found to be statistically insignificant). An error analysis revealed that LINC and Chain-of-Thought exhibit distinctly complementary failure modes: Chain-of-Thought suffers from logical fallacies and reasoning breakdowns, whereas LINC maintains a higher precision on True/False predictions (93% versus 81%) but experiences lower recall due to occasional information loss or syntax errors during semantic parsing.

These findings demonstrate that separating language parsing from logical deduction significantly reduces overconfidence and logical errors in language models. Neurosymbolic architectures enable smaller, lower-cost open-source models to match or exceed the reasoning performance of significantly larger proprietary models on structured deduction tasks.

Organizations developing automated reasoning systems should consider adopting hybrid neurosymbolic architectures where language models parse domain text into formal representations and symbolic solvers execute the deduction. To maximize reliability, developers should investigate techniques such as constrained grammar generation to eliminate syntax errors, forward-backward translation validation to reduce information loss, and hybrid pipelines that combine neurosymbolic precision with natural language fallback reasoning.

Readers should note that the evaluation is confined to first-order logic on relatively short premise statements and does not account for higher-order logics or non-classical reasoning. Additionally, executing multi-sample majority voting incurs non-trivial computational and API costs, and theorem proving on massive premise sets may face NP-hard scaling constraints. Despite these boundaries, there is high confidence that neurosymbolic integration provides a robust, scalable foundation for automated deductive reasoning.

Massachusetts Institute of Technology first order logic inference language model first-order logic provers neurosymbolic computation logical reasoning

arXiv: 2310.15164 benlipkin/linc

Paper: PAL: Program-aided Language Models, Luyu Gao et al. (2023). PAL introduces the paradigm of offloading intermediate reasoning and computation from language models to external programmatic engines, establishing the conceptual blueprint that LINC adapts to first-order logic provers.
Paper: Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks, Wenhu Chen et al. (2022). This paper establishes the foundational concept of disentangling language model reasoning from deterministic computation via external program interpreters, motivating LINC's neurosymbolic modular architecture.
Paper: Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought, Abulhair Saparov et al. (2023). By formally showing how chain-of-thought prompting breaks down during multi-step proof planning despite local validity, this work directly motivates offloading symbolic deduction to dedicated provers as done in LINC.
Paper: Chain-of-Thought Prompting Elicits Reasoning in Large Language Models, Jason Wei et al. (2022). It introduces chain-of-thought prompting, the primary baseline prompting methodology against which LINC's neurosymbolic theorem-proving approach is directly compared and evaluated.
Paper: Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanations, Jaehun Jung et al. (2022). This paper explores coupling LLM-generated explanations with formal satisfiability solvers to enforce consistency, serving as an important conceptual precursor to LINC's theorem-prover integration.
Paper: Language Models of Code are Few-Shot Commonsense Learners, Aman Madaan et al. (2022). This work demonstrates the effectiveness of code-pretrained language models for structured formal generation, underpinning LINC's reliance on models like StarCoder+ for semantic parsing into logic.

Paper: Fact-Checking Complex Claims with Program-Guided Reasoning, Liangming Pan et al. (2023). Extends neurosymbolic decomposition by translating complex multi-hop natural language claims into modular reasoning programs executed across specialized sub-modules.
Paper: LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks, Po-Nien Kung et al. (2026). Applies modular informal-to-formal parsing and external symbolic verification to competition-level mathematical theorem proving using the Lean environment.
Paper: Efficient Rectification of Neuro-Symbolic Reasoning Inconsistencies by Abductive Reflection, Wen-Chao Hu et al. (2025). Builds on neurosymbolic error handling by introducing an abductive reflection layer to identify and rectify logical inconsistencies between neural outputs and symbolic rules.
Paper: Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2, Yuri Chervonyi et al. (2025). Demonstrates an advanced neurosymbolic architecture that combines specialized neural parsing with a dedicated deduction engine to solve complex formal proofs.
Paper: ReCEval: Evaluating Reasoning Chains via Correctness and Informativeness, Archiki Prasad et al. (2023). Provides a reference-free framework to evaluate the step-by-step logical correctness and validity of intermediate natural language reasoning chains.

Cover for LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers

Abstract

Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available at this https URL

Topics

first order logic inference language model large language models reasoning theorem provers probabilistic inference

Keywords

first-order logic provers neurosymbolic computation logical reasoning language models deductive reasoning theorem provers symbolic solver semantic parser

1 Introduction
2 LINC: Logical Inference via Neurosymbolic Computation
3 Experiments
4 Results & Discussion
5 Error Analysis
5.1 Qualitative Analysis
5.2 Quantitative Analysis
6 Related Work
7 Conclusion
8 Limitations
9 Acknowledgements
References
A Future Directions
B Model Details and Parameters
C FOLIO Dataset Preprocessing
D FOLIO Few-Shot Prompts
D.1 FOLIO, 1-shot (baseline)
D.2 FOLIO, 1-shot (scratchpad)
D.3 FOLIO, 1-shot (chain of thought)
D.4 FOLIO, 1-shot (neurosymbolic)
E FOLIO Error Analysis
E.1 Ambiguity of “Either” statements
E.2 GPT-4 LINC Failure Modes
E.3 GPT-4 CoT Failure Modes
E.4 Shared mistakes between GPT-4 CoT and LINC
F Proofwriter StarCoder+ Errors
G StarCoderPlus FOLIO Error Analysis
H The effect of KK-way majority voting on LINC and CoT

Knowls

Knowl 1 — LINC Neurosymbolic Reasoning Architecture
model/method
LINC (Logical Inference via Neurosymbolic Computation) is a modular, two-stage neurosymbolic framework designed to perform deductive logical reasoning over natural language statements without requiring the language model itself to carry out deductive steps.

The framework operates in two main stages followed by a sample aggregation procedure:
1. Semantic Parsing (Natural Language to FOL): Given a set of natural language premises and a candidate conclusion, an autoregressive large language model (LLM) acts as a semantic parser. Conditioned on few-shot in-context examples, the LLM translates each natural language statement into a first-order logic (FOL) expression formatted for automated theorem provers (specifically adhering to the Python NLTK logic package syntax).
2. Symbolic Automated Theorem Proving: The formalized logic expressions are parsed from the LLM output and offloaded to an external symbolic theorem prover (Prover9). The prover algorithmically checks whether the formalized conclusion follows deductively from the premises, returning an output from the discrete set $\{\text{True}, \text{False}, \text{Uncertain}\}$ . If the generated expressions violate FOL syntax or arity constraints, the solver raises an exception, yielding an output of $\text{Error}$ .
3. $K$ -Way Majority Voting: To mitigate syntax and semantic formalization errors, $K$ candidate logic formalizations are sampled independently at a decoding temperature of $T > 0$ . Each parse is executed in the prover, syntax errors are filtered out, and a majority vote across the remaining valid symbolic outputs determines the final prediction. In case of ties, the earliest generated valid label is chosen.

Knowl 2 — Benchmark Reasoning Accuracy of LINC across Models and Datasets

data/table

The reasoning performance of LINC was benchmarked against three prompting baselines (Naïve direct prediction, Scratchpad logic generation without an external solver, and natural language Chain-of-Thought (CoT)) across three language models: StarCoder+ (15.5B parameters), GPT-3.5 (gpt-3.5-turbo-16k-0613), and GPT-4 (gpt-4-0613). Evaluations used $K=10$ -way majority voting at decoding temperature $T = 0.8$ across 182 cleaned validation instances of the naturalistic FOLIO benchmark and 360 balanced instances of the synthetic ProofWriter benchmark under the Open-World Assumption (depths 0–5; 120 each of True/False/Uncertain).

Dataset	Model	Naïve (%)	Scratchpad (%)	CoT (%)	LINC (ours) (%)
FOLIO	StarCoder+ (15.5B)	34.6	32.4	41.8	56.0
FOLIO	GPT-3.5	48.4	47.8	54.9	62.6
FOLIO	GPT-4	69.8	68.7	75.3	72.5
ProofWriter	StarCoder+ (15.5B)	37.8	38.1	38.6	82.5
ProofWriter	GPT-3.5	36.4	33.1	43.6	96.4
ProofWriter	GPT-4	53.1	55.8	72.2	98.3

On FOLIO, LINC yields the largest improvement on smaller models (StarCoder+ +14.2% over CoT; GPT-3.5 +7.7% over CoT). On GPT-4, the difference between LINC (72.5%) and CoT (75.3%) is not statistically significant (McNemar's test $p = 0.58$ ). On ProofWriter, LINC produces massive improvements across all models, enabling StarCoder+ (82.5%) to outperform GPT-3.5 + CoT (43.6%) and GPT-4 + CoT (72.2%).

Knowl 3 — Scratchpad Ablation and the Necessity of External Symbolic Solvers
empirical result
The Scratchpad baseline serves as an ablation of LINC: the model is prompted to first generate first-order logic (FOL) expressions corresponding to the premises and conclusion, but the label (True/False/Uncertain) is generated directly by the LLM itself rather than calling the external symbolic prover (Prover9).

Across all tested models and datasets, generating intermediate FOL representations without an external solver yields no significant performance gain over the Naïve baseline (which predicts labels directly without any intermediate formalization):
- On FOLIO: StarCoder+ scores 32.4% on Scratchpad vs. 34.6% on Naïve; GPT-3.5 scores 47.8% on Scratchpad vs. 48.4% on Naïve; GPT-4 scores 68.7% on Scratchpad vs. 69.8% on Naïve.
- On ProofWriter: StarCoder+ scores 38.1% on Scratchpad vs. 37.8% on Naïve; GPT-3.5 scores 33.1% on Scratchpad vs. 36.4% on Naïve; GPT-4 scores 55.8% on Scratchpad vs. 53.1% on Naïve.
These findings demonstrate that language models cannot reliably execute deductive inference over intermediate formal logic expressions autoregressively; the performance gains of neurosymbolic architectures depend strictly on delegating deduction to the external symbolic solver.
Knowl 4 — Robustness of Deductive Reasoning Across Proof Depths on ProofWriter
empirical result
Evaluating deductive reasoning as a function of ground-truth proof depth (ranging from depth 0 to depth 5, with 50 samples per depth and random guessing chance equal to $33.3\%$ ) on ProofWriter reveals divergent scaling dynamics between in-context reasoning and neurosymbolic computation:
- In-Context Baselines (Naïve, Scratchpad, CoT): For StarCoder+, all baselines remain flat near random chance across all depths. For GPT-3.5, baselines perform above chance only at depth 0 (immediate conclusions), dropping to chance level ( $\,\approx 33.3\%$ ) for depths 1 through 5, with CoT completing some depth-1 tasks before degrading to chance. For GPT-4, baselines perform well on shallow proofs (depths 0–1), but accuracy steadily deteriorates as proof depth increases.
- LINC: When paired with GPT-3.5 or GPT-4, LINC achieves near-perfect ceiling accuracy ( $\,\approx 96\%\text{--}98\%$ ) consistently across all proof depths from 0 to 5 without degradation. For StarCoder+, LINC sustains accuracy far above chance across all depths, exhibiting only minor degradation at higher depths due to the syntactic challenges of translating longer sets of premises into FOL.
Knowl 5 — Taxonomy of Failure Modes in Neurosymbolic vs Chain-of-Thought Logical Reasoning
empirical result
Qualitative analysis of GPT-4 on the FOLIO dataset demonstrates that neurosymbolic reasoning (LINC) and natural language Chain-of-Thought (CoT) fail through completely distinct and non-overlapping mechanisms.

LINC Failure Modes
- L1 (Omission of Implicit Information): Natural language deduction often relies on implicit common-sense premises (e.g., that an individual named Harry is an instance of Person(x)). When the LLM omits these implicit facts from the FOL translation, Prover9 cannot bridge the logical gap and returns Uncertain.
- L2 (Inadequate/Lossy Representation): Explicit information is translated into FOL in a way that discards logical structure or atomicity (e.g., formalizing 'Heinrich Schmidt was a Nazi German politician' as a monolithic predicate NaziGermanPolitician(HeinrichSchmidt), which prevents deducing German(HeinrichSchmidt)), or using mismatched predicate names across premises (e.g., FourSided(x) vs. FourSides(x)).
- L3 (Syntax and Arity Violations): The LLM generates invalid FOL expressions that fail prover compilation (e.g., using the same symbol with multiple arities, such as Summer/1 and Summer/0). Unfiltered syntax error rates are 38% for StarCoder+, 24% for GPT-3.5, and 13% for GPT-4.
Chain-of-Thought Failure Modes
- C1 (Inconsistent/Contradictory Conclusion): The generated reasoning steps verbalize uncertainty or lack of evidence, but the model outputs False instead of Uncertain.
- C2 (Formal Logical Deductive Fallacies): The verbal chain commits classical deductive errors, most commonly the fallacy of affirming the consequent (deducing $A$ from $B$ given $A \to B$ ).
- C3 (Breakdown on Complex Reasoning Paths): The model gets lost, enters cyclical loops, or fails to execute multi-step contrapositive or resolution steps on complex proofs.
Knowl 6 — Precision-Recall Discrepancy and Prediction Distributions in LINC vs CoT
empirical result
Analysis of the confusion matrices of GPT-4 on FOLIO reveals marked distributional and precision differences between LINC and Chain-of-Thought (CoT):
- Predicted Label Distribution: CoT predictions are distributed as 32% True, 27% False, and 41% Uncertain. In contrast, LINC predicts 24% True, 17% False, 57% Uncertain, and 2% Error.
- High Precision on Definite Labels: Because the natural language to first-order logic translation is lossy (omitting necessary implicit or explicit premises), missing information typically renders the theorem prover unable to derive a proof, collapsing the prediction to Uncertain rather than introducing false deductions. Consequently, LINC achieves 93% precision on True and False predictions compared to 81% precision for CoT.
- Lower Recall on Definite Labels: Due to this conservative bias toward Uncertain, LINC achieves a recall of 60% on True and False ground-truth instances, whereas CoT achieves 75% recall.
Knowl 7 — Misprediction Similarity Metric and Method Discrepancy
equation
To quantify the correlation and behavioral overlap between the errors made by different reasoning techniques, the pairwise misprediction similarity metric $\text{sim}_D(A, B)$ is defined for two methods $A$ and $B$ over a dataset $D$ containing $N$ examples with ground-truth labels $\{R_i\}_{i=1}^N$ and predictions $\{A_i\}_{i=1}^N, \{B_i\}_{i=1}^N$ as:

$\text{sim}_D(A, B) \triangleq \frac{\sum_{i=1}^N \mathbf{1}[A_i = B_i \neq R_i]}{\sum_{i=1}^N \mathbf{1}[A_i \neq R_i \lor B_i \neq R_i]}$

where $\mathbf{1}[\cdot]$ is the indicator function. The numerator counts instances where both methods make identical incorrect predictions, while the denominator counts instances where at least one method fails.

On the FOLIO dataset with GPT-4:
- Similarity among pure in-context baselines is high: $\text{sim}_D(\text{CoT}, \text{Scratchpad}) = 0.54$ $\text{sim}_D(\text{CoT}, \text{Naïve}) = 0.52$ $\text{sim}_D(\text{Scratchpad}, \text{Naïve}) = 0.56$
- Similarity between LINC and each in-context baseline is low: $\text{sim}_D(\text{LINC}, \text{CoT}) = 0.22$ $\text{sim}_D(\text{LINC}, \text{Scratchpad}) = 0.21$ $\text{sim}_D(\text{LINC}, \text{Naïve}) = 0.14$
Out of 74 cases where either GPT-4 + CoT or GPT-4 + LINC failed, only 21 errors were shared, of which 16 were caused by flawed dataset annotations in FOLIO, leaving only 5 shared errors on well-formed samples.
Knowl 8 — Impact of Sample Scaling via Majority Voting on Neurosymbolic vs Prompting Baselines
empirical result
Evaluating accuracy across $K \in \{1, 2, \dots, 10\}$ for $K$ -way majority voting at decoding temperature $T = 0.8$ shows distinct scaling dynamics between LINC and Chain-of-Thought on FOLIO:
- LINC: Accuracy increases monotonically and substantially as $K$ increases from 1 to 10 for all models. The gain is especially pronounced on weaker models (such as StarCoder+), where individual sampled generations frequently produce syntax or arity errors that cause Prover9 to return $\text{Error}$ . Majority voting over multiple independent parses effectively filters out uncompilable drafts and converges on valid FOL representations.
- Chain-of-Thought: Increasing $K$ from 1 to 10 yields flat performance with no significant accuracy gains on the FOLIO benchmark across StarCoder+, GPT-3.5, and GPT-4.
Knowl 9 — Validation Split Audit and Quality Filtering of FOLIO
experimental setup
The standard validation split of the FOLIO benchmark contains 204 natural language deductive reasoning instances. A systematic formal verification of the ground truth using Prover9 and manual checking identified that 22 instances ( $10.8\%$ ) are defective, leading to their removal to establish a clean evaluation split of 182 instances:
1. Unbalanced Parentheses: 4 samples (indices 3, 109, 110, 111) contain syntax errors with unbalanced parentheses in the ground-truth FOL statements.
2. Ground-Truth Label Discrepancy: 8 samples (indices 6, 28, 30, 48, 113, 115, 139, 140) have ground-truth FOL statements whose deduction in Prover9 directly contradicts the labeled ground-truth target.
3. Premise-FOL Count Mismatch: 10 samples (indices 10, 11, 12, 88, 106, 107, 108, 174, 175, 176) contain an unequal number of natural language premises and reference FOL translations.
Knowl 10 — Limitations of First-Order Neurosymbolic Reasoning
limitation
The LINC framework and first-order neurosymbolic deduction exhibit several structural limitations:
1. Structural Input Format Restrictions: LINC assumes short, discrete, segmented premise-conclusion statements. When inputs are provided as unsegmented paragraphs (e.g., long context question answering), formalization difficulty increases significantly due to multiple valid translations and heavy reliance on pragmatic inferences.
2. Expressivity of First-Order Logic: Classical first-order logic (FOL) cannot express higher-order logic constructs or non-classical logics (e.g., modal, temporal, or intuitionistic logic) required in complex natural language semantics without changing the underlying formalism and symbolic reasoner.
3. Computational Complexity: First-order logical theorem proving is undecidable in general and NP-hard for propositional fragments; provers may encounter exponential runtimes or fail to terminate on very large premise sets.
4. Failure Cascades from Lossy Formalization: Semantic parsing from natural language to FOL is lossy. A single omitted predicate, misnamed relation, or missed implicit common-ground assumption leads the symbolic prover to return Uncertain.

Coverage note — None was omitted; all contributed models, benchmark results, ablations, error taxonomies, mathematical formulations, majority voting dynamics, data preprocessing, and limitations are fully covered.

References

1.Cem Anil, Yuhuai Wu, Anders Andreassen, Aitor Lewkowycz, Vedant Misra, Vinay Ramasesh, Ambrose Slone, Guy Gur-Ari, Ethan Dyer, and Behnam Neyshabur. 2022. Exploring length generalization in large language models. In Advances in Neural Information Processing Systems, volume 35, pages 38546–38556. (Cited on pg. 1)
2.Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. 2023. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433. (Cited on pg. 9)
3.David Barker-Plummer, Jon Barwise, and John Etchemendy. 2011. Language, proof, and logic, 2 edition. Center for the Study of Language and Information. (Cited on pg. 2)
4.Mohammad Bavarian, Heewoo Jun, Nikolas Tezak, John Schulman, Christine McLeavey, Jerry Tworek, and Mark Chen. 2022. Efficient training of language models to fill in the middle. arXiv preprint arXiv:2207.14255. (Cited on pg. 15)
5.Jonathan Berant, Andrew Chou, Roy Frostig, and Percy Liang. 2013. Semantic parsing on Freebase from question-answer pairs. In Proceedings of the 2013 Conference on Empirical Methods in Natural Language Processing, pages 1533–1544, Seattle, Washington, USA. Association for Computational Linguistics. (Cited on pg. 8)
6.Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. 2020. Language models are few-shot learners. In Advances in neural information processing systems, volume 33, pages 1877–1901. (Cited on pg. 1, 4)
7.John P Burgess. 2009. Philosophical logic. Princeton University Press. (Cited on pg. 10)
8.Wenhu Chen, Xueguang Ma, Xinyi Wang, and William W Cohen. 2022. Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks. arXiv preprint arXiv:2211.12588. (Cited on pg. 10)
9.Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. 2023a. Teaching large language models to self-debug. arXiv preprint arXiv:2304.05128. (Cited on pg. 9)
10.Yongchao Chen, Rujul Gandhi, Yang Zhang, and Chuchu Fan. 2023b. NL2TL: Transforming natural languages to temporal logics using large language models. arXiv preprint arXiv:2305.07766. (Cited on pg. 9)
11.Zhoujun Cheng, Tianbao Xie, Peng Shi, Chengzu Li, Rahul Nadkarni, Yushi Hu, Caiming Xiong, Dragomir Radev, Mari Ostendorf, Luke Zettlemoyer, Noah A. Smith, and Tao Yu. 2023. Binding language models in symbolic languages. In The Eleventh International Conference on Learning Representations. (Cited on pg. 9)
12.Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, et al. 2022. Palm: Scaling language modeling with pathways. arXiv preprint arXiv:2204.02311. (Cited on pg. 1)
13.Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 2023. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In Computer Aided Verification, pages 383–396, Cham. Springer Nature Switzerland. (Cited on pg. 9)
14.Antonia Creswell, Murray Shanahan, and Irina Higgins. 2023. Selection-inference: Exploiting large language models for interpretable logical reasoning. In The Eleventh International Conference on Learning Representations. (Cited on pg. 1, 3, 8)
15.David Dohan, Winnie Xu, Aitor Lewkowycz, Jacob Austin, David Bieber, Raphael Gontijo Lopes, Yuhuai Wu, Henryk Michalewski, Rif A Saurous, Jascha Sohl-Dickstein, et al. 2022. Language model cascades. arXiv preprint arXiv:2207.10342. (Cited on pg. 8)
16.Iddo Drori, Sarah Zhang, Reece Shuttleworth, Leonard Tang, Albert Lu, Elizabeth Ke, Kevin Liu, Linda Chen, Sunny Tran, Newman Cheng, et al. 2022. A neural network solves, explains, and generates university math problems by program synthesis and few-shot learning at human level. Proceedings of the National Academy of Sciences, 119(32):e2123433119. (Cited on pg. 9)
17.Andrew Drozdov, Nathanael Schärli, Ekin Akyürek, Nathan Scales, Xinying Song, Xinyun Chen, Olivier Bousquet, and Denny Zhou. 2022. Compositional semantic parsing with large language models. arXiv preprint arXiv:2209.15003. (Cited on pg. 8)
18.Nouha Dziri, Ximing Lu, Melanie Sclar, Xiang Lorraine Li, Liwei Jian, Bill Yuchen Lin, Peter West, Chandra Bhagavatula, Ronan Le Bras, Jena D Hwang, et al. 2023. Faith and fate: Limits of transformers on compositionality. arXiv preprint arXiv:2305.18654. (Cited on pg. 1)
19.Monireh Ebrahimi, Aaron Eberhart, Federico Bianchi, and Pascal Hitzler. 2021. Towards bridging the neuro-symbolic gap: Deep deductive reasoners. Applied Intelligence, 51:6326–6348. (Cited on pg. 8)
20.Herbert B Enderton. 2001. A mathematical introduction to logic. Elsevier. (Cited on pg. 2)
21.Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. 2023. PAL: Program-aided language models. In International Conference on Machine Learning, pages 10764–10799. PMLR. (Cited on pg. 9, 10)
22.Herbert P Grice. 1975. Logic and conversation. In Speech acts, pages 41–58. Brill. (Cited on pg. 15)
23.Christopher Hahn, Frederik Schmitt, Julia J Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. 2022. Formal specifications from natural language. arXiv preprint arXiv:2206.01962. (Cited on pg. 9)
24.Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Luke Benson, Lucy Sun, Ekaterina Zubova, Yujie Qiao, Matthew Burtell, et al. 2022. Folio: Natural language reasoning with first-order logic. arXiv preprint arXiv:2209.00840. (Cited on pg. 3)
25.James Higginbotham. 1998. On higher-order logic and natural language. In Proceedings of the British Academy, volume 95, pages 1–27. (Cited on pg. 10)
26.Jie Huang and Kevin Chen-Chuan Chang. 2022. Towards reasoning in large language models: A survey. arXiv preprint arXiv:2212.10403. (Cited on pg. 1)
27.Jie Huang, Xinyun Chen, Swaroop Mishra, Huaixiu Steven Zheng, Adams Wei Yu, Xinying Song, and Denny Zhou. 2023. Large language models cannot self-correct reasoning yet. arXiv preprint arXiv:2310.01798. (Cited on pg. 10)
28.Borja Ibarz, Vitaly Kurin, George Papamakarios, Kyriacos Nikiforou, Mehdi Bennani, Róbert Csordás, Andrew Joseph Dudzik, Matko Bošnjak, Alex Vitvitskyi, Yulia Rubanova, et al. 2022. A generalist neural algorithmic learner. In Learning on Graphs Conference, pages 2–1. PMLR. (Cited on pg. 8)
29.Aishwarya Kamath and Rajarshi Das. 2019. A survey on semantic parsing. In Automated Knowledge Base Construction (AKBC). (Cited on pg. 8)
30.Mehran Kazemi, Najoung Kim, Deepti Bhatia, Xin Xu, and Deepak Ramachandran. 2023. LAMBADA: Backward chaining for automated reasoning in natural language. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 6547–6568, Toronto, Canada. Association for Computational Linguistics. (Cited on pg. 8)
31.Denis Kocetkov, Raymond Li, Loubna Ben Allal, Jia Li, Chenghao Mou, Carlos Muñoz Ferrandis, Yacine Jernite, Margaret Mitchell, Sean Hughes, Thomas Wolf, et al. 2022. The Stack: 3 TB of permissively licensed source code. arXiv preprint arXiv:2211.15533. (Cited on pg. 15)
32.Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. 2022. Large language models are zero-shot reasoners. In Advances in neural information processing systems, volume 35, pages 22199–22213. (Cited on pg. 1, 4, 8)
33.Raymond Li, Loubna Ben Allal, Yangtian Zi, Niklas Muennighoff, Denis Kocetkov, Chenghao Mou, Marc Marone, Christopher Akiki, Jia Li, Jenny Chim, et al. 2023. Starcoder: may the source be with you! arXiv preprint arXiv:2305.06161. (Cited on pg. 4, 15)
34.Percy Liang, Rishi Bommasani, Tony Lee, Dimitris Tsipras, Dilara Soylu, Michihiro Yasunaga, Yian Zhang, Deepak Narayanan, Yuhuai Wu, Ananya Kumar, et al. 2022. Holistic evaluation of language models. arXiv preprint arXiv:2211.09110. (Cited on pg. 1)
35.Percy Liang, Michael I Jordan, and Dan Klein. 2013. Learning dependency-based compositional semantics. Computational Linguistics, 39(2):389–446. (Cited on pg. 8)
36.Ruibo Liu, Jason Wei, Shixiang Shane Gu, Te-Yen Wu, Soroush Vosoughi, Claire Cui, Denny Zhou, and Andrew M. Dai. 2023. Mind’s eye: Grounded language model reasoning through simulation. In The Eleventh International Conference on Learning Representations. (Cited on pg. 9)
37.Xuantao Lu, Jingping Liu, Zhouhong Gu, Hanwen Tong, Chenhao Xie, Junyang Huang, Yanghua Xiao, and Wenguang Wang. 2022. Parsing natural language into propositional and first-order logic with dual reinforcement learning. In Proceedings of the 29th International Conference on Computational Linguistics, pages 5419–5431. (Cited on pg. 8)
38.Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, et al. 2023. Self-refine: Iterative refinement with self-feedback. arXiv preprint arXiv:2303.17651. (Cited on pg. 9)
39.Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester, and Luc De Raedt. 2018. DeepProbLog: Neural probabilistic logic programming. In Advances in neural information processing systems, volume 31. (Cited on pg. 8)
40.Giuseppe Marra, Francesco Giannini, Michelangelo Diligenti, and Marco Gori. 2019. Integrating learning and reasoning with deep logic models. In Joint European Conference on Machine Learning and Knowledge Discovery in Databases, pages 517–532. Springer. (Cited on pg. 8)
41.W. McCune. 2005–2010. Prover9 and mace4. |http://www.cs.unm.edu/ mccune/prover9/|. (Cited on pg. 3)
42.Ian McKenzie, Alexander Lyzhov, Alicia Parrish, Ameya Prabhu, Aaron Mueller, Najoung Kim, Sam Bowman, and Ethan Perez. 2022. The inverse scaling prize. (Cited on pg. 1)
43.Quinn McNemar. 1947. Note on the sampling error of the difference between correlated proportions or percentages. Psychometrika, 12(2):153–157. (Cited on pg. 5)
44.Grégoire Mialon, Roberto Dessì, Maria Lomeli, Christoforos Nalmpantis, Ram Pasunuru, Roberta Raileanu, Baptiste Rozière, Timo Schick, Jane Dwivedi-Yu, Asli Celikyilmaz, et al. 2023. Augmented language models: a survey. arXiv preprint arXiv:2302.07842. (Cited on pg. 9)
45.Dale A. Miller and Gopalan Nadathur. 1986. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting on Association for Computational Linguistics, page 247–256, New York, USA. Association for Computational Linguistics. (Cited on pg. 10)
46.Maxwell Nye, Anders Johan Andreassen, Guy Gur-Ari, Henryk Michalewski, Jacob Austin, David Bieber, David Dohan, Aitor Lewkowycz, Maarten Bosma, David Luan, et al. 2021. Show your work: Scratchpads for intermediate computation with language models. arXiv preprint arXiv:2112.00114. (Cited on pg. 1, 4, 8)
47.Theo X Olausson, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao, and Armando Solar-Lezama. 2023. Is self-repair a silver bullet for code generation? arXiv preprint arXiv:2306.09896. (Cited on pg. 9)
48.OpenAI. 2023. GPT-4 technical report. (Cited on pg. 1, 4, 15)
49.Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, et al. 2022. Training language models to follow instructions with human feedback. In Advances in Neural Information Processing Systems, volume 35, pages 27730–27744. (Cited on pg. 4, 15)
50.Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. 2023. Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. arXiv preprint arXiv:2305.12295. (Cited on pg. 9)
51.Guilherme Penedo, Quentin Malartic, Daniel Hesslow, Ruxandra Cojocaru, Alessandro Cappelli, Hamza Alobeidli, Baptiste Pannier, Ebtesam Almazrouei, and Julien Launay. 2023. The RefinedWeb dataset for Falcon LLM: outperforming curated corpora with web data, and web data only. arXiv preprint arXiv:2306.01116. (Cited on pg. 15)
52.Baolin Peng, Michel Galley, Pengcheng He, Hao Cheng, Yujia Xie, Yu Hu, Qiuyuan Huang, Lars Liden, Zhou Yu, Weizhu Chen, and Jianfeng Gao. 2023. Check your facts and try again: Improving large language models with external knowledge and automated feedback. arXiv preprint arXiv:2302.12813. (Cited on pg. 9)
53.Gabriel Poesia, Alex Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. 2022. Synchromesh: Reliable code generation from pre-trained language models. In International Conference on Learning Representations. (Cited on pg. 15)
54.Graham Priest. 2008. An introduction to non-classical logic: From if to is. Cambridge University Press. (Cited on pg. 10)
55.Abulhair Saparov, Richard Yuanzhe Pang, Vishakh Padmakumar, Nitish Joshi, Seyed Mehran Kazemi, Najoung Kim, and He He. 2023. Testing the general deductive reasoning capacity of large language models using ood examples. arXiv preprint arXiv:2305.15269. (Cited on pg. 1)
56.Timo Schick, Jane Dwivedi-Yu, Roberto Dessì, Roberta Raileanu, Maria Lomeli, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. 2023. Toolformer: Language models can teach themselves to use tools. arXiv preprint arXiv:2302.04761. (Cited on pg. 2, 9)
57.Noam Shazeer. 2019. Fast transformer decoding: One write-head is all you need. arXiv preprint arXiv:1911.02150. (Cited on pg. 15)
58.Richard Shin and Benjamin Van Durme. 2022. Few-shot semantic parsing with language models trained on code. In Proceedings of the 2022 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, pages 5417–5425, Seattle, United States. Association for Computational Linguistics. (Cited on pg. 8)
59.Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, et al. 2023. Beyond the imitation game: Quantifying and extrapolating the capabilities of language models. Transactions on Machine Learning Research. (Cited on pg. 1)
60.Robert Stalnaker. 2002. Common ground. Linguistics and philosophy, 25(5/6):701–721. (Cited on pg. 15)
61.Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021. ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621–3634, Online. Association for Computational Linguistics. (Cited on pg. 3)
62.Oyvind Tafjord, Bhavana Dalvi Mishra, and Peter Clark. 2022. Entailer: Answering questions with faithful and truthful chains of reasoning. In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pages 2078–2093, Abu Dhabi, United Arab Emirates. Association for Computational Linguistics. (Cited on pg. 8)
63.Romal Thoppilan, Daniel De Freitas, Jamie Hall, Noam Shazeer, Apoorv Kulshreshtha, Heng-Tze Cheng, Alicia Jin, Taylor Bos, Leslie Baker, Yu Du, et al. 2022. LaMDA: Language models for dialog applications. arXiv preprint arXiv:2201.08239. (Cited on pg. 9)
64.Petar Veličković, Adrià Puigdomènech Badia, David Budden, Razvan Pascanu, Andrea Banino, Misha Dashevskiy, Raia Hadsell, and Charles Blundell. 2022. The clrs algorithmic reasoning benchmark. In International Conference on Machine Learning, pages 22084–22102. PMLR. (Cited on pg. 9)
65.Bailin Wang, Zi Wang, Xuezhi Wang, Yuan Cao, Rif A Saurous, and Yoon Kim. 2023a. Grammar prompting for domain-specific language generation with large language models. arXiv preprint arXiv:2305.19234. (Cited on pg. 8)
66.Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. 2020. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 85–98. (Cited on pg. 9)
67.Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. 2018. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11, pages 255–270. Springer. (Cited on pg. 9)
68.Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. 2023b. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations. (Cited on pg. 1, 3, 4, 8, 23)
69.Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, et al. 2022. Chain-of-thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems, volume 35, pages 24824–24837. (Cited on pg. 1, 4, 8)
70.Nathaniel Weir and Benjamin Van Durme. 2022. Dynamic generation of interpretable inference rules in a neuro-symbolic expert system. arXiv preprint arXiv:2209.07662. (Cited on pg. 9)
71.Lionel Wong, Gabriel Grand, Alexander K Lew, Noah D Goodman, Vikash K Mansinghka, Jacob Andreas, and Joshua B Tenenbaum. 2023. From word models to world models: Translating from natural language to the probabilistic language of thought. arXiv preprint arXiv:2306.12672. (Cited on pg. 8, 9)
72.Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. In Advances in Neural Information Processing Systems, volume 35, pages 32353–32368. (Cited on pg. 9)
73.Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Thomas L Griffiths, Yuan Cao, and Karthik Narasimhan. 2023. Tree of thoughts: Deliberate problem solving with large language models. arXiv preprint arXiv:2305.10601. (Cited on pg. 10)
74.Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. 2022. React: Synergizing reasoning and acting in language models. arXiv preprint arXiv:2210.03629. (Cited on pg. 9)
75.Michihiro Yasunaga, Xinyun Chen, Yujia Li, Panupong Pasupat, Jure Leskovec, Percy Liang, Ed H Chi, and Denny Zhou. 2023. Large language models as analogical reasoners. arXiv preprint arXiv:2310.01714. (Cited on pg. 10)
76.Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. Satisfiability-aided language models using declarative prompting. arXiv preprint arXiv:2305.09656. (Cited on pg. 9)
77.Eric Zelikman, Yuhuai Wu, Jesse Mu, and Noah Goodman. 2022. STaR: Bootstrapping reasoning with reasoning. In Advances in Neural Information Processing Systems, volume 35, pages 15476–15488. (Cited on pg. 8)
78.John M Zelle and Raymond J Mooney. 1996. Learning to parse database queries using inductive logic programming. In Proceedings of the National Conference on Artificial Intelligence, pages 1050–1055. (Cited on pg. 8)
79.Luke S Zettlemoyer and Michael Collins. 2005. Learning to map sentences to logical form: Structured classification with probabilistic categorial grammars. In Proceedings of the Twenty-First Conference on Uncertainty in Artificial Intelligence, UAI’05, page 658–666, Arlington, Virginia, USA. AUAI Press. (Cited on pg. 8)
80.Hanlin Zhang, Ziyang Li, Jiani Huang, Mayur Naik, and Eric Xing. 2022. Improved logical reasoning of language models via differentiable symbolic programming. In First Workshop on Pre-training: Perspectives, Pitfalls, and Paths Forward at ICML 2022. (Cited on pg. 9)
81.Honghua Zhang, Meihua Dang, Nanyun Peng, and Guy Van den Broeck. 2023a. Tractable control for autoregressive language generation. In International Conference on Machine Learning, pages 40932–40945. PMLR. (Cited on pg. 8)
82.Kechi Zhang, Zhuo Li, Jia Li, Ge Li, and Zhi Jin. 2023b. Self-edit: Fault-aware code editor for code generation. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 769–787, Toronto, Canada. Association for Computational Linguistics. (Cited on pg. 9)
83.Denny Zhou, Nathanael Schärli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Claire Cui, Olivier Bousquet, Quoc V Le, and Ed H Chi. 2023. Least-to-most prompting enables complex reasoning in large language models. In The Eleventh International Conference on Learning Representations. (Cited on pg. 8)

Citation

MLA

Olausson, T., et al. “LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers”. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, 2023, pp. 5153–76, https://doi.org/10.18653/v1/2023.emnlp-main.313.

APA

Olausson, T., Gu, A., Lipkin, B., Zhang, C., Solar-Lezama, A., Tenenbaum, J., & Levy, R. (2023). LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, 5153–5176. https://doi.org/10.18653/v1/2023.emnlp-main.313

Chicago

Olausson, T., A. Gu, B. Lipkin, et al. 2023. “LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers”. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, 5153–76. https://doi.org/10.18653/v1/2023.emnlp-main.313.

Harvard

Olausson, T. et al. (2023) “LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers”, Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics, pp. 5153–5176. Available at: https://doi.org/10.18653/v1/2023.emnlp-main.313.

Vancouver

1. Olausson T, Gu A, Lipkin B, Zhang C, Solar-Lezama A, Tenenbaum J, Levy R (2023) LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers. In: Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics, pp 5153–5176

BibTeX

@inproceedings{olausson-etal-2023-linc,
    title = "{LINC}: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers",
    author = "Olausson, Theo  and
      Gu, Alex  and
      Lipkin, Ben  and
      Zhang, Cedegao  and
      Solar-Lezama, Armando  and
      Tenenbaum, Joshua  and
      Levy, Roger",
    editor = "Bouamor, Houda  and
      Pino, Juan  and
      Bali, Kalika",
    booktitle = "Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing",
    month = dec,
    year = "2023",
    address = "Singapore",
    publisher = "Association for Computational Linguistics",
    url = "https://aclanthology.org/2023.emnlp-main.313/",
    doi = "10.18653/v1/2023.emnlp-main.313",
    pages = "5153--5176"
}

Metadata:ACL Anthology

Source Code

This paper has an official code repository available. Click below to access the source code.

View Repository

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF

License: https://creativecommons.org/licenses/by/4.0/

LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers

Abstract

Topics

Keywords

Table of Contents

Knowls

Knowl 1 — LINC Neurosymbolic Reasoning Architecture

Knowl 2 — Benchmark Reasoning Accuracy of LINC across Models and Datasets

Knowl 3 — Scratchpad Ablation and the Necessity of External Symbolic Solvers

Knowl 4 — Robustness of Deductive Reasoning Across Proof Depths on ProofWriter

Knowl 5 — Taxonomy of Failure Modes in Neurosymbolic vs Chain-of-Thought Logical Reasoning

LINC Failure Modes

Chain-of-Thought Failure Modes

Knowl 6 — Precision-Recall Discrepancy and Prediction Distributions in LINC vs CoT

Knowl 7 — Misprediction Similarity Metric and Method Discrepancy

Knowl 8 — Impact of Sample Scaling via Majority Voting on Neurosymbolic vs Prompting Baselines

Knowl 9 — Validation Split Audit and Quality Filtering of FOLIO

Knowl 10 — Limitations of First-Order Neurosymbolic Reasoning

References

Citation

BibTeX

Source Code

Access the Paper