让大模型生成可机器验证的推理步骤，提升答案可信度。
Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries
- 用结构化中间步骤替代直接写证明，适合7B小模型
- 只有全部步骤通过形式化验证才给高奖励
- 适合需要可靠推理的AI系统开发者
大语言模型在复杂多步推理任务中表现优异，尤其在使用结果奖励强化学习微调后。然而，仅基于最终结果奖励常忽视中间步骤中的错误，导致正确答案却伴随不可靠推理。为此，我们提出PRoSFI（基于结构化形式中间步骤的过程奖励），一种新奖励机制，在不牺牲准确率的前提下提升推理可靠性。模型不直接生成形式化证明（7B模型难以实现），而是输出与自然语言推理对齐的结构化中间步骤，每个步骤由形式化证明器验证。只有完整通过验证的推理链才能获得高奖励。该机制引导模型生成可机器检查的逐步推导，从而产出更可信的最终答案。PRoSFI提供了一种简单有效的训练可信推理模型的方法。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。