Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification¶

会议: ACL 2025
arXiv: 2506.04592
代码: https://github.com/liuchengwucn/Safe
领域: LLM 推理
关键词: 形式化验证, Lean 4, 过程奖励模型, 数学推理, 自动定理证明

一句话总结¶

提出 Safe 框架，首次利用 Lean 4 形式化语言对 LLM 数学推理的每一步进行回顾性逐步验证，通过自动形式化+自动定理证明检测幻觉，并与前瞻性 PRM 分数融合，在多个数学数据集上取得 SOTA，同时发布包含 30,809 条形式化声明的 FormalStep 基准。

研究背景与动机¶

领域现状:
CoT 推理已成为提升 LLM 推理能力的标准方法
过程奖励模型（PRM）通过对每一步打分来验证推理质量，实现 Best-of-N 采样
自动定理证明（ATP）在 Lean/Coq 等形式化环境中取得进展（如 DeepSeek-Prover）
自动形式化（Auto-Formalization）利用 LLM 将自然语言数学翻译为形式化语言
现有痛点:
PRM 是黑盒: 不提供可检查的证据，缺乏可解释性和正确性保证
CoT 幻觉难以检测: 推理步骤中的微小错误会严重影响后续推理和最终结果
形式化证明与自然语言推理隔离: 两个方向的研究各自独立，缺乏有效桥接
完整问题的形式化证明困难: miniF2F 上 DeepSeek-Prover 在布局 16×6400 下才达 60.2%
核心矛盾:
形式化验证能提供正确性保证但难以应用于完整问题
PRM 实用但不可靠——它们预测的是"前瞻性"概率（能否到达正确答案），而非"回顾性"确认（当前步骤是否正确）
两者是互补的：一个看步骤正确性，一个看前景可达性
本文要解决什么？
如何利用形式化方法验证自然语言推理步骤的正确性
如何将形式化验证（回顾性）与 PRM（前瞻性）有效融合
切入角度:
验证单步正确性（而非整个问题），降低 ATP 难度
用自动形式化将每步推理翻译为 Lean 4 定理，再用 ATP 尝试证明
四种验证状态 → LSTM 聚合 → 与 PRM 分数集成
核心idea一句话:
"数学声明的黄金标准是提供证明"——用 Lean 4 为 LLM 推理的每一步提供形式化验证证据

方法详解¶

整体框架¶

Safe 的流水线： 1. 采样与分解: 用 zero-shot CoT 采样 \(n\) 个推理轨迹，分解为步骤序列 2. 步骤验证器: 对每步进行自动形式化 + 自动定理证明 3. 状态聚合器: LSTM 聚合每步验证状态，输出回顾性分数 4. 分数融合: 回顾性分数 × 前瞻性 PRM 分数 → 最终 Best-of-N 选择

关键设计¶

步骤验证器（Step Verifier）:
做什么: 对每个推理步骤产生四种状态之一：(1)无需验证、(2)形式化失败、(3)形式化成功且证明成功、(4)形式化成功但证明失败
核心思路: 将前一步作为前提（premise），当前步作为证明目标（goal），生成 Lean 4 定理
设计动机: 单步验证比整个问题证明 简单得多，样本预算仅 16 就能达到 80%+ 的证明成功率
自动形式化模块（Auto-Formalization Module）:
做什么: 利用 LLM ICL 将自然语言推理步骤翻译为 Lean 4 形式化声明
核心思路: 不等式变换 → 变换前的不等式为前提，变换后的为目标
设计动机: 不同于传统的"翻译完整问题"的自动形式化，这里只需形式化单步正确性
自动定理证明模块（ATP Module）:
做什么: 使用 COPRA 或 DeepSeek-Prover-V1.5 对形式化声明进行证明
核心思路: 采用 DeepSeek-Prover-V1.5（7B参数），样本预算 16（不用 MCTS），证明率 >80%
设计动机: 单步声明虽然是 OOD 数据，但难度远低于完整数学问题
状态聚合器（State Aggregator）:
做什么: 用 tiny LSTM（2层, hidden=64）将验证状态序列映射为回顾性分数
核心思路: \(score_{retro}^i = \sigma(W \cdot \text{LSTM}(state_{i1}, ..., state_{ij}) + b)\)
设计动机: 验证状态有噪声（形式化/证明可能失败），需要学习从有噪声的状态推断正确性
回顾-前瞻融合:
做什么: 将 LSTM 的回顾性分数与 PRM 的前瞻性分数融合
核心思路: \(score_i = (score_{retro}^i)^\alpha \cdot (score_{pro}^i)^{1-\alpha}\)，最终选择 \(A^* = A_{i^*}, i^* = \arg\max_i score_i\)
设计动机: 两种分数互补——回顾性看步骤对不对，前瞻性看能不能到正确答案

