Research map / Large language models / Reasoning and chain of thought

LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervision

ICLR 2026 · Large language models › Reasoning and chain of thought · approach: Search and self-correction in reasoning · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Proposes LogicReward, a reward combining premise grounding and Isabelle theorem-prover logic checks (with soft unification autoformalization) to build SFT/DPO data, yielding an 8B model that outperforms o4-mini and GPT-4o on NLI and logical reasoning benchmarks.

Problem

Outcome-only rewards let LLMs reach correct answers through flawed reasoning, and probabilistic process rewards do not guarantee logical soundness, which matters in high-stakes settings.

Approach

A step-level reward that combines embedding-based premise validity with theorem-prover (Isabelle) logic validity over autoformalized steps, where LLM soft unification adds implicit assumptions to reduce formalization failures; the reward selects SFT targets and DPO pairs.

Key results

• LogicReward-Qwen (Qwen3-8B + LogicReward) averages 85.5 across eight benchmarks, vs 83.5 for o4-mini and 82.6 for QwQ-32B; reported as +2.0 over o4-mini.
• LogicReward-Llama improves Llama3.1-8B-Instruct average from 60.4 to 71.4 (+11.0).
• Under identical Llama3.1-8B training, LogicReward (71.4 avg) beats Confidence (64.3), LLM-as-judge (60.2), and PRM (66.0).

Surprising findings

• Many LLM reasoning steps were judged logically invalid by Isabelle even when the final answer was correct.
• Removing SFT causes the largest ablation drop (22.9%), exceeding removing DPO (5.9%).

Limitations

• Autoformalization remains imperfect; some natural-language ambiguities are hard to formalize even with soft unification.
• Labeling with the theorem prover is slower than outcome-only rewards, limiting on-policy RL use.
• Logic validity falls back to token confidence when syntax is invalid.

Experimental setup

Datasets: Multi-LogiEval ProofWriter FOLIO ProntoQA ProverQA LogiQA e-SNLI QASC BBH (BoardgameQA) GSM8K CommonsenseQA

Benchmarks: Multi-LogiEval ProofWriter FOLIO ProntoQA ProverQA LogiQA e-SNLI QASC BBH GSM8K CommonsenseQA

Metrics: accuracy (exact match) faithfulness (manual evaluation of 100 correct responses)

Baselines: GPT-4o GPT-4.1 o4-mini DeepSeek-R1-8B Qwen3-8B QwQ-32B Confidence reward LLM-as-judge PRM (Nemotron-70B-Reward)

Builds on: DPO Chain-of-thought LINC Logic-LM LoRA

Closest papers by meaning

• General-Reasoner: Advancing LLM Reasoning Across All Domains (NeurIPS 2025 · similarity 0.90)
• Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpus (NeurIPS 2024 · similarity 0.90)
• Right Question is Already Half the Answer: Fully Unsupervised LLM Reasoning Incentivization (NeurIPS 2025 · similarity 0.89)
• Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · similarity 0.89)
• Incentivizing LLMs to Self-Verify Their Answers (NeurIPS 2025 · similarity 0.88)
• Reinforcing General Reasoning Without Verifiers (ICLR 2026 · similarity 0.88)