PCRLLM: Proof-Carrying Reasoning with Large Language Models under Stepwise Logical Constraints

• URL: http://arxiv.org/abs/2511.08392v1
• Date: Wed, 12 Nov 2025 01:57:01 GMT
• Title: PCRLLM: Proof-Carrying Reasoning with Large Language Models under Stepwise Logical Constraints
• Authors: Tangrui Li, Pei Wang, Hongzheng Wang Christian Hahm, Matteo Spatola, Justin Shi,
• Abstract summary: We propose Proof-Carrying Reasoning with Large Language Models (PCRLLM)<n>PCRLLM constrains reasoning to single-step inferences while preserving natural language formulations.<n>We introduce a benchmark schema for generating large-scale step-level reasoning data.
• Score: 2.8310349862016726
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) often exhibit limited logical coherence, mapping premises to conclusions without adherence to explicit inference rules. We propose Proof-Carrying Reasoning with LLMs (PCRLLM), a framework that constrains reasoning to single-step inferences while preserving natural language formulations. Each output explicitly specifies premises, rules, and conclusions, thereby enabling verification against a target logic. This mechanism mitigates trustworthiness concerns by supporting chain-level validation even in black-box settings. Moreover, PCRLLM facilitates systematic multi-LLM collaboration, allowing intermediate steps to be compared and integrated under formal rules. Finally, we introduce a benchmark schema for generating large-scale step-level reasoning data, combining natural language expressiveness with formal rigor.

Related papers

• Beyond Correctness: Exposing LLM-generated Logical Flaws in Reasoning via Multi-step Automated Theorem Proving [11.24425572063955]
  Large Language Models (LLMs) have demonstrated impressive reasoning capabilities, leading to their adoption in high-stakes domains such as healthcare, law, and scientific research.<n>They often contain subtle logical errors masked by fluent language, posing significant risks for critical applications.<n>We present MATP, an evaluation framework for systematically verifying LLM reasoning via Multi-step Automatic Theorem Proving.
  arXiv  Detail & Related papers  (2025-12-29T14:48:15Z)
• Last Layer Logits to Logic: Empowering LLMs with Logic-Consistent Structured Knowledge Reasoning [55.55968342644846]
  Large Language Models (LLMs) achieve excellent performance in natural language reasoning tasks through pre-training on vast unstructured text.<n>We propose the textitLogits-to-Logic framework, which incorporates logits strengthening and logits filtering as core modules to correct logical defects in LLM outputs.
  arXiv  Detail & Related papers  (2025-11-11T07:08:27Z)
• Abductive Logical Rule Induction by Bridging Inductive Logic Programming and Multimodal Large Language Models [22.49558896794021]
  We propose ILP-CoT, a method that bridges Inductive Logic Programming (ILP) and Multimodal Large Language Models (MLLMs)<n>The task involves both discovering logical facts and inducing logical rules from a small number of unstructured textual or visual inputs.<n>Our approach automatically builds ILP tasks with pruned search spaces based on the rule structure proposals from MLLMs.
  arXiv  Detail & Related papers  (2025-09-26T04:56:19Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  Large Language Models (LLMs) have demonstrated strong generalization across a wide range of tasks.<n>Recent studies have shifted attention from explicit chain-of-thought prompting toward implicit reasoning.<n>This survey introduces a taxonomy centered on execution paradigms, shifting the focus from representational forms to computational strategies.
  arXiv  Detail & Related papers  (2025-09-02T14:16:02Z)
• Revisiting LLM Reasoning via Information Bottleneck [57.519119962528166]
  Large language models (LLMs) have recently demonstrated remarkable progress in reasoning capabilities through reinforcement learning with verifiable rewards (RLVR)<n>We present a theoretical characterization of LLM reasoning grounded in information bottleneck (IB) principle.<n>We propose IB-aware reasoning optimization (IBRO), a framework that encourages reasoning trajectories to be both informative about the final correct answer and generalizable.
  arXiv  Detail & Related papers  (2025-07-24T13:14:25Z)
• CTRLS: Chain-of-Thought Reasoning via Latent State-Transition [57.51370433303236]
  Chain-of-thought (CoT) reasoning enables large language models to break down complex problems into interpretable intermediate steps.<n>We introduce groundingS, a framework that formulates CoT reasoning as a Markov decision process (MDP) with latent state transitions.<n>We show improvements in reasoning accuracy, diversity, and exploration efficiency across benchmark reasoning tasks.
  arXiv  Detail & Related papers  (2025-07-10T21:32:18Z)
• 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)<n>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)
• 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)
• Inductive Learning of Logical Theories with LLMs: An Expressivity-Graded Analysis [9.865771016218549]
  This work presents a novel systematic methodology to analyse the capabilities and limitations of Large Language Models (LLMs)<n>The analysis is complexity-graded w.r.t. rule dependency structure, allowing quantification of specific inference challenges on LLM performance.
  arXiv  Detail & Related papers  (2024-08-15T16:41:00Z)
• DECIDER: A Dual-System Rule-Controllable Decoding Framework for Language Generation [57.07295906718989]
  Constrained decoding approaches aim to control the meaning or style of text generated by pre-trained large language (Ms also PLMs) for various tasks at inference time.<n>These methods often guide plausible continuations by greedily and explicitly selecting targets.<n>Inspired by cognitive dual-process theory, we propose a novel decoding framework DECIDER.
  arXiv  Detail & Related papers  (2024-03-04T11:49:08Z)
• Can LLMs Reason with Rules? Logic Scaffolding for Stress-Testing and Improving LLMs [87.34281749422756]
  Large language models (LLMs) have achieved impressive human-like performance across various reasoning tasks. However, their mastery of underlying inferential rules still falls short of human capabilities. We propose a logic scaffolding inferential rule generation framework, to construct an inferential rule base, ULogic.
  arXiv  Detail & Related papers  (2024-02-18T03:38:51Z)
• Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning [74.90592233107712]
  We propose a Direct-Indirect Reasoning (DIR) method, which considers Direct Reasoning (DR) and Indirect Reasoning (IR) as multiple parallel reasoning paths that are merged to derive the final answer.<n>Our DIR method is simple yet effective and can be straightforwardly integrated with existing variants of CoT methods.
  arXiv  Detail & Related papers  (2024-02-06T03:41:12Z)

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.