PEIRCE: Unifying Material and Formal Reasoning via LLM-Driven Neuro-Symbolic Refinement (2025.acl-demo)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) are capable of material inference but lack formal rigour and verifiability. |
| Approach: | They propose a framework to unify material and formal inference through an iterative conjecture–criticism process. |
| Outcome: | The proposed framework unifies material and formal inference through an iterative conjecture–criticism process. |
Similar Papers
Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition (2026.eacl-long)
Copied to clipboard
| Challenge: | Existing approaches to NLP are static and require manual formalization. |
| Approach: | They propose an adaptive, multi-paradigm, neuro-symbolic inference framework that automatically identifies formal reasoning strategies from problems expressed in natural language and dynamically selects and applies specialized formal logical solvers. |
| Outcome: | The proposed framework outperforms baselines on individual and multi-paradigm reasoning tasks by 17% and 6%. |
LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers (2023.emnlp-main)
Copied to clipboard
Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, Roger Levy
| Challenge: | Logical reasoning is an important task for artificial intelligence, says a new study . many prompting-based strategies to enable large language models fail in subtle and unpredictable ways. |
| Approach: | They propose to reformulate logical reasoning tasks by leveraging large language models . they use a modular neurosymbolic programming approach to translate premises and conclusions from natural language to logic . |
| Outcome: | The proposed approach outperforms open-source models on FOLIO and ProofWriter while showing distinct failure modes. |
Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement (2024.eacl-long)
Copied to clipboard
| Challenge: | Recent studies have focused on the application and evaluation of Large Language Models (LLMs) but LLMs are still prone to factual errors and inconsistencies in their explanations, offering limited control and interpretability for inference in complex domains. |
| Approach: | They propose an abductive-deductive framework that integrates Large Language Models with an external backward-chaining solver to refine step-wise natural language explanations. |
| Outcome: | The proposed framework improves explanations generated via in-context learning methods and Chain-of-Thought (CoT) on ethical NLI tasks while producing formal proofs describing and supporting models’ reasoning. |
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving (2024.emnlp-main)
Copied to clipboard
| Challenge: | Existing methods for assessing the validity of explanations for NLI are time-consuming and prone to logical errors. |
| Approach: | They propose a framework that integrates Large Language Models and Theorem Provers to verify and refine natural language explanations through crowd-sourcing . they propose to use TPs to generate and formalise explanatory sentences and suggest potential inference strategies for NLI. |
| Outcome: | The proposed framework generates and formalises explanatory sentences and suggests potential inference strategies for NLI. |
Neuro-Symbolic Natural Language Processing (2025.emnlp-tutorials)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) have limitations in terms of safe and controlled reasoning, interpretability and adaptability . this tutorial aims to bridge the gap between the practical performance of LLMs and the principled modelling of language and inference of formal methods. |
| Approach: | This tutorial aims to bridge the gap between the practical performance of Large Language Models and the principled modelling of language and inference of formal methods. |
| Outcome: | This tutorial aims to bridge the gap between the performance of LLMs and the principled modelling of language and inference of formal methods. |
Formally Specifying the Intended Behavior of the Program: LLM-Driven Neuro-Symbolic Program Specification Synthesis (2026.acl-demo)
Copied to clipboard
Cheng Wen, Hu Junjie, YiKun Hu, Jie Su, Bin Yu, Dugang Liu, Zhiwu Xu, Weidi Sun, Shengchao Qin, Cong Tian
| Challenge: | Formal verification typically requires developers to write detailed formal specifications . a formal verification system that generates candidate specifications is costly and error-prone . |
| Approach: | They propose an LLM-driven neuro-symbolic demonstration system that reframes specification writing as constrained structured synthesis. |
| Outcome: | The proposed system reduces hallucinations and produces proof-ready annotations. |
Evaluating Step-by-Step Reasoning through Symbolic Verification (2024.findings-naacl)
Copied to clipboard
| Challenge: | Pre-trained language models (LMs) have shown remarkable reasoning performance using explanations or chain-of-thoughts (CoT)) for in-context learning. |
| Approach: | They propose to use symbolic examples to iteratively reason over symbolic examples and to recover Prolog’s backward chaining algorithm to iterate over KBs. |
| Outcome: | The proposed model performs better on length generalization benchmarks than CoT on explanations and chain-of-thoughts (CoT) tasks. |
From Sentences to Proof Trees: Leveraging Language Models for Structured Reasoning (2026.eacl-srw)
Copied to clipboard
| Challenge: | Multi-hop reasoning requires a chain of facts to reflect the reasoning behind the answer. |
| Approach: | They propose an inference-guided prompting approach that performs well in natural language questions . they propose a neuro-symbolic approach to reasoning using large language models . |
| Outcome: | The proposed model outperforms all prompting strategies and fine-tunes LLMs trained specifically for proof generation. |
Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations (2025.acl-long)
Copied to clipboard
| Challenge: | Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations. |
| Approach: | They propose to use logical expressions to guide LLMs in generating structured proof sketches and to use them to improve their accuracy. |
| Outcome: | The proposed strategies improve autoformalisation, syntactic errors and explanation refinement over the state-of-the-art model. |
RIMRULE: Improving Tool-Using Language Agents via MDL-Guided Rule Learning (2026.acl-long)
Copied to clipboard
Xiang Gao, Yuguang Yao, Qi Zhang, Kaiwen Dong, Avinash Baidya, Ruocheng Guo, Hilaf Hasson, Kamalika Das
| Challenge: | Large language models (LLMs) struggle to use tools reliably in domain-specific settings. |
| Approach: | They propose a neuro-symbolic approach to adapt large language models to task-specific tools . they propose reusable rules that are distilled from failure traces and injected into the prompt . |
| Outcome: | Experiments show that the proposed approach outperforms prompting-based adaptation methods and complements finetuning. |