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. |
Similar Papers
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. |
Self-Critique and Refinement for Faithful Natural Language Explanations (2025.emnlp-main)
Copied to clipboard
| Challenge: | Existing work has demonstrated that Large Language Models (LLMs) can self-critique and refine their initial outputs, but this capability remains unexplored for improving explanation faithfulness. |
| Approach: | They propose a framework that enables models to improve the faithfulness of their own explanations through an iterative critique and refinement process without external supervision. |
| Outcome: | The proposed framework reduces unfaithfulness rates in three datasets and four state-of-the-art LLMs by 36% compared to 54.81% for baseline. |
Large Language Models Help Humans Verify Truthfulness – Except When They Are Convincingly Wrong (2024.naacl-long)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) are increasingly used for accessing information on the web. |
| Approach: | They conduct experiments with 80 crowdworkers to compare LLMs with search engines . they ask LLM to provide contrastive information to reduce over-reliance on LLM . |
| Outcome: | The results show that LLMs can outperform search engines but not LLM explanations . the study shows that LMS explanations are not reliable replacements for reading retrieved passages compared to search engines alone. |
MASA: LLM-Driven Multi-Agent Systems for Autoformalization (2025.emnlp-demos)
Copied to clipboard
| Challenge: | This paper presents a framework for building multi-agent systems for autoformalization driven by Large Language Models. |
| Approach: | They propose a framework for building multi-agent systems for autoformalization driven by Large Language Models. |
| Outcome: | The proposed framework leverages collaborative agents to convert natural language statements into formal representations. |
Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation (2024.acl-long)
Copied to clipboard
| Challenge: | Logic-based approaches to reasoning have lost popularity due to limited scalability and coverage. |
| Approach: | They present a dataset of 28K sentence-level NL-FOL pairs from GPT4 and a LogicLLaMA2-7B/13B fine-tuned on MALLS for NL translation. |
| Outcome: | The proposed model can be used standalone or to correct previously generated rules by GPT3.5. |
LLM2: Let Large Language Models Harness System 2 Reasoning (2025.naacl-short)
Copied to clipboard
| Challenge: | Empirical results on mathematical reasoning benchmarks substantiate the efficacy of Large language models (LLMs). |
| Approach: | They propose a framework that combines an LLM with a process-based verifier to generate plausible candidates and provide timely process-driven feedback to distinguish desirable and undesirable outputs. |
| Outcome: | Empirical results show that LLM2 improves accuracy on GSM8K and self-consistency increases major@20 accuracy. |
Self-Correction Makes LLMs Better Parsers (2025.findings-emnlp)
Copied to clipboard
| Challenge: | Large language models (LLMs) have achieved remarkable success across various natural language processing tasks, but they still face challenges in performing fundamental NLP tasks, such as syntactic parsing. |
| Approach: | They propose a method that leverages grammar rules from existing treebanks to guide LLMs in correcting previous errors. |
| Outcome: | The proposed method significantly improves performance on in-domain and cross-domain datasets. |
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. |
Towards Fast Multilingual LLM Inference: Speculative Decoding and Specialized Drafters (2024.emnlp-main)
Copied to clipboard
| Challenge: | Large language models (LLMs) have revolutionized natural language processing and are limited by high inference time in multilingual settings. |
| Approach: | They propose a training recipe for an assistant model in speculative decoding, which are leveraged to draft and-then its future tokens are verified by the target LLM. |
| Outcome: | The proposed model significantly speeds up inference time and out-of-domain speedup across various languages. |
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. |