Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries

• URL: http://arxiv.org/abs/2603.29500v1
• Date: Tue, 31 Mar 2026 09:42:13 GMT
• Title: Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries
• Abstract summary: PRoSFI (Process Reward over Structured Formal Intermediates) is a novel reward method that enhances reasoning reliability without compromising accuracy.<n>Only fully validated reasoning chains receive high rewards.<n>The integration of formal verification guides the model towards generating step-by-step machine-checkable proofs.
• Score: 18.744562922743405
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) have recently demonstrated impressive performance on complex, multi-step reasoning tasks, especially when post-trained with outcome-rewarded reinforcement learning Guo et al. 2025. However, it has been observed that outcome rewards often overlook flawed intermediate steps, leading to unreliable reasoning steps even when final answers are correct. To address this unreliable reasoning, we propose PRoSFI (Process Reward over Structured Formal Intermediates), a novel reward method that enhances reasoning reliability without compromising accuracy. Instead of generating formal proofs directly, which is rarely accomplishable for a modest-sized (7B) model, the model outputs structured intermediate steps aligned with its natural language reasoning. Each step is then verified by a formal prover. Only fully validated reasoning chains receive high rewards. The integration of formal verification guides the model towards generating step-by-step machine-checkable proofs, thereby yielding more credible final answers. PRoSFI offers a simple and effective approach to training trustworthy reasoning models.

Related papers

• Learning from Partial Chain-of-Thought via Truncated-Reasoning Self-Distillation [15.338493974763471]
  We introduce Truncated-Reasoning Self-Distillation (TRSD), a lightweight post-training procedure that encourages models to produce correct predictions from partial reasoning traces.<n>We demonstrate that TRSD improves robustness to truncated inference, with far reduced accuracy tradeoffs when applied to a diverse set of reasoning models.
  arXiv  Detail & Related papers  (2026-02-27T06:08:22Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  Large Language Models (LLMs) show remarkable capabilities, yet their next-token prediction creates logical inconsistencies and reward hacking.<n>We introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process.<n>We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization.
  arXiv  Detail & Related papers  (2026-01-30T07:01:25Z)
• Structured Reasoning for Large Language Models [59.215789462977206]
  We propose Structured Reasoning (SCR), a framework that decouples reasoning trajectories into explicit, evaluable, and trainable components.<n>SCR substantially improves reasoning efficiency and self-verification.<n>Compared with existing reasoning paradigms, it reduces output token length by up to 50%.
  arXiv  Detail & Related papers  (2026-01-12T04:04:01Z)
• Training LLMs with LogicReward for Faithful and Rigorous Reasoning [75.30425553246177]
  We propose LogicReward, a reward system that guides model training by enforcing step-level logical correctness with a theorem prover.<n>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.
  arXiv  Detail & Related papers  (2025-12-20T03:43:02Z)
• Step-Aware Policy Optimization for Reasoning in Diffusion Large Language Models [57.42778606399764]
  Diffusion language models (dLLMs) offer a promising, non-autoregressive paradigm for text generation.<n>Current reinforcement learning approaches often rely on sparse, outcome-based rewards.<n>We argue that this stems from a fundamental mismatch with the natural structure of reasoning.
  arXiv  Detail & Related papers  (2025-10-02T00:34:15Z)
• Typed Chain-of-Thought: A Curry-Howard Framework for Verifying LLM Reasoning [0.0]
  Chain-of-Thought (CoT) prompting enhances the reasoning capabilities of large language models.<n>We propose a novel theoretical lens for this problem grounded in the Curry-Howard correspondence.<n>We operationalise this analogy, presenting methods to extract and map the informal, natural language steps of CoT into a formal, typed proof structure.
  arXiv  Detail & Related papers  (2025-10-01T16:06:40Z)
• StepProof: Step-by-step verification of natural language mathematical proofs [16.150265021594088]
  We propose StepProof, a novel autoformalization method for granular, step-by-step verification.<n>StepProof breaks down complete proofs into multiple verifiable subproofs, enabling sentence-level verification.<n>We show that StepProof significantly improves proof success rates and efficiency compared to traditional methods.
  arXiv  Detail & Related papers  (2025-06-12T10:31:23Z)
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  This paper investigates the logical reasoning capabilities of large language models (LLMs)<n>A trained LLM receives as input a set of assumptions and a goal, and produces as output a proof that formally derives the goal from the assumptions.<n>A critical obstacle for training is the scarcity of real-world proofs.
  arXiv  Detail & Related papers  (2025-04-28T19:25:29Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  We introduce LeanProgress, a method that predicts the progress in the proof.<n>Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.1%.
  arXiv  Detail & Related papers  (2025-02-25T07:46:36Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Deductive Verification of Chain-of-Thought Reasoning [22.79166959432764]
  Large Language Models (LLMs) benefit from Chain-of-Thought prompting in performing various reasoning tasks. While CoT allows models to produce more comprehensive reasoning processes, its emphasis on intermediate reasoning steps can inadvertently introduce hallucinations and accumulated errors. We propose Natural Program, a natural language-based deductive reasoning format.
  arXiv  Detail & Related papers  (2023-06-06T17:18:56Z)

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.