A Balanced Neuro-Symbolic Approach for Commonsense Abductive Logic

TL;DR

ARGOS addresses commonsense abductive reasoning in logic problems by coupling a SAT-based solver with an open-ended LLM-driven generation of new background rules. It iteratively expands the problem with forward-chaining, two-literal antecedent rules, guided by backbone feedback from the solver and dual LLM scoring for commonsense and relevance. Across abductive variants of CLUTRR, FOLIO, ProntoQA and non-logical datasets, ARGOS achieves substantial improvements over purely neural or purely symbolic baselines, demonstrating robust performance when background knowledge is incomplete. The approach highlights the practical value of balancing neural and symbolic components, with open questions about scaling the search space and reducing reliance on logit-level access.

Abstract

Although Large Language Models (LLMs) have demonstrated impressive formal reasoning abilities, they often break down when problems require complex proof planning. One promising approach for improving LLM reasoning abilities involves translating problems into formal logic and using a logic solver. Although off-the-shelf logic solvers are in principle substantially more efficient than LLMs at logical reasoning, they assume that all relevant facts are provided in a question and are unable to deal with missing commonsense relations. In this work, we propose a novel method that uses feedback from the logic solver to augment a logic problem with commonsense relations provided by the LLM, in an iterative manner. This involves a search procedure through potential commonsense assumptions to maximize the chance of finding useful facts while keeping cost tractable. On a collection of pure-logical reasoning datasets, from which some commonsense information has been removed, our method consistently achieves considerable improvements over existing techniques, demonstrating the value in balancing neural and symbolic elements when working in human contexts.

Figures (11)

• Figure 1: An example from a children's comprehension exercise booklet . Left: the problem phrased in human language. Right: the same problem translated to first-order-logic.
• Figure 2: Symbolic-Linguistic Spectrum depicting the positioning of LLM-Tres llm-tres, Logic-of-Thought lot, and Chain-of-Thought (COT) cot_wei_2022 relative to our approach.
• Figure 2: Ablations. We ablate elements of ARGOS: (i) the score thresholding, taking the first clause sampled at each iteration (ARGOS - No T), (ii) the backbone-tracking, generating prompts by randomly selecting two variables (ARGOS - No BB).
• Figure 3: ARGOS at a glance. See Section \ref{['sec:algorithm']} and Appendix \ref{['sec:algorithm-details']} for details. (A) Given a propositional logic problem, we iteratively augment the problem with new propositions until it is solvable. (B) We attempt to solve the problem both with a logic solver, and with self-consistency SC. (C) If we fail, we attempt to add additional commonsense propositions by combining literals from the backbone as antecedents, and generating a right-hand-side using an LLM. We test the proposition for commonsense and relevance using this same LLM, and add it to the pool if it passes the tests.
• Figure 4: Overview of ARGOS with the winter fox example. We iteratively add to the logic problem and query a logic solver to look for conflicts within the backbone compared to the query. Eventually, we find that $absorbs(white, sun)$ is $False$, contradicting the query.

Theorems & Definitions (2)

• Proposition 1
• proof