PRoSFI：通过形式化中间表示提升大语言模型推理可靠性的新方法

PRoSFI核心导读

PRoSFI（Process Reward over Structured Formal Intermediates）是一种提升大语言模型推理可靠性的新方法。其核心在于通过结构化形式化中间步骤和过程奖励机制，让7B参数级别的模型生成可机器验证的推理链，解决了传统结果奖励忽略中间推理错误的问题。该方法平衡了形式化验证的可靠性与模型生成的可行性，为构建可信推理模型提供了新路径。

推理模型的可靠性困境

近年来，大语言模型在复杂多步推理任务上通过结果奖励强化学习取得进展，但存在根本性问题：结果奖励仅关注最终答案正确与否，忽略中间步骤质量。这导致模型可能因“蒙对”答案获得奖励，却存在严重推理缺陷。在数学证明、法律分析、医疗诊断等需高可信度的场景中，这种“结果正确但过程错误”的现象构成信任障碍。

直接生成形式化证明的挑战

形式化证明逻辑严密且可通过自动定理证明器验证，但直接生成完整形式化证明对模型能力要求极高。即使最先进的模型，在复杂任务上也难以生成正确的形式化证明，7B级别模型更是几乎不可能。因此，需寻找务实方法，兼顾形式化验证优势与模型能力现实。

PRoSFI方法核心思想

PRoSFI不要求模型直接输出完整形式化证明，而是生成与自然语言推理对齐的结构化中间步骤，再由外部形式化证明器逐一验证。此方法降低了模型任务难度（只需生成结构化中间表示），同时通过严格验证确保每步推理的逻辑正确性。只有完整验证通过的推理链才能获高分奖励，引导模型学习可靠推理过程。

技术实现细节

PRoSFI包含两个关键组件：

1. 结构化形式化中间表示：模型生成自然语言推理时，输出对应的结构化步骤（形式化骨架，保留精确性且灵活），每个步骤对应一个逻辑环节，形成完整推理链。
2. 过程奖励机制：形式化证明器验证每个中间步骤，仅当所有步骤通过验证时模型获高分；若中间有误，即使结果正确，奖励也大幅降低。这种细粒度奖励指导模型优化推理过程而非仅结果。

方法优势：可靠性与准确性平衡

PRoSFI解决了传统结果奖励的两难困境：既避免了严格标准导致的收敛困难/准确性下降，也防止宽松标准牺牲可靠性。形式化验证提供客观、可量化的可靠性度量，不受文本流畅性影响。实验表明，PRoSFI在不牺牲最终答案准确性的前提下，显著提升推理过程的可靠性，每步推理均经得起逻辑检验。

应用前景与意义

PRoSFI为可信推理模型提供切实技术路径，适用于高可靠性场景：

• 数学教育：为学生提供验证过的解题步骤；
• 科研辅助：提供逻辑严密的分析思路；
• 自动定理证明：辅助专家提升生成效率。 此外，PRoSFI展示了形式化方法与LLM结合的新范式，可扩展到程序验证、逻辑谜题、法律推理等领域，未来潜力巨大。