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

TL;DR

PCRLLM introduces a framework that constrains LLM reasoning to single steps with explicit premises, rules, and conclusions, enabling verification and collaboration under formal logic constraints to improve trustworthiness.

Contribution

It presents a novel proof-carrying reasoning framework for LLMs that enhances logical coherence, verification, and multi-model collaboration using explicit step-level reasoning.

Findings

Enables verification of reasoning steps against formal logic.

Supports multi-LLM collaboration with formal constraints.

Introduces a benchmark for step-level reasoning data.

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.