Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation

• URL: http://arxiv.org/abs/2502.06563v1
• Date: Mon, 10 Feb 2025 15:31:54 GMT
• Title: Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation
• Authors: Chengwen Qi, Ren Ma, Bowen Li, He Du, Binyuan Hui, Jinwang Wu, Yuanjun Laili, Conghui He,
• Abstract summary: First-order logic (FOL) reasoning is pivotal for intelligent systems. Existing benchmarks often rely on extensive human annotation or handcrafted templates. We propose a novel framework called ProverGen that synergizes the generative strengths of Large Language Models with the rigor and precision of symbolic provers.
• Score: 24.081573908824353
• License:
• Abstract: First-order logic (FOL) reasoning, which involves sequential deduction, is pivotal for intelligent systems and serves as a valuable task for evaluating reasoning capabilities, particularly in chain-of-thought (CoT) contexts. Existing benchmarks often rely on extensive human annotation or handcrafted templates, making it difficult to achieve the necessary complexity, scalability, and diversity for robust evaluation. To address these limitations, we propose a novel framework called ProverGen that synergizes the generative strengths of Large Language Models (LLMs) with the rigor and precision of symbolic provers, enabling the creation of a scalable, diverse, and high-quality FOL reasoning dataset, ProverQA. ProverQA is also distinguished by its inclusion of accessible and logically coherent intermediate reasoning steps for each problem. Our evaluation shows that state-of-the-art LLMs struggle to solve ProverQA problems, even with CoT prompting, highlighting the dataset's challenging nature. We also finetune Llama3.1-8B-Instruct on a separate training set generated by our framework. The finetuned model demonstrates consistent improvements on both in-distribution and out-of-distribution test sets, suggesting the value of our proposed data generation framework. Code available at: https://github.com/opendatalab/ProverGen

Related papers

• Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment [21.12989936864145]
  Chain-of-Thought (CoT) prompting has shown promise in enhancing the reasoning capabilities of large language models (LLMs) We propose Reasoning-as-Logic-Units (RaLU), which constructs a more reliable reasoning path by aligning logical units between the generated program and their corresponding NL descriptions.
  arXiv  Detail & Related papers  (2025-02-05T08:23:18Z)
• BRiTE: Bootstrapping Reinforced Thinking Process to Enhance Language Model Reasoning [78.63421517563056]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in complex reasoning tasks. We present a unified probabilistic framework that formalizes LLM reasoning through a novel graphical model. We introduce the Bootstrapping Reinforced Thinking Process (BRiTE) algorithm, which works in two steps.
  arXiv  Detail & Related papers  (2025-01-31T02:39:07Z)
• TARGA: Targeted Synthetic Data Generation for Practical Reasoning over Structured Data [9.390415313514762]
  TARGA is a framework that generates high-relevance synthetic data without manual annotation. It substantially outperforms existing non-fine-tuned methods that utilize close-sourced model. It exhibits superior sample efficiency, robustness, and generalization capabilities under non-I.I.D. settings.
  arXiv  Detail & Related papers  (2024-12-27T09:16:39Z)
• SRA-MCTS: Self-driven Reasoning Augmentation with Monte Carlo Tree Search for Code Generation [14.786100203787194]
  Large language models demonstrate exceptional performance in simple code generation tasks but face challenges in tackling complex problems. We propose a reasoning-augmented data generation process, SRA-MCTS, which guides the model to autonomously generate high-quality intermediate reasoning paths. Our method operates entirely through the model itself without requiring additional supervision.
  arXiv  Detail & Related papers  (2024-11-17T12:31:04Z)
• Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning [1.3003982724617653]
  Large Language Models (LLMs) have revolutionized natural language processing, yet they struggle with inconsistent reasoning. This research introduces Proof of Thought, a framework that enhances the reliability and transparency of LLM outputs. Key contributions include a robust type system with sort management for enhanced logical integrity, explicit representation of rules for clear distinction between factual and inferential knowledge.
  arXiv  Detail & Related papers  (2024-09-25T18:35:45Z)
• Unlocking Reasoning Potential in Large Langauge Models by Scaling Code-form Planning [94.76546523689113]
  We introduce CodePlan, a framework that generates and follows textcode-form plans -- pseudocode that outlines high-level, structured reasoning processes. CodePlan effectively captures the rich semantics and control flows inherent to sophisticated reasoning tasks. It achieves a 25.1% relative improvement compared with directly generating responses.
  arXiv  Detail & Related papers  (2024-09-19T04:13:58Z)
• A Large-Scale Evaluation of Speech Foundation Models [110.95827399522204]
  We establish the Speech processing Universal PERformance Benchmark (SUPERB) to study the effectiveness of the foundation model paradigm for speech. We propose a unified multi-tasking framework to address speech processing tasks in SUPERB using a frozen foundation model followed by task-specialized, lightweight prediction heads.
  arXiv  Detail & Related papers  (2024-04-15T00:03:16Z)
• ChainLM: Empowering Large Language Models with Improved Chain-of-Thought Prompting [124.69672273754144]
  Chain-of-Thought (CoT) prompting can enhance the reasoning capabilities of large language models (LLMs) Existing CoT approaches usually focus on simpler reasoning tasks and thus result in low-quality and inconsistent CoT prompts. We introduce CoTGenius, a novel framework designed for the automatic generation of superior CoT prompts.
  arXiv  Detail & Related papers  (2024-03-21T11:34:26Z)
• SymbolicAI: A framework for logic-based approaches combining generative models and solvers [9.841285581456722]
  We introduce SymbolicAI, a versatile and modular framework employing a logic-based approach to concept learning and flow management in generative processes. We treat large language models (LLMs) as semantic solvers that execute tasks based on both natural and formal language instructions.
  arXiv  Detail & Related papers  (2024-02-01T18:50:50Z)
• MuSR: Testing the Limits of Chain-of-thought with Multistep Soft Reasoning [63.80739044622555]
  We introduce MuSR, a dataset for evaluating language models on soft reasoning tasks specified in a natural language narrative. This dataset has two crucial features. First, it is created through a novel neurosymbolic synthetic-to-natural generation algorithm. Second, our dataset instances are free text narratives corresponding to real-world domains of reasoning.
  arXiv  Detail & Related papers  (2023-10-24T17:59:20Z)
• Logical Natural Language Generation from Open-Domain Tables [107.04385677577862]
  We propose a new task where a model is tasked with generating natural language statements that can be emphlogically entailed by the facts. To facilitate the study of the proposed logical NLG problem, we use the existing TabFact dataset citechen 2019tabfact featured with a wide range of logical/symbolic inferences. The new task poses challenges to the existing monotonic generation frameworks due to the mismatch between sequence order and logical order.
  arXiv  Detail & Related papers  (2020-04-22T06:03:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.