# Sound and Complete Neurosymbolic Reasoning with LLM-Grounded Interpretations

arXiv: https://arxiv.org/abs/2507.09751 · HTML: https://mlsanity.com/paper/2507.09751/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 24 of its 73 references that are in the map.
- First posted on arXiv 13 Jul 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 24 of 24)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [GPQA: A Graduate-Level Google-Proof Q&A Benchmark](https://mlsanity.com/paper/2311.12022/) (2023)
- [Language Models as Knowledge Bases?](https://mlsanity.com/paper/1909.01066/) (2019)
- [Language Models (Mostly) Know What They Know](https://mlsanity.com/paper/2207.05221/) (2022)
- [Large Language Monkeys: Scaling Inference Compute with Repeated Sampling](https://mlsanity.com/paper/2407.21787/) (2024)
- [Selective Classification for Deep Neural Networks](https://mlsanity.com/paper/1705.08500/) (2017)
- [LLMs-as-Judges: A Comprehensive Survey on LLM-based Evaluation Methods](https://mlsanity.com/paper/2412.05579/) (2024)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Measuring short-form factuality in large language models](https://mlsanity.com/paper/2411.04368/) (2024)
- [Chain-of-Verification Reduces Hallucination in Large Language Models](https://mlsanity.com/paper/2309.11495/) (2023)
- [Survey on Factuality in Large Language Models: Knowledge, Retrieval and Domain-Specificity](https://mlsanity.com/paper/2310.07521/) (2023)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [HalluLens: LLM Hallucination Benchmark](https://mlsanity.com/paper/2504.17550/) (2025)
- [The FACTS Grounding Leaderboard: Benchmarking LLMs' Ability to Ground Responses to Long-Form Input](https://mlsanity.com/paper/2501.03200/) (2025)
- [Empowering LLMs with Logical Reasoning: A Comprehensive Survey](https://mlsanity.com/paper/2502.15652/) (2025)
- [SynLogic: Synthesizing Verifiable Reasoning Data at Scale for Learning Logical Reasoning and Beyond](https://mlsanity.com/paper/2505.19641/) (2025)
- [Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpus](https://mlsanity.com/paper/2411.12498/) (2024)
- [VERUS-LM: a Versatile Framework for Combining LLMs with Symbolic Reasoning](https://mlsanity.com/paper/2501.14540/) (2025)
- [Exploring Self-supervised Logic-enhanced Training for Large Language Models](https://mlsanity.com/paper/2305.13718/) (2023)
- [Investigating the Robustness of Deductive Reasoning with Large Language Models](https://mlsanity.com/paper/2502.04352/) (2025)

## Built on by (most cited first, 4 of 4)

- [Evaluating Confidence-Gated Retrieval with Matched Trajectory Replay](https://mlsanity.com/paper/2608.26846/) (2026)
- [AtomEval: Validity-Aware Atomic Evaluation of Adversarial Claim Rewriting in Fact Verification](https://mlsanity.com/paper/2604.07967/) (2026)
- [Agentic Interpretation: Lattice-Structured Evidence for LLM-Based Program Analysis](https://mlsanity.com/paper/2605.12694/) (2026)
- [Discourse-Aware Policy Analysis with Argumentation: A Hybrid LLM-Symbolic Framework for Disaster Governance](https://mlsanity.com/paper/2607.13260/) (2026)

## Abstract (arXiv)

Large language models (LLMs) have demonstrated impressive capabilities in natural language understanding and generation, but exhibit problems with logical consistency in their output. How can we harness LLMs' broad-coverage parametric knowledge in formal reasoning despite their inconsistency? We present a method for directly integrating an LLM into the interpretation function of the formal semantics for a paraconsistent logic. We evaluate the method empirically using datasets derived from the short-form factuality benchmarks GPQA and SimpleQA, showing that bilateral factuality evaluation improves macro-F1 over a unilateral baseline by roughly 6 percentage points on both benchmarks (at the cost of reduced coverage, as abstention is triggered on inconsistent or uncertain cases). We further describe a proof-of-concept tableau reasoner implementing the method, and apply it to a medication-safety knowledge base of 228 asserted and 712 inferred statements: the system detects 92 gluts corresponding to medically significant errors (e.g., opioids inferred as non-addictive, beta-blockers inferred as safe in asthma) while remaining satisfiable, demonstrating that contradictions are localized rather than causing logical explosion. Unlike prior work, our method offers a theoretical framework with a practical implementation for neurosymbolic reasoning that leverages an LLM's knowledge while preserving the underlying logic's soundness and completeness properties.