损失函数 / 训练策略¶

LSTM 训练: 2层 LSTM，hidden=64，batch=32，lr=0.0001，200 epochs
训练数据极少: MATH 500题 + GSM8K 1000题 + CollegeMath 全部训练集
ATP 不需额外训练: 直接使用现成的 DeepSeek-Prover-V1.5
自动形式化: GPT-4o + few-shot ICL

实验关键数据¶

主实验¶

BoN@5 准确率对比（Llama-3.1-8B-Instruct）：

方法	MATH-500	GSM8K	CollegeMath
ZS-CoT@1	49.1	85.4	52.6
Majority@5	50.5	87.8	54.3
Skywork (ORM)	48.9	90.2	53.2
ArmoRM (ORM)	55.1	90.0	57.1
Shepherd (PRM)	58.1	90.2	58.3
RLHFlow (PRM)	51.7	89.9	53.6
LSTM (Ours)	55.1	88.7	55.9
Safe (Ours)	60.0	90.8	59.0
Pass@5 (上限)	70.8	95.5	72.3

跨模型结果摘要： - Llama-3.0-8B: Safe 在 MATH 上 36.3，比 Shepherd PRM (34.7) 提升 1.6%，比 Majority 提升 11.5% - GPT-4o: Safe 在 MATH 上 80.4（vs Shepherd 79.8），CollegeMath 上 74.2（vs 73.5） - DeepSeek-Math: Safe 在 MATH 上 52.4（vs Shepherd 49.7）

关键发现¶

LSTM 验证器极轻量但有效: 参数量极少（2层×64维），训练数据极少，性能与 SOTA ORM/PRM 相当
Safe = LSTM + PRM 一致超越所有基线: 回顾性与前瞻性分数的融合带来一致性提升
困难数据集提升更大: MATH-500 和 CollegeMath 提升明显，GSM8K 因难度低导致数据不平衡
单步 ATP 证明率 >80%: 仅需样本预算 16，无需 MCTS，大幅降低计算成本
验证覆盖范围: 能验证数值计算、方程求解，还能验证"充分/必要条件"等数学性质

FormalStep 数据集统计¶

类别	数量	声明长度	证明长度	证明率
Geometry	873	147.5	51.1	72.3%
Number Theory	11,515	79.5	36.4	82.1%
Algebra	5,525	107.8	39.8	81.7%
Combinatorics	9,414	125.0	49.8	81.4%
Others	3,482	112.8	25.5	79.1%
Total	30,809	104.2	41.0	81.2%

Geometry 声明最长且证明率最低（72.3%），符合直觉
整体证明率 81.2%，证明单步验证确实比完整问题容易得多

亮点与洞察¶

首个用 Lean 4 验证 LLM 自然语言推理的工作: 开创性地将形式化验证引入 CoT 验证
"回顾性 vs 前瞻性"的精辟分析: 形式化验证（这步对不对）与 PRM（能不能到正确答案）的本质区别
单步验证的 key insight: 完整问题证明太难，但单步验证简单到现有 ATP 就能处理
极轻量的 LSTM 聚合器: 词表大小仅 4，模型极小，训练数据极少，却有效
FormalStep 基准贡献: 30K+ 条形式化声明，填补了步骤级 ATP 评估的空白
Neuro-Symbolic AI 的优秀实践: 自然语言推理 + 形式化验证的互补融合

局限性 / 可改进方向¶

Lean 4 表达范围有限: 几何和组合数学的形式化能力较弱，导致部分步骤无法验证
依赖 GPT-4o 做自动形式化: 成本较高，且形式化质量受 LLM 能力限制
验证状态有噪声: 形式化失败不等于步骤错误，证明失败不等于声明错误
仅验证步骤正确性: 不能检测"步骤正确但推理方向错误"的问题
BoN@5 设定: 仅 5 个候选增加了采样多样性的需求
未来可探索更强的 ATP、更广的形式化覆盖、与 RLHF 的结合

评分¶

维度	分数 (1-10)
创新性	9
技术深度	8
实验充分性	8
写作质量	8
实用价值	8
总分	8.2