LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervision

TL;DR

LogicReward introduces a step-wise logical supervision framework using theorem proving to enhance reasoning accuracy and faithfulness in large language models, outperforming existing models on reasoning tasks.

Contribution

The paper presents a novel reward system, LogicReward, that enforces logical correctness at each reasoning step using theorem proving, along with Autoformalization with Soft Unification to improve formalization.

Findings

Model trained with LogicReward surpasses GPT-4o and o4-mini on reasoning tasks.

LogicReward improves reasoning faithfulness and generalizability.

Provides reliable reward signals without ground-truth labels.

Abstract

Although LLMs exhibit strong reasoning capabilities, existing training methods largely depend on outcome-based feedback, which can produce correct answers with flawed reasoning. Prior work introduces supervision on intermediate steps but still lacks guarantees of logical soundness, which is crucial in high-stakes scenarios where logical consistency is paramount. To address this, we propose LogicReward, a novel reward system that guides model training by enforcing step-level logical correctness with a theorem prover. We further introduce Autoformalization with Soft Unification, which reduces natural language ambiguity and improves formalization quality, enabling more effective use of the theorem prover. An 8B model trained on data constructed with LogicReward surpasses GPT-4o and o4-mini by 11.6\% and 2\% on natural language inference and logical reasoning tasks with simple training procedures. Further analysis shows that LogicReward enhances reasoning faithfulness, improves generalizability to unseen tasks such as math and commonsense reasoning, and provides a reliable reward signal even without ground-truth labels. We will release all data and code at https://llm-symbol.github.io/LogicReward.